# Proving Program Termination¶

In this notebook, we'll walk through how Imandra can be used to analyse program termination. Along the way, we'll learn about soundness, conservative extensions, the Halting Problem, ordinals (up to $\epsilon_0$!) and well-founded orderings, path-guarded call-graphs, measure conjectures and more.

Before we dive into discussing (relatively deep!) aspects of mathematical logic, let's begin with a simple example. What happens when we try to define a non-terminating recursive function in Imandra?

In :
let rec f x = f x + 1

Out:
val f : 'a -> Z.t = <fun>

At jupyter cell 1:1,0--21
1 | let rec f x = f x + 1
^^^^^^^^^^^^^^^^^^^^^

Error[/server]:
unsupported: Validate: no measure provided, and Imandra cannot guess any.
Are you sure this function is actually terminating?
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
----------------------------------------------------------------------------
Context:
At jupyter cell 1:1,0--21
1 | let rec f x = f x + 1
^^^^^^^^^^^^^^^^^^^^^

Checking termination of function f


As we can see, Imandra rejects this definition of f given above. Contrast this with a definition of a function like map:

In :
let rec map f xs = match xs with
| [] -> []
| x :: xs -> f x :: map f xs

Out:
val map : ('a -> 'b) -> 'a list -> 'b list = <fun>

termination proof

### Termination proof

call map f_0 (List.tl xs) from map f_0 xs
original:map f_0 xs
sub:map f_0 (List.tl xs)
original ordinal:Ordinal.Int (_cnt xs)
sub ordinal:Ordinal.Int (_cnt (List.tl xs))
path:[xs <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.026s
details:
Expand
smt_stats:
 num checks: 8 arith-make-feasible: 8 arith-max-columns: 12 arith-conflicts: 1 rlimit count: 1696 arith-cheap-eqs: 2 mk clause: 12 datatype occurs check: 12 mk bool var: 52 arith-lower: 5 datatype splits: 1 decisions: 11 propagations: 12 arith-max-rows: 4 conflicts: 7 datatype accessor ax: 10 datatype constructor ax: 8 num allocs: 658506 final checks: 4 added eqs: 35 del clause: 4 arith eq adapter: 5 arith-upper: 5 memory: 5.08 max memory: 5.08
Expand
• start[0.026s]
let (_x_0 : int) = count.list (const 0) xs in
let (_x_1 : ty_1 list) = List.tl xs in
let (_x_2 : int) = count.list (const 0) _x_1 in
xs <> [] && _x_0 >= 0 && _x_2 >= 0
==> not (_x_1 <> [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : ty_1 list) = List.tl xs in let (_x_1 : int) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) xs in (not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((xs <> [] && _x_2 >= 0) && _x_1 >= 0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.list { Resolved_term.spec_idx = 0;… expansions:
• unroll
 expr: (|count.list { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: ty_1 -> int) (const (v.val 0)… expansions:
• unroll
 expr: (|count.list { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: ty_1 -> int) (const (v.val 0)… expansions:
• Unsat

Imandra accepts our function map and proves it terminating. Under the hood, Imandra uses ordinals in its termination analyses, beautiful mathematical objects representing equivalence classes of well-orderings. We'll discuss these more below! Before we do so, let's return to that function f that Imandra rejected.

## Inconsistent non-terminating functions¶

Imagine if Imandra allowed every possible recursive function to be admitted into its logic, even those that didn't terminate. If that were the case, we could easily define the following function:

let rec f x = f x + 1 (note the binding strength of f, i.e., this is equivalent to let rec f x = (f x) + 1)

With this function admitted, we could then use its defining equation f x = f x + 1 to derive a contradiction, e.g., by subtracting f x from both sides to derive 0 = 1:

f x       = f x + 1
f x - f x = f x + 1 - f x
0         = 1


This inconsistency arises because, actually, such a function f cannot "exist"!

You may be wondering: Why does consistency matter?

## Soundness, Consistency and Conservative Extensions¶

Imandra is both a programming language and a logic. A crucial property of a logic is soundness. For a logic to be sound, every theorem provable in the logic must be true. An unsound theorem prover would be of little use!

As we're developing programs and reasoning about them in Imandra, we're extending Imandra's logical world by defining types, functions, modules, and proving theorems. At any given time, this collection of all definitions and theorems is referred to as Imandra's current theory. It's important to ensure this current theory T is consistent, i.e., that there exists no statement P such that both P and (not P) are provable from T. If we weren't sure if T were consistent, then we would never know if a "theorem" was provable because it was true, or simply because T proves false (and false implies everything!).

Imandra's definitional principle is designed to ensure this consistency, by enforcing certain restrictions on our definitions. In the parlance of mathematical logic, Imandra's definitional principle ensures that every definitional extension of Imandra's current theory is a conservative extension.

There are two main rules Imandra enforces for ensuring consistency:

• Every defined type must be well-founded.
• Every defined function must be total (i.e., terminating on all possible inputs).

In this notebook, we'll focus on the latter: proving program termination!

## Termination ensures existence¶

Thankfully, a deep theorem of mathematical logic tells us that admitting terminating (also known as total) functions cannot lead us to inconsistency.

To admit a new function into Imandra's logic, Imandra must be able to prove that it always terminates. For most common patterns of recursion, Imandra is able to prove termination automatically. For others, users may need to give Imandra help in the form of hints and measures.

## Let's get our hands dirty¶

Let's define a few functions and see what this is like. First, let's observe that non-recursive functions are always admissible (provided we're not dealing with redefinition):

In :
let k x y z = if x > y then x + y else z - 1

Out:
val k : Z.t -> Z.t -> Z.t -> Z.t = <fun>


Let's now define some simple recursive functions, and observe how Imandra responds.

In :
let rec sum_lst = function
| [] -> 0
| x :: xs -> x + sum_lst xs

Out:
val sum_lst : Z.t list -> Z.t = <fun>

termination proof

### Termination proof

call sum_lst (List.tl _x) from sum_lst _x
original:sum_lst _x
sub:sum_lst (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[_x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.042s
details:
Expand
smt_stats:
 num checks: 8 arith-make-feasible: 18 arith-max-columns: 18 arith-conflicts: 2 rlimit count: 3725 mk clause: 25 datatype occurs check: 20 mk bool var: 80 arith-lower: 14 datatype splits: 1 decisions: 16 propagations: 26 arith-max-rows: 6 conflicts: 9 datatype accessor ax: 10 minimized lits: 1 datatype constructor ax: 9 num allocs: 2.48916e+06 final checks: 4 added eqs: 56 del clause: 11 arith eq adapter: 13 arith-upper: 16 memory: 5.15 max memory: 5.15
Expand
• start[0.042s]
let (_x_0 : int) = count.list mk_nat _x in
let (_x_1 : int list) = List.tl _x in
let (_x_2 : int) = count.list mk_nat _x_1 in
_x <> [] && _x_0 >= 0 && _x_2 >= 0
==> not (_x_1 <> [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int list) = List.tl _x in let (_x_1 : int) = count.list mk_nat _x_0 in let (_x_2 : int) = count.list mk_nat _x in (not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((_x <> [] && _x_2 >= 0) && _x_1 >= 0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.list { Resolved_term.spec_idx = 0;… expansions:
• unroll
 expr: (|count.list { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty … expansions:
• unroll
 expr: (|count.list { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty … expansions:
• Unsat
In :
sum_lst [1;2;3]

Out:
- : Z.t = 6

In :
let rec sum x =
if x <= 0 then 0
else x + sum(x-1)

Out:
val sum : Z.t -> Z.t = <fun>

termination proof

### Termination proof

call sum (x - 1) from sum x
original:sum x
sub:sum (x - 1)
original ordinal:Ordinal.Int (_cnt x)
sub ordinal:Ordinal.Int (_cnt (x - 1))
path:[not (x <= 0)]
proof:
detailed proof
ground_instances:1
definitions:0
inductions:0
search_time:
0.024s
details:
Expand
smt_stats:
 num checks: 3 arith-make-feasible: 5 arith-max-columns: 11 arith-conflicts: 1 rlimit count: 4795 mk clause: 5 datatype occurs check: 2 mk bool var: 17 arith-lower: 3 decisions: 2 arith-propagations: 3 propagations: 2 arith-bound-propagations-cheap: 3 arith-max-rows: 4 conflicts: 2 datatype accessor ax: 2 num allocs: 5.85386e+06 final checks: 1 added eqs: 6 del clause: 5 arith eq adapter: 2 arith-upper: 6 memory: 5.22 max memory: 7.77
Expand
• start[0.024s]
let (_x_0 : int) = if x >= 0 then x else 0 in
let (_x_1 : int) = x - 1 in
let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
not (x <= 0) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 <= 0 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: (x <= 0 || x <= 1) || Ordinal.( << ) (Ordinal.Int (if x >= 1 then (-1) + x else 0)) (Ordinal.Int (if x >= 0 then x else 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (ite (>= x_1723/server 1) (+ (- 1) x_1723/s… expansions:
• Unsat
In :
sum 5

Out:
- : Z.t = 15

In :
sum 100

Out:
- : Z.t = 5050


Out of curiosity, let's see what would happen if we made a mistake in our definition of sum above, by, e.g., using x = 0 as our test instead of x <= 0:

In :
let rec sum_oops x =
if x = 0 then 0
else x + sum_oops (x-1)

Out:
val sum_oops : Z.t -> Z.t = <fun>

At jupyter cell 9:1,0--62
1 | let rec sum_oops x =
2 |  if x = 0 then 0
3 |  else x + sum_oops (x-1)

Error[/server]:
unsupported: rejected definition for function sum_oops,
Imandra could not prove termination.
hint: problematic sub-call from sum_oops x
to sum_oops (x - 1)  under path not (x = 0) is not decreasing
(measured subset: (x))
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
----------------------------------------------------------------------------
Context:
At jupyter cell 9:1,0--62
1 | let rec sum_oops x =
2 |  if x = 0 then 0
3 |  else x + sum_oops (x-1)

Checking termination of function sum_oops


Note how Imandra rejects the definition, and tells us this is because it could not prove termination, in particular regarding the problematic recursive call sum_oops (x-1). Indeed, sum_oops does not terminate when x is negative!

# Structural Recursions¶

Structural recursions are easy for Imandra. For example, let's define a datatype of trees and a few functions on them. Imandra will fly on these termination proofs.

In :
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree

Out:
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree

In :
let rec size = function
| Leaf _     -> 1
| Node (a,b) -> size a + size b

Out:
val size : 'a tree -> Z.t = <fun>

termination proof

### Termination proof

call size (Destruct(Node, 0, _x)) from size _x
original:size _x
sub:size (Destruct(Node, 0, _x))
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (Destruct(Node, 0, _x)))
path:[not Is_a(Leaf, _x)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.027s
details:
Expand
smt_stats:
 num checks: 8 arith-assume-eqs: 2 arith-make-feasible: 23 arith-max-columns: 18 arith-conflicts: 2 rlimit count: 10322 mk clause: 29 datatype occurs check: 15 mk bool var: 80 arith-lower: 13 datatype splits: 3 decisions: 20 propagations: 18 interface eqs: 2 arith-max-rows: 5 conflicts: 6 datatype accessor ax: 13 datatype constructor ax: 11 num allocs: 1.96345e+07 final checks: 6 added eqs: 61 del clause: 22 arith eq adapter: 11 arith-upper: 19 memory: 7.84 max memory: 10.26
Expand
• start[0.027s]
let (_x_0 : int) = count.tree (const 0) _x in
let (_x_1 : ty_0 tree) = Destruct(Node, 0, _x) in
let (_x_2 : int) = count.tree (const 0) _x_1 in
let (_x_3 : bool) = Is_a(Leaf, _x_1) in
not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : ty_0 tree) = Destruct(Node, 0, _x) in let (_x_1 : int) = count.tree (const 0) _x_0 in let (_x_2 : int) = count.tree (const 0) _x in (Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: ty_0 -> int) (const (v.val 0)… expansions:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.tree { Resolved_term.spec_idx = 0;… expansions:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: ty_0 -> int) (const (v.val 0)… expansions:
• Unsat
call size (Destruct(Node, 1, _x)) from size _x
original:size _x
sub:size (Destruct(Node, 1, _x))
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (Destruct(Node, 1, _x)))
path:[not Is_a(Leaf, _x)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.028s
details:
Expand
smt_stats:
 num checks: 8 arith-make-feasible: 19 arith-max-columns: 17 arith-conflicts: 2 rlimit count: 8116 mk clause: 19 datatype occurs check: 14 mk bool var: 74 arith-lower: 13 arith-diseq: 1 datatype splits: 3 decisions: 19 propagations: 15 arith-max-rows: 4 conflicts: 7 datatype accessor ax: 13 datatype constructor ax: 11 num allocs: 1.31286e+07 final checks: 4 added eqs: 57 del clause: 12 arith eq adapter: 10 arith-upper: 14 memory: 7.8 max memory: 10.22
Expand
• start[0.028s]
let (_x_0 : int) = count.tree (const 0) _x in
let (_x_1 : ty_0 tree) = Destruct(Node, 1, _x) in
let (_x_2 : int) = count.tree (const 0) _x_1 in
let (_x_3 : bool) = Is_a(Leaf, _x_1) in
not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : ty_0 tree) = Destruct(Node, 1, _x) in let (_x_1 : int) = count.tree (const 0) _x_0 in let (_x_2 : int) = count.tree (const 0) _x in (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || Is_a(Leaf, _x_0)) || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: ty_0 -> int) (const (v.val 0)… expansions:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: ty_0 -> int) (const (v.val 0)… expansions:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.tree { Resolved_term.spec_idx = 0;… expansions:
• Unsat

For fun, let's ask Imandra to synthesize an int tree of size 5 for us:

In :
instance (fun (x : int tree) -> size x = 5)

Out:
- : Z.t tree -> bool = <fun>
module CX : sig val x : Z.t tree end

Instance (after 9 steps, 0.050s):
let x : int tree =
Node (Node (Leaf 7, Leaf 8), Node (Leaf 10, Node (Leaf 11, Leaf 9)))

Instance
proof attempt
ground_instances:9
definitions:0
inductions:0
search_time:
0.050s
details:
Expand
smt_stats:
 num checks: 19 arith-make-feasible: 62 arith-max-columns: 35 arith-conflicts: 8 rlimit count: 6752 arith-cheap-eqs: 4 mk clause: 149 datatype occurs check: 53 mk bool var: 563 arith-lower: 73 arith-diseq: 38 datatype splits: 20 decisions: 114 arith-propagations: 15 propagations: 292 arith-bound-propagations-cheap: 15 arith-max-rows: 13 conflicts: 18 datatype accessor ax: 105 minimized lits: 2 arith-bound-propagations-lp: 8 datatype constructor ax: 105 num allocs: 3.06713e+07 final checks: 17 added eqs: 606 del clause: 65 arith eq adapter: 80 arith-upper: 112 memory: 5.61 max memory: 10.26
Expand
• start[0.050s] size ( :var_0: ) = 5
• unroll
 expr: (size_1854/server x_1379/client) expansions:
• unroll
 expr: (size_1854/server (|get.Node.1_1853/server| x_1379/client)) expansions:
• unroll
 expr: (size_1854/server (|get.Node.0_1852/server| x_1379/client)) expansions:
• unroll
 expr: (size_1854/server (|get.Node.1_1853/server| (|get.Node.1_1853/server| x_1379/cli… expansions:
• unroll
 expr: (size_1854/server (|get.Node.0_1852/server| (|get.Node.1_1853/server| x_1379/cli… expansions:
• unroll
 expr: (size_1854/server (|get.Node.1_1853/server| (|get.Node.0_1852/server| x_1379/cli… expansions:
• unroll
 expr: (size_1854/server (|get.Node.0_1852/server| (|get.Node.0_1852/server| x_1379/cli… expansions:
• unroll
 expr: (size_1854/server (|get.Node.1_1853/server| (|get.Node.1_1853/server| … expansions:
• unroll
 expr: (size_1854/server (|get.Node.0_1852/server| (|get.Node.1_1853/server| … expansions:
• Sat (Some let x : int tree = Node (Node (Leaf (Z.of_nativeint (7n)), Leaf (Z.of_nativeint (8n))), Node (Leaf (Z.of_nativeint (10n)), Node (Leaf (Z.of_nativeint (11n)), Leaf (Z.of_nativeint (9n))))) )
In :
size CX.x

Out:
- : Z.t = 5


Cool! Let's now define a function to sum the leaves of an int tree:

In :
let rec sum_tree = function
| Leaf n     -> n
| Node (a,b) -> sum_tree a + sum_tree b

Out:
val sum_tree : Z.t tree -> Z.t = <fun>

termination proof

### Termination proof

call sum_tree (Destruct(Node, 0, _x)) from sum_tree _x
original:sum_tree _x
sub:sum_tree (Destruct(Node, 0, _x))
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (Destruct(Node, 0, _x)))
path:[not Is_a(Leaf, _x)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.022s
details:
Expand
smt_stats:
 num checks: 8 arith-make-feasible: 19 arith-max-columns: 17 arith-conflicts: 2 rlimit count: 11145 mk clause: 20 datatype occurs check: 15 mk bool var: 75 arith-lower: 13 arith-diseq: 1 datatype splits: 3 decisions: 19 propagations: 15 arith-max-rows: 4 conflicts: 7 datatype accessor ax: 13 datatype constructor ax: 11 num allocs: 5.01123e+07 final checks: 4 added eqs: 59 del clause: 13 arith eq adapter: 10 arith-upper: 14 memory: 5.67 max memory: 10.26
Expand
• start[0.022s]
let (_x_0 : int) = count.tree mk_nat _x in
let (_x_1 : int tree) = Destruct(Node, 0, _x) in
let (_x_2 : int) = count.tree mk_nat _x_1 in
let (_x_3 : bool) = Is_a(Leaf, _x_1) in
not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int) = count.tree mk_nat _x in let (_x_1 : int tree) = Destruct(Node, 0, _x) in let (_x_2 : int) = count.tree mk_nat _x_1 in (not ((not Is_a(Leaf, _x) && _x_0 >= 0) && _x_2 >= 0) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)) || Is_a(Leaf, _x_1) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty … expansions:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty … expansions:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.tree { Resolved_term.spec_idx = 0;… expansions:
• Unsat
call sum_tree (Destruct(Node, 1, _x)) from sum_tree _x
original:sum_tree _x
sub:sum_tree (Destruct(Node, 1, _x))
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (Destruct(Node, 1, _x)))
path:[not Is_a(Leaf, _x)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.025s
details:
Expand
smt_stats:
 num checks: 8 arith-make-feasible: 15 arith-max-columns: 17 arith-conflicts: 2 rlimit count: 8843 mk clause: 18 datatype occurs check: 14 mk bool var: 70 arith-lower: 8 datatype splits: 3 decisions: 14 propagations: 11 arith-max-rows: 4 conflicts: 6 datatype accessor ax: 13 datatype constructor ax: 11 num allocs: 4.02259e+07 final checks: 4 added eqs: 53 del clause: 11 arith eq adapter: 6 arith-upper: 11 memory: 5.69 max memory: 10.26
Expand
• start[0.025s]
let (_x_0 : int) = count.tree mk_nat _x in
let (_x_1 : int tree) = Destruct(Node, 1, _x) in
let (_x_2 : int) = count.tree mk_nat _x_1 in
let (_x_3 : bool) = Is_a(Leaf, _x_1) in
not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int tree) = Destruct(Node, 1, _x) in let (_x_1 : int) = count.tree mk_nat _x_0 in let (_x_2 : int) = count.tree mk_nat _x in (Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<_129/client| (|Ordinal.Int_114/client| (|count.tree { Resolved_term.spec_idx = 0;… expansions:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty … expansions:
• unroll
 expr: (|count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty … expansions:
• Unsat

Out of curiosity, are there any trees whose size is greater than 5 and equal to 3 times their sum?

In :
instance (fun x -> size x >= 5 && size x = 3 * sum_tree x)

Out:
- : Z.t tree -> bool = <fun>
module CX : sig val x : Z.t tree end

Instance (after 26 steps, 0.098s):
let x : int tree =
Node
(Node (Leaf 56867, Leaf (-46532)),
Node
(Node (Leaf (-54829), Leaf (-50521)), Node (Leaf 107403, Leaf (-12386))))

Instance
proof attempt
ground_instances:26
definitions:0
inductions:0
search_time:
0.098s
details:
Expand
smt_stats:
 arith-assume-eqs: 43 arith-make-feasible: 345 arith-max-columns: 102 arith-conflicts: 23 arith-gcd-calls: 17 datatype occurs check: 277 arith-lower: 452 arith-diseq: 197 datatype splits: 83 arith-propagations: 96 arith-patches-success: 9 propagations: 1963 arith-patches: 16 interface eqs: 43 arith-bound-propagations-cheap: 96 conflicts: 51 datatype constructor ax: 478 arith-gomory-cuts: 2 num allocs: 6.35025e+07 final checks: 95 added eqs: 3307 del clause: 542 arith-branch: 3 arith-gcd-conflict: 1 num checks: 53 arith-cube-calls: 2 arith-hnf-calls: 2 rlimit count: 34133 arith-cheap-eqs: 38 mk clause: 812 mk bool var: 2791 decisions: 976 arith-max-rows: 46 datatype accessor ax: 478 minimized lits: 4 arith-bound-propagations-lp: 8 arith eq adapter: 463 arith-upper: 643 time: 0.001 memory: 6.74 max memory: 10.26
Expand
• start[0.098s]
let (_x_0 : int) = size ( :var_0: ) in
_x_0 >= 5 && _x_0 = 3 * sum_tree ( :var_0: )
• unroll
 expr: (sum_tree_1381/client x_1386/client) expansions:
• unroll
 expr: (size_1953/server x_1386/client) expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.1_1952/server| x_1386/client)) expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.0_1951/server| x_1386/client)) expansions:
• unroll
 expr: (size_1953/server (|get.Node.1_1952/server| x_1386/client)) expansions:
• unroll
 expr: (size_1953/server (|get.Node.0_1951/server| x_1386/client)) expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.1_1952/server| (|get.Node.1_1952/server| x_1386/client))) expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.0_1951/server| (|get.Node.1_1952/server| x_1386/client))) expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.1_1952/server| (|get.Node.0_1951/server| x_1386/client))) expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.0_1951/server| (|get.Node.0_1951/server| x_1386/client))) expansions:
• unroll
 expr: (size_1953/server (|get.Node.1_1952/server| (|get.Node.1_1952/server| x_1386/cli… expansions:
• unroll
 expr: (size_1953/server (|get.Node.0_1951/server| (|get.Node.1_1952/server| x_1386/cli… expansions:
• unroll
 expr: (size_1953/server (|get.Node.1_1952/server| (|get.Node.0_1951/server| x_1386/cli… expansions:
• unroll
 expr: (size_1953/server (|get.Node.0_1951/server| (|get.Node.0_1951/server| x_1386/cli… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.1_1952/server| (|get.Node.1_1952/server| (|get.Node.1_1952/se… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.0_1951/server| (|get.Node.1_1952/server| (|get.Node.1_1952/se… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.1_1952/server| (|get.Node.0_1951/server| (|get.Node.1_1952/se… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.0_1951/server| (|get.Node.0_1951/server| (|get.Node.1_1952/se… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.1_1952/server| (|get.Node.1_1952/server| (|get.Node.0_1951/se… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.0_1951/server| (|get.Node.1_1952/server| (|get.Node.0_1951/se… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.1_1952/server| (|get.Node.0_1951/server| (|get.Node.0_1951/se… expansions:
• unroll
 expr: (sum_tree_1381/client (|get.Node.0_1951/server| (|get.Node.0_1951/server| (|get.Node.0_1951/se… expansions:
• unroll
 expr: (size_1953/server (|get.Node.1_1952/server| (|get.Node.1_1952/server| … expansions:
• unroll
 expr: (size_1953/server (|get.Node.0_1951/server| (|get.Node.1_1952/server| … expansions:
• unroll
 expr: (size_1953/server (|get.Node.1_1952/server| (|get.Node.0_1951/server| … expansions:
• unroll
 expr: (size_1953/server (|get.Node.0_1951/server| (|get.Node.0_1951/server| … expansions:
• Sat (Some let x : int tree = Node (Node (Leaf (Z.of_nativeint (56867n)), Leaf (Z.of_nativeint (-46532n))), Node (Node (Leaf (Z.of_nativeint (-54829n)), Leaf (Z.of_nativeint (-50521n))), Node (Leaf (Z.of_nativeint (107403n)), Leaf (Z.of_nativeint (-12386n))))) )

Yes! Let's compute with that counterexample to see:

In :
size CX.x

Out:
- : Z.t = 6

In :
3 * sum_tree CX.x

Out:
- : Z.t = 6 The Ackermann function (actually, family of functions) is famous for many reasons. It grows extremely quickly, so quickly that it can be proved to not be primitive recursive!

Here's an example definition:

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

It's worth it to study this function for a bit, to get a feel for why its recursion is tricky.

If we ask Imandra to admit it, we find out that it's tricky for Imandra, too!

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

Out:
val ack : Z.t -> Z.t -> Z.t = <fun>

termination proof

### Termination proof

call ack (m - 1) 1 from ack m n
original:ack m n
sub:ack (m - 1) 1
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt (m - 1)); Ordinal.Int (_cnt 1)]
path:[n <= 0 && not (m <= 0)]
proof:
detailed proof
ground_instances:5
definitions:0
inductions:0
search_time:
0.034s
details:
Expand
smt_stats:
 num checks: 12 arith-make-feasible: 22 arith-max-columns: 20 arith-conflicts: 1 rlimit count: 57668 arith-cheap-eqs: 4 mk clause: 55 datatype occurs check: 51 mk bool var: 136 arith-lower: 19 arith-diseq: 16 datatype splits: 3 decisions: 75 arith-propagations: 13 propagations: 71 arith-bound-propagations-cheap: 13 arith-max-rows: 7 conflicts: 14 datatype accessor ax: 23 datatype constructor ax: 13 num allocs: 1.34813e+08 final checks: 7 added eqs: 146 del clause: 21 arith eq adapter: 15 arith-upper: 14 memory: 6.37 max memory: 10.26
Expand
• start[0.034s]
let (_x_0 : int) = m - 1 in
let (_x_1 : bool) = 1 <= 0 in
let (_x_2 : bool) = not (_x_0 <= 0) in
let (_x_3 : bool) = not (not _x_1 && _x_2) in
n <= 0
&& not (m <= 0)
&& (if m >= 0 then m else 0) >= 0
&& (if n >= 0 then n else 0) >= 0
&& (if _x_0 >= 0 then _x_0 else 0) >= 0
&& (if 1 >= 0 then 1 else 0) >= 0
==> not (_x_1 && _x_2) && _x_3 && _x_3
|| Ordinal.( << ) (if … <> [] then … else …)
(if … <> [] then … else …)
• ###### simplify
 into: let (_x_0 : Ordinal.t) = Ordinal.Int 1 in (m <= 1 || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_0) _x_0) (Ordinal.plus (Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) _x_0) (Ordinal.Int (if n >= 0 then n else 0)))) || not (n <= 0 && not (m <= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 0) m_2025/server 0)) … expansions:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 1) (+ (- 1) m_202… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• Unsat
call ack (m - 1) (ack m (n - 1)) from ack m n
original:ack m n
sub:ack (m - 1) (ack m (n - 1))
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt (m - 1)); Ordinal.Int (_cnt (ack m (n - 1)))]
path:[not (n <= 0) && not (m <= 0)]
proof:
detailed proof
ground_instances:5
definitions:0
inductions:0
search_time:
0.032s
details:
Expand
smt_stats:
 num checks: 12 arith-assume-eqs: 2 arith-make-feasible: 31 arith-max-columns: 24 arith-conflicts: 1 rlimit count: 52015 arith-cheap-eqs: 2 mk clause: 86 datatype occurs check: 60 mk bool var: 158 arith-lower: 19 arith-diseq: 8 datatype splits: 2 decisions: 71 arith-propagations: 19 propagations: 119 interface eqs: 2 arith-bound-propagations-cheap: 19 arith-max-rows: 9 conflicts: 15 datatype accessor ax: 24 datatype constructor ax: 13 num allocs: 1.15443e+08 final checks: 9 added eqs: 141 del clause: 33 arith eq adapter: 17 arith-upper: 40 memory: 6.4 max memory: 10.26
Expand
• start[0.032s]
let (_x_0 : int) = m - 1 in
let (_x_1 : int) = ack m (n - 1) in
let (_x_2 : bool) = _x_1 <= 0 in
let (_x_3 : bool) = not (_x_0 <= 0) in
let (_x_4 : bool) = not (not _x_2 && _x_3) in
not (n <= 0)
&& not (m <= 0)
&& (if m >= 0 then m else 0) >= 0
&& (if n >= 0 then n else 0) >= 0
&& (if _x_0 >= 0 then _x_0 else 0) >= 0
&& (if _x_1 >= 0 then _x_1 else 0) >= 0
==> not (_x_2 && _x_3) && _x_4 && _x_4
|| Ordinal.( << ) (if … <> [] then … else …)
(if … <> [] then … else …)
• ###### simplify
 into: let (_x_0 : Ordinal.t) = Ordinal.Int 1 in let (_x_1 : int) = ack m … in let (_x_2 : bool) = _x_1 <= 0 in let (_x_3 : bool) = not (m <= 1) in (not (not (n <= 0) && not (m <= 0)) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_0) (Ordinal.Int (if _x_1 >= 0 then _x_1 else 0))) (Ordinal.plus (Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) _x_0) (Ordinal.Int (if n >= 0 then n else 0)))) || not (_x_2 && _x_3) && not (not _x_2 && _x_3) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 0) m_2025/server 0)) … expansions:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 1) (+ (- 1) m_202… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• Unsat
call ack m (n - 1) from ack m n
original:ack m n
sub:ack m (n - 1)
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt (n - 1))]
path:[not (n <= 0) && not (m <= 0)]
proof:
detailed proof
ground_instances:9
definitions:0
inductions:0
search_time:
0.050s
details:
Expand
smt_stats:
 num checks: 19 arith-make-feasible: 18 arith-max-columns: 39 arith-conflicts: 1 rlimit count: 45649 arith-cheap-eqs: 6 mk clause: 101 datatype occurs check: 196 mk bool var: 264 arith-lower: 12 arith-diseq: 3 datatype splits: 24 decisions: 159 arith-propagations: 3 propagations: 104 arith-bound-propagations-cheap: 3 arith-max-rows: 17 conflicts: 18 datatype accessor ax: 49 arith-bound-propagations-lp: 2 datatype constructor ax: 32 num allocs: 9.66145e+07 final checks: 16 added eqs: 230 del clause: 60 arith eq adapter: 12 arith-upper: 14 memory: 6.46 max memory: 10.26
Expand
• start[0.050s]
let (_x_0 : bool) = not (m <= 0) in
let (_x_1 : bool) = (if m >= 0 then m else 0) >= 0 in
let (_x_2 : int) = n - 1 in
let (_x_3 : bool) = _x_2 <= 0 in
let (_x_4 : bool) = not (not _x_3 && _x_0) in
not (n <= 0)
&& _x_0
&& _x_1
&& (if n >= 0 then n else 0) >= 0
&& _x_1 && (if _x_2 >= 0 then _x_2 else 0) >= 0
==> not (_x_3 && _x_0) && _x_4 && _x_4
|| Ordinal.( << ) (if … <> [] then … else …)
(if … <> [] then … else …)
• ###### simplify
 into: let (_x_0 : Ordinal.t) = Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) (Ordinal.Int 1) in let (_x_1 : bool) = n <= 1 in let (_x_2 : bool) = not (m <= 0) in (Ordinal.( << ) (Ordinal.plus _x_0 (Ordinal.Int (if n >= 1 then … else 0))) (Ordinal.plus _x_0 (Ordinal.Int (if n >= 0 then n else 0))) || not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || not (not (n <= 0) && _x_2) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 0) m_2025/server 0)) … expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|get.Ordinal.Cons.2_2007/server| (|Ordinal.Int_114/client| (… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• Unsat

Imandra tells us that it's unable to prove termination in the particular path that goes from ack m n to ack m (n-1). Imandra further tells us that it tried to prove termination in this case using a measured subset of the arguments of ack containing only m.

Why does ack terminate, and how can we explain this to Imandra?

If we think about it for a little bit, we realise that ack terminates because its pair of arguments decreases lexicographically in its recursive calls. From the perspective of ordinals, the arguments of the recursive calls decrease along the ordinal $\omega^2$.

## Lexicographic termination (up to $\omega^\omega$)¶

Lexicographic termination is so common, there's a special way we can tell Imandra to use it.

This is done with the @@adm ("admission") attribute.

We can tell Imandra to prove ack terminating by using a lexicographic order on (m,n) in the following way:

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

Out:
val ack : Z.t -> Z.t -> Z.t = <fun>

termination proof

### Termination proof

call ack (m - 1) 1 from ack m n
original:ack m n
sub:ack (m - 1) 1
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt (m - 1)); Ordinal.Int (_cnt 1)]
path:[n <= 0 && not (m <= 0)]
proof:
detailed proof
ground_instances:5
definitions:0
inductions:0
search_time:
0.034s
details:
Expand
smt_stats:
 num checks: 12 arith-make-feasible: 22 arith-max-columns: 20 arith-conflicts: 1 rlimit count: 57668 arith-cheap-eqs: 4 mk clause: 55 datatype occurs check: 51 mk bool var: 136 arith-lower: 19 arith-diseq: 16 datatype splits: 3 decisions: 75 arith-propagations: 13 propagations: 71 arith-bound-propagations-cheap: 13 arith-max-rows: 7 conflicts: 14 datatype accessor ax: 23 datatype constructor ax: 13 num allocs: 1.34813e+08 final checks: 7 added eqs: 146 del clause: 21 arith eq adapter: 15 arith-upper: 14 memory: 6.37 max memory: 10.26
Expand
• start[0.034s]
let (_x_0 : int) = m - 1 in
let (_x_1 : bool) = 1 <= 0 in
let (_x_2 : bool) = not (_x_0 <= 0) in
let (_x_3 : bool) = not (not _x_1 && _x_2) in
n <= 0
&& not (m <= 0)
&& (if m >= 0 then m else 0) >= 0
&& (if n >= 0 then n else 0) >= 0
&& (if _x_0 >= 0 then _x_0 else 0) >= 0
&& (if 1 >= 0 then 1 else 0) >= 0
==> not (_x_1 && _x_2) && _x_3 && _x_3
|| Ordinal.( << ) (if … <> [] then … else …)
(if … <> [] then … else …)
• ###### simplify
 into: let (_x_0 : Ordinal.t) = Ordinal.Int 1 in (m <= 1 || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_0) _x_0) (Ordinal.plus (Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) _x_0) (Ordinal.Int (if n >= 0 then n else 0)))) || not (n <= 0 && not (m <= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 0) m_2025/server 0)) … expansions:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 1) (+ (- 1) m_202… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• Unsat
call ack (m - 1) (ack m (n - 1)) from ack m n
original:ack m n
sub:ack (m - 1) (ack m (n - 1))
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt (m - 1)); Ordinal.Int (_cnt (ack m (n - 1)))]
path:[not (n <= 0) && not (m <= 0)]
proof:
detailed proof
ground_instances:5
definitions:0
inductions:0
search_time:
0.032s
details:
Expand
smt_stats:
 num checks: 12 arith-assume-eqs: 2 arith-make-feasible: 31 arith-max-columns: 24 arith-conflicts: 1 rlimit count: 52015 arith-cheap-eqs: 2 mk clause: 86 datatype occurs check: 60 mk bool var: 158 arith-lower: 19 arith-diseq: 8 datatype splits: 2 decisions: 71 arith-propagations: 19 propagations: 119 interface eqs: 2 arith-bound-propagations-cheap: 19 arith-max-rows: 9 conflicts: 15 datatype accessor ax: 24 datatype constructor ax: 13 num allocs: 1.15443e+08 final checks: 9 added eqs: 141 del clause: 33 arith eq adapter: 17 arith-upper: 40 memory: 6.4 max memory: 10.26
Expand
• start[0.032s]
let (_x_0 : int) = m - 1 in
let (_x_1 : int) = ack m (n - 1) in
let (_x_2 : bool) = _x_1 <= 0 in
let (_x_3 : bool) = not (_x_0 <= 0) in
let (_x_4 : bool) = not (not _x_2 && _x_3) in
not (n <= 0)
&& not (m <= 0)
&& (if m >= 0 then m else 0) >= 0
&& (if n >= 0 then n else 0) >= 0
&& (if _x_0 >= 0 then _x_0 else 0) >= 0
&& (if _x_1 >= 0 then _x_1 else 0) >= 0
==> not (_x_2 && _x_3) && _x_4 && _x_4
|| Ordinal.( << ) (if … <> [] then … else …)
(if … <> [] then … else …)
• ###### simplify
 into: let (_x_0 : Ordinal.t) = Ordinal.Int 1 in let (_x_1 : int) = ack m … in let (_x_2 : bool) = _x_1 <= 0 in let (_x_3 : bool) = not (m <= 1) in (not (not (n <= 0) && not (m <= 0)) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_0) (Ordinal.Int (if _x_1 >= 0 then _x_1 else 0))) (Ordinal.plus (Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) _x_0) (Ordinal.Int (if n >= 0 then n else 0)))) || not (_x_2 && _x_3) && not (not _x_2 && _x_3) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 0) m_2025/server 0)) … expansions:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 1) (+ (- 1) m_202… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• Unsat
call ack m (n - 1) from ack m n
original:ack m n
sub:ack m (n - 1)
original ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
sub ordinal:Ordinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt (n - 1))]
path:[not (n <= 0) && not (m <= 0)]
proof:
detailed proof
ground_instances:9
definitions:0
inductions:0
search_time:
0.050s
details:
Expand
smt_stats:
 num checks: 19 arith-make-feasible: 18 arith-max-columns: 39 arith-conflicts: 1 rlimit count: 45649 arith-cheap-eqs: 6 mk clause: 101 datatype occurs check: 196 mk bool var: 264 arith-lower: 12 arith-diseq: 3 datatype splits: 24 decisions: 159 arith-propagations: 3 propagations: 104 arith-bound-propagations-cheap: 3 arith-max-rows: 17 conflicts: 18 datatype accessor ax: 49 arith-bound-propagations-lp: 2 datatype constructor ax: 32 num allocs: 9.66145e+07 final checks: 16 added eqs: 230 del clause: 60 arith eq adapter: 12 arith-upper: 14 memory: 6.46 max memory: 10.26
Expand
• start[0.050s]
let (_x_0 : bool) = not (m <= 0) in
let (_x_1 : bool) = (if m >= 0 then m else 0) >= 0 in
let (_x_2 : int) = n - 1 in
let (_x_3 : bool) = _x_2 <= 0 in
let (_x_4 : bool) = not (not _x_3 && _x_0) in
not (n <= 0)
&& _x_0
&& _x_1
&& (if n >= 0 then n else 0) >= 0
&& _x_1 && (if _x_2 >= 0 then _x_2 else 0) >= 0
==> not (_x_3 && _x_0) && _x_4 && _x_4
|| Ordinal.( << ) (if … <> [] then … else …)
(if … <> [] then … else …)
• ###### simplify
 into: let (_x_0 : Ordinal.t) = Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) (Ordinal.Int 1) in let (_x_1 : bool) = n <= 1 in let (_x_2 : bool) = not (m <= 0) in (Ordinal.( << ) (Ordinal.plus _x_0 (Ordinal.Int (if n >= 1 then … else 0))) (Ordinal.plus _x_0 (Ordinal.Int (if n >= 0 then n else 0))) || not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || not (not (n <= 0) && _x_2) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>= m_2025/server 0) m_2025/server 0)) … expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|get.Ordinal.Cons.2_2007/server| (|Ordinal.Int_114/client| (… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift_184/client| (|Ordinal.Int_114/client| (ite (>… expansions:
• Unsat

Success! You may enjoy walking through Imandra's termination proof presented in the document above.

# Measures and Ordinals¶

If a lexicographic ordering isn't sufficient to prove termination for your function, you may need to construct a custom measure function.

A measure function is ordinal valued, meaning it returns a value of type Ordinal.t.

Imandra's Ordinal module comes with helpful tools for constructing ordinals.

Let's view its contents with the #show directive:

In :
#show Ordinal

Out:
module Ordinal :
sig
type t = Int of Z.t | Cons of t * Z.t * t
val pp : Format.formatter -> t -> unit
val of_int : Z.t -> t
val ( ~$) : Z.t -> t val ( << ) : t -> t -> bool val plus : t -> t -> t val simple_plus : t -> t -> t val ( + ) : t -> t -> t val of_list : t list -> t val pair : t -> t -> t val triple : t -> t -> t -> t val quad : t -> t -> t -> t -> t val shift : t -> by:t -> t val is_valid : t -> bool val is_valid_rec : t -> bool val zero : t val one : t val omega : t val omega_omega : t end  Even though ordinals like$\omega$are infinite, we may still compute with them in Imandra. In : Ordinal.omega  Out: - : Ordinal.t = ω  In : Ordinal.(omega + omega)  Out: - : Ordinal.t = 2·ω  In : let o1 = Ordinal.(omega + omega_omega + shift omega ~by:(omega + one))  Out: val o1 : Ordinal.t = ω^(ω + 1)  In : Ordinal.(o1 << omega_omega)  Out: - : bool = false  Ordinals are fundamental to program termination because they represent well-founded orderings (well-orders). If we can prove that a function's recursive calls always get smaller with respect to some well-founded ordering, then we know the function will always terminate. The fundamental well-founded relation in Imandra is Ordinal.(<<). This is the strict, well-founded ordering relation on the ordinals up to$\epsilon_0\$: Let's consider an example famous recursive function that we can't admit with a lexicographic order and see how we can write our own measure function and communicate it to Imandra.

Consider the following function left_pad:

let rec left_pad c n xs =
if List.length xs >= n then
xs
else
left_pad c n (c :: xs)

If we give this function to Imandra without any hints, it will not be able to prove it terminating.

In :
let rec left_pad c n xs =
if List.length xs >= n then
xs
else
left_pad c n (c :: xs)

Out:
val left_pad : 'a -> Z.t -> 'a list -> 'a list = <fun>

At jupyter cell 25:1,0--96
1 | let rec left_pad c n xs =
2 |   if List.length xs >= n then
3 |     xs
4 |   else
5 |     left_pad c n (c :: xs)

Error[/server]:
unsupported: rejected definition for function left_pad,
Imandra could not prove termination.
hint: problematic sub-call from left_pad c n xs
to left_pad c n (c :: xs)  under path
not (List.length xs >= n) is not decreasing
(measured subset: (xs))
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
----------------------------------------------------------------------------
Context:
At jupyter cell 25:1,0--96
1 | let rec left_pad c n xs =
2 |   if List.length xs >= n then
3 |     xs
4 |   else
5 |     left_pad c n (c :: xs)

Checking termination of function left_pad


Why does this function terminate? If we think about it, we can realise that it terminates because in each recursive call, the quantity n - List.length xs is getting smaller. Moreover, under the guards governing the recursive calls, this quantity is always non-negative. So, let's construct an ordinal-valued measure function to express this:

In :
let left_pad_measure n xs =
Ordinal.of_int (n - List.length xs)

Out:
val left_pad_measure : Z.t -> 'a list -> Ordinal.t = <fun>


We can compute with this function, to really see it does what we want:

In :
left_pad_measure 5 [1;2;3]

Out:
- : Ordinal.t = 2


Finally, we can give it to Imandra as the measure to use in proving left_pad terminates:

In :
let rec left_pad c n xs =
if List.length xs >= n then
xs
else
left_pad c n (c :: xs)

Out:
val left_pad : 'a -> Z.t -> 'a list -> 'a list = <fun>

termination proof

### Termination proof

call left_pad c n (c :: xs) from left_pad c n xs
sub:left_pad c n (c :: xs)
sub ordinal:left_pad_measure n (c :: xs)
path:[not (List.length xs >= n)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.032s
details:
Expand
smt_stats:
 num checks: 7 arith-assume-eqs: 2 arith-make-feasible: 11 arith-max-columns: 19 arith-conflicts: 1 rlimit count: 62477 arith-cheap-eqs: 2 mk clause: 20 datatype occurs check: 19 mk bool var: 51 arith-lower: 9 datatype splits: 3 decisions: 12 arith-propagations: 2 propagations: 11 interface eqs: 2 arith-bound-propagations-cheap: 2 arith-max-rows: 9 conflicts: 4 datatype accessor ax: 7 datatype constructor ax: 4 num allocs: 1.67169e+08 final checks: 8 added eqs: 31 del clause: 13 arith eq adapter: 6 arith-upper: 11 memory: 8.92 max memory: 10.26
Expand
• start[0.032s]
let (_x_0 : int) = List.length xs in
let (_x_1 : int) = n - _x_0 in
let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
let (_x_3 : int) = List.length (… :: xs) in
let (_x_4 : int) = n - _x_3 in
let (_x_5 : int) = if _x_4 >= 0 then _x_4 else 0 in
not (_x_0 >= n) && _x_2 >= 0 && _x_5 >= 0
==> _x_3 >= n || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_2)
• ###### simplify
 into: let (_x_0 : int) = List.length (… :: xs) in let (_x_1 : int) = List.length xs in let (_x_2 : int) = n + (-1) * _x_0 in let (_x_3 : int) = n + (-1) * _x_1 in (_x_0 >= n || _x_1 >= n) || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0)) (Ordinal.Int (if _x_3 >= 0 then _x_3 else 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (+ n_2263/server (* (- 1) (|List.length_2258/server| (|::|… expansions:
• unroll
 expr: (|List.length_2258/server| xs_2264/server) expansions:
• unroll
 expr: (|List.length_2258/server| (|::| c_2262/server xs_2264/server)) expansions:
• Unsat

Success! Note also how we only used two of left_pad's three arguments in our measure. In general, economical measures are good, as they give us smaller measured subsets, which allow us to simplify more symbolic instances of our recursive functions during proof search. Moreover, they also affect how Imandra is able to use its functional induction (a.k.a. recursion induction) schemes.

We can find out the measured subset (and much other data) about our functions through the #history directive. It's also available with the handy alias #h:

In :
#history left_pad

Out:

iml:
definition
fun (c : 'b) ->
fun (n : int) ->
fun (xs : 'b list) ->
if List.length xs >= n then xs else left_pad c n (c :: xs)
def:
type:'b -> int -> 'b list -> 'b list
recursive:true
def-depth:4
def-ty-depth:2
call signature:left_pad (c : 'b) (n : int) (xs : 'b list)
measured subset:[n; xs]
parametric:true
validated:in 0.000s
location:At jupyter cell 28:1,0--130 1 | let rec left_pad c n xs = 2 | if List.length xs >= n then 3 | xs 4 | else 5 | left_pad c n (c :: xs) 6 | [@@measure left_pad_measure n xs]
sub-function(s):
Expand
 name: measure_fun.left_pad type: int -> 'a list -> Ordinal.t recursive: false def-depth: 6 def-ty-depth: 2 call signature: measure_fun.left_pad (n : int) (xs : 'a list) body: left_pad_measure n xs parametric: true validated: in 0.001s location: At jupyter cell 28:1,0--130 1 | let rec left_pad c n xs = 2 | if List.length xs >= n then 3 | xs 4 | else 5 | left_pad c n (c :: xs) 6 | [@@measure left_pad_measure n xs]
hashes: