Functions

Functions are the heart of IML. Every function you define is both an executable program and a mathematical definition that ImandraX can reason about. The key requirement is that all recursive functions must terminate.

Defining functions

Simple (non-recursive) functions use let:

let double x = x + x
let max a b = if a >= b then a else b
let hypotenuse a b = Int.sqrt (a * a + b * b)

Recursive functions

Recursive functions use let rec:

let rec factorial n =
  if n <= 0 then 1
  else n * factorial (n - 1)
 
let rec length = function
  | [] -> 0
  | _ :: xs -> 1 + length xs
 
let rec sum_tree = function
  | Leaf x -> x
  | Node (a, b) -> sum_tree a + sum_tree b

When you define a recursive function, ImandraX automatically attempts to prove it terminates. For the common patterns above — structural recursion on a list or tree, numeric recursion with a decreasing argument — termination is proved automatically.

Why termination matters

Termination is not a technicality — it is fundamental to logical consistency.

Consider what would happen if ImandraX accepted a non-terminating function:

(* REJECTED — this does not terminate *)
let rec bad x = bad x + 1

If this were accepted, its defining equation bad x = bad x + 1 would imply 0 = 1, allowing you to "prove" anything. ImandraX's definitional principle (conservative extensions) prevents this: every definition must be shown to preserve consistency, and termination is the key requirement.

The proof-theoretic foundation is based on ordinals up to ε₀ (epsilon-zero). Every recursive function is associated with an ordinal-valued measure that strictly decreases on each recursive call. ImandraX attempts to synthesize this measure automatically.

Automatic termination proofs

For structural recursion (recursion on a structurally smaller subterm), termination is automatic:

(* Structural recursion on a list — automatic *)
let rec map f = function
  | [] -> []
  | x :: xs -> f x :: map f xs
 
(* Structural recursion on a tree — automatic *)
let rec size = function
  | Leaf _ -> 1
  | Node (l, r) -> size l + size r + 1

For numeric recursion where an argument decreases, termination is usually automatic too:

let rec sum n =
  if n <= 0 then 0
  else n + sum (n - 1)

Custom termination measures with [@@adm]

When automatic termination synthesis fails, you provide a measure explicitly. The [@@adm] attribute specifies a lexicographic ordering on arguments:

(* Ackermann's function — needs lexicographic measure on (m, n) *)
let rec ack m n =
  if m <= 0 then n + 1
  else if n <= 0 then ack (m - 1) 1
  else ack (m - 1) (ack m (n - 1))
[@@adm m, n]

The [@@adm m, n] annotation tells ImandraX to prove termination using the lexicographic ordering on (m, n): either m strictly decreases, or m stays the same and n strictly decreases.

Custom ordinal measures with [@@measure]

For more sophisticated termination arguments, you can provide an explicit ordinal-valued measure using [@@measure]:

let rec merge_sort l =
  match l with
  | [] -> []
  | [_] -> l
  | _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))
[@@measure Ordinal.of_int (List.length l)]

Here the measure is the length of the list l, expressed as an ordinal. ImandraX verifies that List.length (odds l) < List.length l for non-trivial lists (with the help of a forward-chaining lemma about odds).

Mutually recursive functions

Use and for mutually recursive definitions:

let rec even n =
  if n <= 0 then true
  else odd (n - 1)
 
and odd n =
  if n <= 0 then false
  else even (n - 1)

Both functions must terminate together under a common measure.

Higher-order functions

IML supports higher-order functions — functions that take or return other functions:

let apply f x = f x
let compose f g x = f (g x)
 
let rec filter pred = function
  | [] -> []
  | x :: xs ->
    if pred x then x :: filter pred xs
    else filter pred xs

Higher-order functions are one of IML's strengths, allowing natural, concise code. Behind the scenes, ImandraX uses lambda-lifting and specialization to reduce higher-order definitions to first-order form for automated reasoning.

(* Using higher-order functions naturally *)
let positives xs = filter (fun x -> x > 0) xs
let squares xs = List.map (fun x -> x * x) xs

Anonymous functions

Use fun to create anonymous (lambda) functions:

let add_one = fun x -> x + 1
let sum_pair = fun (a, b) -> a + b
 
(* Common with verify and instance *)
verify (fun x -> x + 1 > x)
instance (fun xs -> List.length xs > 5 && List.hd xs = 0)

Currying

Multi-argument functions are automatically curried:

let add x y = x + y
 
(* Partial application *)
let add5 = add 5
eval add5 3  (* 8 *)

Induction schemes from termination

An important consequence of termination proofs: the termination data for a recursive function generates an induction scheme that ImandraX can use in proofs. When you write [@@by auto], ImandraX selects an induction scheme derived from the recursive functions in your goal.

For example, the termination proof for length generates an induction scheme that splits into:

• Base case: xs = []
• Inductive step: xs = x :: xs', with inductive hypothesis about xs'

This dual purpose — termination proofs both ensure consistency and generate proof strategies — is a key insight of ImandraX's design.

A real-world example

Here's the termination annotation from the merge sort example, showing all the pieces working together:

let rec merge (l : int list) (m : int list) =
  match l, m with
  | [], _ -> m
  | _, [] -> l
  | a :: ls, b :: ms ->
    if a < b then a :: (merge ls m)
    else b :: (merge l ms)
[@@adm l, m]
[@@by auto]

The [@@adm l, m] annotation establishes the use of a lexicographic measure on l and m for the termination argument proving admissibility of the function. The [@@by auto] proves the termination obligation using the waterfall.