Termination

Every recursive function admitted into ImandraX's logic must be proved terminating (total) — it must halt on every possible input. This is not a technicality but a fundamental requirement for logical consistency.

Why termination matters

ImandraX's logical foundation rests on the principle of conservative extensions: every new definition preserves the consistency of the logic. If a non-terminating function were admitted, its defining equation could derive contradictions.

Consider:

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

If this were accepted, the defining equation bad x = bad x + 1 would hold. Subtracting bad x from both sides gives 0 = 1. From there, you could "prove" anything — the logic would be unsound.

By requiring termination, ImandraX ensures that:

Every defining equation is consistent
Every function has a well-defined value on every input
Induction schemes derived from function definitions are sound

The third point is especially important: termination proofs do double duty. They both preserve consistency and generate the induction principles used in proofs. The structure of a termination argument tells ImandraX exactly how to perform induction over the function.

Ordinals up to ε₀

ImandraX proves termination using ordinal-valued measures. The idea: associate each function call with an ordinal value, and show that recursive calls have strictly smaller ordinals.

Ordinals are beautiful mathematical objects representing equivalence classes of well-orderings. The finite ordinals are just the natural numbers: 0, 1, 2, 3, ... After all the finite ordinals comes ω (omega), the first infinite ordinal. Then ω+1, ω+2, ..., ω·2, ω·2+1, ..., ω², ..., ω^ω, ..., ω^ω^ω, and so on, building an extraordinary tower of infinities — each well-ordered.

Ordinals up to ω^ω, showing the structure of ordinal arithmetic

ε₀ (epsilon-zero) is the smallest ordinal satisfying ε₀ = ω^ε₀ — the limit of the tower ω, ω^ω, ω^ω^ω, ω^ω^ω^ω, ... This ordinal occupies a central place in the foundations of mathematics: in Gentzen's famous 1936 proof of the consistency of Peano Arithmetic, ε₀ appears as the proof-theoretic ordinal measuring the strength of arithmetic induction. ImandraX supports ordinals up to ε₀, giving it the same proof-theoretic strength as Peano arithmetic and ACL2 — powerful enough to express essentially all the mathematics encountered in program verification.

The well-foundedness of the ordering on ordinals below ε₀ is an axiom of ImandraX's logic. Every other fact about ordinals is derived from their definition.

Cantor Normal Form representation

ImandraX encodes ordinals below ε₀ as a datatype using a variant of Cantor Normal Form. Every ordinal below ε₀ can be uniquely written as a finite sum:

c₁·ω^a₁ + c₂·ω^a₂ + ... + cₖ·ω^aₖ + n

where a₁ > a₂ > ... > aₖ are themselves ordinals below ε₀ (the exponents are recursively ordinals), each cᵢ is a positive integer coefficient, and n is a natural number.

The Ordinal.t type in ImandraX's prelude implements this directly:

type t =
  | Int of int
  | Cons of t * int * t

where:

Int n represents a finite ordinal (natural number n)
Cons (a, x, tl) represents x·ω^a + tl, where a is the exponent (itself an ordinal), x is the coefficient, and tl is the remaining (smaller) sum

For example:

Int 5 is the ordinal 5
Cons (Int 1, 3, Int 2) is 3·ω + 2
Cons (Int 2, 1, Cons (Int 1, 2, Int 0)) is ω² + 2·ω
Cons (Cons (Int 1, 1, Int 0), 1, Int 0) is ω^ω

Ordinal ordering

The ordering << on ordinals is defined lexicographically on the Cantor Normal Form. This is one of the most fundamental definitions in the system — it is the well-founded relation that bootstraps all termination proofs:

let rec ( << ) (x : t) (y : t) : bool =
  match x, y with
  | Int x, Int y -> x < y
  | Int _, Cons _ -> true        (* finite < infinite *)
  | Cons _, Int _ -> false       (* infinite ≮ finite *)
  | Cons (a1, x1, tl1), Cons (a2, x2, tl2) ->
    a1 << a2                     (* leading exponent smaller *)
    || (a1 = a2 && (x1 < x2     (* same exponent, smaller coefficient *)
    || (x1 = x2 && tl1 << tl2)))  (* same leading term, compare tails *)

Every finite ordinal is less than every infinite one. Among infinite ordinals, we first compare leading exponents, then coefficients, then tails — exactly the lexicographic order on Cantor Normal Form.

Ordinal arithmetic

Ordinal addition is not commutative (1 + ω = ω ≠ ω + 1). ImandraX implements it faithfully:

let rec plus (x : t) (y : t) : t =
  match x, y with
  | Int x, Int y -> Int (x + y)
  | Int _, Cons _ -> y                          (* finite absorbed by infinite *)
  | Cons (a, x, tl), Int _ -> Cons (a, x, plus tl y)
  | Cons (a1, x1, tl1), Cons (a2, x2, tl2) ->
    if a1 << a2 then y                          (* smaller power absorbed *)
    else if a1 = a2 then Cons (a1, x1 + x2, tl2)  (* combine coefficients *)
    else Cons (a1, x1, plus tl1 y)              (* keep leading term *)

The shift operation multiplies an ordinal by ω^n, and is used internally to build lexicographic measures:

let rec shift (x : t) (n : t) : t =
  if n = Int 0 || x = Int 0 then x
  else match x with
  | Int x -> Cons (n, x, zero)           (* x becomes x·ω^n *)
  | Cons (a, x, tl) ->
    Cons (plus a n, x, shift tl n)        (* ω^a becomes ω^(a+n) *)

Automatic termination proofs

For common recursion patterns, ImandraX synthesizes termination measures automatically.

Structural recursion on datatypes

When a function recurses on structurally smaller subterms, termination is automatic:

(* Structural recursion on a list *)
let rec length = function
  | [] -> 0
  | _ :: xs -> 1 + length xs
(* Automatically proved terminating: xs is smaller than _ :: xs *)
 
(* Structural recursion on a tree *)
let rec size = function
  | Leaf _ -> 1
  | Node (l, r) -> size l + size r + 1
(* Automatically proved: l and r are smaller than Node (l, r) *)

Numeric recursion

When a numeric argument decreases toward a bound:

let rec sum n =
  if n <= 0 then 0
  else n + sum (n - 1)
(* Automatically proved: n - 1 < n when n > 0 *)

Guard conditions are critical

Using if n = 0 instead of if n <= 0 would be rejected: sum (-1) would call sum (-2), sum (-3), etc., never terminating. The guard n <= 0 ensures n is positive when recursing.

Lexicographic measures with `[@@adm]`

When termination depends on multiple arguments decreasing in a lexicographic order, use the [@@adm] annotation:

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):

Call ack (m-1) 1: m strictly decreases ✓
Call ack m (n-1): m stays the same, n strictly decreases ✓
Call ack (m-1) (ack m (n-1)): m strictly decreases ✓

Without [@@adm], ImandraX would reject this definition because no single argument decreases in all recursive calls.

Custom ordinal measures with `[@@measure]`

For more complex termination arguments, provide an explicit ordinal-valued 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)]

The measure Ordinal.of_int (List.length l) says: "prove that List.length decreases on each recursive call." ImandraX verifies this using a forward-chaining lemma about odds:

theorem odds_len x =
  x <> [] && List.tl x <> []
  ==>
  (List.length (odds x) [@trigger]) < List.length x
[@@by induct ~on_fun:[%id odds] ()] [@@fc]

The `Ordinal` module

The Ordinal module provides a full API for constructing ordinal-valued measures:

Function	Type	Description
`of_int`	`int -> t`	Natural number as an ordinal
`pair`	`t -> t -> t`	Lexicographic pair
`triple`	`t -> t -> t -> t`	Lexicographic triple
`quad`	`t -> t -> t -> t -> t`	Lexicographic quadruple
`of_list`	`t list -> t`	Lexicographic tuple of arbitrary length
`(+)` / `plus`	`t -> t -> t`	Ordinal addition (non-commutative)
`shift`	`t -> by:t -> t`	Multiply by ω^n
`(<<)`	`t -> t -> bool`	Strict ordinal ordering
`is_valid`	`t -> bool`	Check Cantor Normal Form validity
`zero`	`t`	The ordinal 0
`one`	`t`	The ordinal 1
`omega`	`t`	The ordinal ω
`omega_omega`	`t`	The ordinal ω^ω

Building measures

(* Measure: the length of a list *)
[@@measure Ordinal.of_int (List.length xs)]
 
(* Measure: lexicographic pair (m, n) *)
[@@measure Ordinal.(pair (of_int m) (of_int n))]
 
(* Measure: lexicographic triple *)
[@@measure Ordinal.(triple (of_int a) (of_int b) (of_int c))]
 
(* Equivalently, using of_list for arbitrary tuples *)
[@@measure Ordinal.of_list [
  Ordinal.of_int a;
  Ordinal.of_int b;
  Ordinal.of_int c
]]

How `pair` encodes lexicographic order

The pair function encodes a lexicographic pair (x, y) as a single ordinal by shifting x up by one power of ω:

let pair (x : t) (y : t) : t =
  match x with
  | Int x -> Cons (one, x + 1, y)         (* x·ω + y *)
  | Cons (a, x, _) -> Cons (plus a one, x, y)  (* x·ω^(a+1) + y *)

This ensures that decreasing the first component always produces a smaller ordinal, regardless of the second — which is exactly lexicographic ordering. The triple, quad, and of_list functions nest pair to extend this to arbitrary tuples.

Named ordinals

The prelude defines commonly needed ordinals:

let omega = of_list [ one; zero ]       (* ω *)
let omega_omega = shift omega omega     (* ω^ω *)

These can be useful in advanced termination arguments where the measure is not simply a natural number but an ordinal expression.

Termination and admissibility proofs

When termination cannot be proved automatically or with simple annotations, you may need to prove auxiliary lemmas. The termination proof obligation is itself a theorem that can be guided with tactics:

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]

Here [@@by auto] after the [@@adm] annotation tells ImandraX to use the waterfall to prove the termination obligation.

Mutually recursive functions

Mutually recursive functions defined with and must terminate together under a common measure:

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)

ImandraX proves both functions terminate together: in each cross-call, n strictly decreases.

Error messages

When ImandraX cannot prove termination, it provides specific guidance:

Error: unsupported: Validate: no measure provided,
and Imandra cannot guess any.
Are you sure this function is actually terminating?

Or more specific:

Error: problematic sub-call from `ack m n` to `ack m (n-1)`
under path `not (n <= 0) and not (m <= 0)`
is not decreasing (measured subset: `(m)`)

The second message identifies exactly which recursive call is problematic and what was measured, guiding you toward the right [@@adm] or [@@measure] annotation.