Basic

Since IML serves as both a programming language and a logic, function termination must be provable:

  • Every let rec definition triggers a termination proving task. All recursive functions need to be admitted before they can be used. The admission includes proving termination.
  • For common recursion patterns, termination is proven automatically. When no custom measure is given, ImandraX's heuristics pick a single argument for the measure.
  • When default measure is not sufficient, provide explicit termination measures using [@@measure ...] or [@@adm ...].

Ordinals in Termination Proofs: Termination measures in IML must return values of type Ordinal.t. This type represents ordinals up to ε₀ in Cantor Normal Form, providing a well-founded ordering essential for proving termination. When defining measures, you can use functions like Ordinal.of_int to convert integers to ordinals, or construct more complex ordinals for nested recursion.

Examples and Recipes

Quick Decision Tree:

Is your function rejected for termination?
├─ Does it use structural recursion on datatypes?
│   └─ Usually automatic, if the default measure picks the shrinking argument (see below).
├─ Does it have simple decreasing integer arguments?
│   └─ Usually automatic, if the default measure picks the decreasing argument (see below).
├─ Do arguments decrease lexicographically?
│   └─ Use `[@@adm arg1, arg2, ...]`
└─ Need custom measure?
    └─ Use `[@@measure fn arg1 arg2 ...]`

Example: Rely on Default Measure

ImandraX handles these automatically:

Structural recursion on lists:

let rec sum_list = function
  | [] -> 0
  | x :: xs -> x + sum_list xs
(* Works automatically *)

Simple decreasing integers:

let rec countdown x =
  if x <= 0 then 0
  else x + countdown (x - 1)
(* Works automatically *)

How the default measure is chosen

With no [@@measure]/[@@adm], ImandraX measures a single argument: the first one appearing in a condition that leads to a recursive call (a match, an if, or a guard like x = s && f ...). No other argument is tried. So an earlier argument in a guard can take the place of a later one that actually shrinks:

(* Fails: measure is on `s`, not `tr`. Admits with `[@@adm tr]`. *)
let rec chain (s : int) (tr : int list) : bool =
  match tr with
  | [] -> true
  | i :: rest -> i = s && chain (i + 1) rest

An int argument is measured as max 0 x, so a base case of x <= 0 admits but x = 0 does not.

Advanced: When the default fails ("Goal is counter-satisfiable"), the chosen argument is visible in the subgoal's << conclusion, e.g. << (Int if s' >= 0 then s' else 0) (Int if s >= 0 then s else 0).

Example: Lexicographic Ordering with [@@adm]

Use when multiple arguments decrease in order:

let rec ackermann m n =
  if m <= 0 then n + 1
  else if n <= 0 then ackermann (m - 1) 1
  else ackermann (m - 1) (ackermann m (n - 1))
[@@adm m, n]
  • [@@adm m, n] tells ImandraX: "m decreases first; when m stays the same, n decreases."
  • When to use:
    • Multiple recursive calls with different decreasing patterns
    • Nested recursion (like Ackermann)
    • Arguments that decrease in a specific priority order

Example: Custom Measure with [@@measure]

(* First define a measure function returning `Ordinal.t` *)
let left_pad_measure n xs =
  Ordinal.of_int (n - List.length xs)
 
let rec left_pad c n xs =
  if List.length xs >= n then xs
  else left_pad c n (c :: xs)
[@@measure left_pad_measure n xs]
(* Then attach the measure to the function *)

Here n - List.length xs decreases with each recursive call and stays non-negative; Ordinal.of_int maps it to an ordinal, giving ImandraX the well-founded ordering it needs.

Gotchas

  • Measure function must return Ordinal.t
  • [@@measure ...] works only on top-level functions (not those defined inside another function). In addition, it's generally discouraged to define nested recursive functions in IML.
  • Refer to [[reference/ordinal.md]] for more details on the Ordinal module (constants, combinators, etc.).

Idioms

Recurring measure/termination patterns from expert proof corpora:

max 0 e guard. Ints can be negative; ordinals can't. Whenever the decreasing quantity could dip below zero on bad inputs, guard it — this is the standard idiom, used on nearly every int-recursion:

let rec real_pow (g : real) (n : int) : real =
  if n <= 0 then 1.0 else g *. real_pow g (n - 1)
[@@measure Ordinal.of_int (max 0 n)]

Upward recursion. Measure by distance to the bound: [@@measure Ordinal.of_int (List.length l + 1 - k)] for a function recursing on k + 1 up to List.length l.

Lexicographic measures. Ordinal.pair (see ordinal.md): [@@measure Ordinal.pair (Ordinal.of_int (List.length p)) (Ordinal.of_int (List.length cands))].

Lemma-assisted admission ([@@by] on the definition). A [@@by] attached to a let rec is the tactic for its termination proof obligation. When the decrease isn't syntactic, prove supporting lemmas first and [%use] them in the admission script:

lemma len_remove_lt x p = List.mem x p ==> List.length (remove x p) < List.length p
[@@by auto]
 
let rec perms_aux (candidates : int list) (p : int list) : int list list = ...
[@@measure Ordinal.pair (Ordinal.of_int (List.length p))
                        (Ordinal.of_int (List.length candidates))]
[@@by [%use len_remove_lt (List.hd candidates) p] @> simplify () @>>| auto]

This is how functions with data-dependent decrease (e.g. recursing on n / d) get admitted: the expert corpus admits prime_factors with a six-[%use] termination script.

Defensive unreachable guards. When the decrease only holds under invariants the admission check can't see, add an early-return branch that makes termination trivial, and refute that branch later in the correctness proof:

let rec descent_loop (m : int) (q : sq4) : sq4 =
  let mp = next_m m q in
  if mp <= 0 || mp >= m then q   (* unreachable under correct hypotheses *)
  else descent_loop mp (descent_q m q)
[@@measure Ordinal.of_int (max 0 m)]

The correctness theorem then proves mp is always in range, so the guard branch never fires on valid inputs. This cleanly separates "it terminates" from "it's correct". (Similarly: guard inputs, e.g. gcd returning 0 on negatives.)

Previous← task-and-artifacts
Nexttimeouts →