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>
File "jupyter cell 1", line 1, characters 0-21:
Error: 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/

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
originalmap f_0 xs
submap f_0 (List.tl xs)
original ordinalOrdinal.Int (Ordinal.count xs)
sub ordinalOrdinal.Int (Ordinal.count (List.tl xs))
path[not (xs = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 1817 mk clause 3 datatype occurs check 21 mk bool var 50 arith assert upper 5 datatype splits 3 decisions 7 arith add rows 7 propagations 2 conflicts 7 arith fixed eqs 4 datatype accessor ax 5 arith conflicts 1 datatype constructor ax 8 num allocs 933581 final checks 6 added eqs 33 del clause 1 arith eq adapter 3 memory 5.9 max memory 5.9
Expand
• start[0.014s]
not (xs = []) && Ordinal.count xs >= 0 && Ordinal.count (List.tl xs) >= 0
==> List.tl xs = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl xs)))
(Ordinal.Int (Ordinal.count xs))
• simplify
 into (not ((not (xs = []) && Ordinal.count xs >= 0) && Ordinal.count (List.tl xs) >= 0) || List.tl xs = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl xs))) (Ordinal.Int (Ordinal.count xs)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_1 list_1112| … expansions
• unroll
 expr (|count_ty_1 list_1112| (|get.::.1_1095| xs_1103)) expansions
• unroll
 expr (|count_ty_1 list_1112| xs_1103) expansions
• unsat
(let ((a!1 (= (|count_ty_1 list_1112| xs_1103)
(+ 1 (|count_ty_1 list_1112| (|get.…

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 : int -> int -> 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
originalsum_lst _x
subsum_lst (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 8 arith assert lower 17 arith pivots 10 rlimit count 2400 mk clause 19 datatype occurs check 21 mk bool var 79 arith assert upper 12 datatype splits 3 decisions 13 arith add rows 16 arith bound prop 1 propagations 13 conflicts 9 arith fixed eqs 7 datatype accessor ax 5 arith conflicts 2 datatype constructor ax 8 num allocs 2.89897e+06 final checks 6 added eqs 47 del clause 7 arith eq adapter 10 memory 9.49 max memory 9.49
Expand
• start[0.014s]
not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> List.tl _x = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• simplify
 into (not ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || List.tl _x = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int list_1131| (… expansions
• unroll
 expr (|count_int list_1131| (|get.::.1_1121| _x_1122)) expansions
• unroll
 expr (|count_int list_1131| _x_1122) expansions
• unsat
(let ((a!1 (>= (ite (>= (|get.::.0_1120| _x_1122) 0)
(|get.::.0_1120| _x_1122)
…

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 : int -> Z.t = <fun>
termination proof

Termination proof

call sum (x - 1) from sum x
originalsum x
subsum (x - 1)
original ordinalOrdinal.Int (if x >= 0 then x else 0)
sub ordinalOrdinal.Int (if (x - 1) >= 0 then x - 1 else 0)
path[not (x <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.010s
details
Expand
smt_stats
 num checks 3 arith assert lower 8 arith pivots 2 rlimit count 1027 mk clause 4 datatype occurs check 2 mk bool var 20 arith assert upper 3 decisions 2 arith add rows 3 propagations 2 conflicts 2 arith fixed eqs 2 datatype accessor ax 2 arith conflicts 1 num allocs 7.57657e+06 final checks 1 added eqs 6 del clause 4 arith eq adapter 2 memory 9.91 max memory 9.91
Expand
• start[0.010s]
not (x <= 0)
&& (if x >= 0 then x else 0) >= 0
&& (if (x - 1) >= 0 then x - 1 else 0) >= 0
==> (x - 1) <= 0
|| Ordinal.( << ) (Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0))
(Ordinal.Int (if x >= 0 then x else 0))
• simplify
 into (not ((not (x <= 0) && (if x >= 0 then x else 0) >= 0) && (if x >= 1 then -1 + x else 0) >= 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.<<_102| (|Ordinal.Int_93| (ite (>= x_1135 1) (+ (- 1) x_1135) 0)) (|Ordi… expansions
• unsat
(let ((a!1 (not (= x_1135 (ite (>= x_1135 0) x_1135 0))))
(a!2 (+ x_1135 (* (- 1) (ite (>= x_1…

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>
File "jupyter cell 9", line 1, characters 0-63:
Error: 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/

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
originalsize _x
subsize (Destruct(Node, 0, _x))
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 0, _x)))
path[not Is_a(Leaf, _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.011s
details
Expand
smt_stats
 num checks 8 arith assert lower 11 arith pivots 9 rlimit count 4468 mk clause 16 datatype occurs check 12 mk bool var 73 arith assert upper 8 datatype splits 3 decisions 14 arith add rows 7 propagations 11 conflicts 6 arith fixed eqs 3 datatype accessor ax 13 arith conflicts 2 datatype constructor ax 11 num allocs 2.74792e+07 final checks 4 added eqs 47 del clause 9 arith eq adapter 6 memory 13.7 max memory 13.7
Expand
• start[0.011s]
not Is_a(Leaf, _x)
&& Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 0, _x)) >= 0
==> Is_a(Leaf, Destruct(Node, 0, _x)) && Is_a(Leaf, Destruct(Node, 0, _x))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))))
(Ordinal.Int (Ordinal.count _x))
• simplify
 into (not ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0) && Ordinal.count (Destruct(Node, 0, _x)) >= 0) || Is_a(Leaf, Destruct(Node, 0, _x))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x)))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 tree_1185| … expansions
• unroll
 expr (|count_ty_0 tree_1185| (|get.Node.0_1168| _x_1174)) expansions
• unroll
 expr (|count_ty_0 tree_1185| _x_1174) expansions
• unsat
(let ((a!1 (ite (>= (|count_ty_0 tree_1185| (|get.Node.1_1169| _x_1174)) 0)
(|coun…

call size (Destruct(Node, 1, _x)) from size _x
originalsize _x
subsize (Destruct(Node, 1, _x))
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 1, _x)))
path[not Is_a(Leaf, _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.011s
details
Expand
smt_stats
 num checks 8 arith assert lower 11 arith pivots 9 rlimit count 2234 mk clause 16 datatype occurs check 12 mk bool var 73 arith assert upper 8 datatype splits 3 decisions 14 arith add rows 7 propagations 11 conflicts 6 arith fixed eqs 3 datatype accessor ax 13 arith conflicts 2 datatype constructor ax 11 num allocs 2.24949e+07 final checks 4 added eqs 47 del clause 9 arith eq adapter 6 memory 10.8 max memory 13.55
Expand
• start[0.011s]
not Is_a(Leaf, _x)
&& Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 1, _x)) >= 0
==> Is_a(Leaf, Destruct(Node, 1, _x)) && Is_a(Leaf, Destruct(Node, 1, _x))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))))
(Ordinal.Int (Ordinal.count _x))
• simplify
 into (not ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0) && Ordinal.count (Destruct(Node, 1, _x)) >= 0) || Is_a(Leaf, Destruct(Node, 1, _x))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x)))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 tree_1185| … expansions
• unroll
 expr (|count_ty_0 tree_1185| (|get.Node.1_1169| _x_1174)) expansions
• unroll
 expr (|count_ty_0 tree_1185| _x_1174) expansions
• unsat
(let ((a!1 (ite (>= (|count_ty_0 tree_1185| (|get.Node.0_1168| _x_1174)) 0)
(|coun…

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:
- : int tree -> bool = <fun>
module CX : sig val x : int tree end
Instance (after 9 steps, 0.021s):
let (x : int tree) =
(Node
((Node ((Leaf (9)), (Leaf (8)))),
(Node ((Leaf (7)), (Node ((Leaf (10)), (Leaf (11))))))))
Instance
proof attempt
ground_instances9
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
 arith offset eqs 2 num checks 19 arith assert lower 134 arith pivots 73 rlimit count 11137 mk clause 168 datatype occurs check 17 mk bool var 725 arith assert upper 83 datatype splits 36 decisions 132 arith add rows 204 arith bound prop 7 propagations 401 interface eqs 4 conflicts 23 arith fixed eqs 26 datatype accessor ax 135 arith conflicts 6 arith assert diseq 52 datatype constructor ax 135 num allocs 3.49467e+07 final checks 22 added eqs 724 del clause 101 arith eq adapter 95 memory 17.29 max memory 17.29
Expand
• start[0.021s] size :var_0: = 5
• unroll
 expr (size_1195 x_45) expansions
• unroll
 expr (size_1195 (|get.Node.1_1194| x_45)) expansions
• unroll
 expr (size_1195 (|get.Node.0_1193| x_45)) expansions
• unroll
 expr (size_1195 (|get.Node.1_1194| (|get.Node.1_1194| x_45))) expansions
• unroll
 expr (size_1195 (|get.Node.0_1193| (|get.Node.1_1194| x_45))) expansions
• unroll
 expr (size_1195 (|get.Node.1_1194| (|get.Node.0_1193| x_45))) expansions
• unroll
 expr (size_1195 (|get.Node.0_1193| (|get.Node.0_1193| x_45))) expansions
• unroll
 expr (size_1195 (|get.Node.1_1194| (|get.Node.1_1194| (|get.Node.1_1194| x_45)))) expansions
• unroll
 expr (size_1195 (|get.Node.0_1193| (|get.Node.1_1194| (|get.Node.1_1194| x_45)))) expansions
• Sat (Some let (x : int tree) = (Node ((Node ((Leaf (9)), (Leaf (8)))), (Node ((Leaf (7)), (Node ((Leaf (10)), (Leaf (11)))))))) )
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
originalsum_tree _x
subsum_tree (Destruct(Node, 0, _x))
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 0, _x)))
path[not Is_a(Leaf, _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 8 arith assert lower 11 arith pivots 9 rlimit count 4704 mk clause 16 datatype occurs check 12 mk bool var 73 arith assert upper 8 datatype splits 3 decisions 14 arith add rows 7 propagations 11 conflicts 6 arith fixed eqs 3 datatype accessor ax 13 arith conflicts 2 datatype constructor ax 11 num allocs 6.8596e+07 final checks 4 added eqs 47 del clause 9 arith eq adapter 6 memory 14.78 max memory 17.57
Expand
• start[0.013s]
not Is_a(Leaf, _x)
&& Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 0, _x)) >= 0
==> Is_a(Leaf, Destruct(Node, 0, _x)) && Is_a(Leaf, Destruct(Node, 0, _x))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))))
(Ordinal.Int (Ordinal.count _x))
• simplify
 into (not ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0) && Ordinal.count (Destruct(Node, 0, _x)) >= 0) || Is_a(Leaf, Destruct(Node, 0, _x))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x)))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int tree_1234| (… expansions
• unroll
 expr (|count_int tree_1234| (|get.Node.0_1221| _x_1223)) expansions
• unroll
 expr (|count_int tree_1234| _x_1223) expansions
• unsat
(let ((a!1 (ite (>= (|count_int tree_1234| (|get.Node.1_1222| _x_1223)) 0)
(|count…

call sum_tree (Destruct(Node, 1, _x)) from sum_tree _x
originalsum_tree _x
subsum_tree (Destruct(Node, 1, _x))
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 1, _x)))
path[not Is_a(Leaf, _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 8 arith assert lower 11 arith pivots 9 rlimit count 2352 mk clause 16 datatype occurs check 12 mk bool var 73 arith assert upper 8 datatype splits 3 decisions 14 arith add rows 7 propagations 11 conflicts 6 arith fixed eqs 3 datatype accessor ax 13 arith conflicts 2 datatype constructor ax 11 num allocs 5.38615e+07 final checks 4 added eqs 47 del clause 9 arith eq adapter 6 memory 14.7 max memory 17.29
Expand
• start[0.013s]
not Is_a(Leaf, _x)
&& Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 1, _x)) >= 0
==> Is_a(Leaf, Destruct(Node, 1, _x)) && Is_a(Leaf, Destruct(Node, 1, _x))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))))
(Ordinal.Int (Ordinal.count _x))
• simplify
 into (not ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0) && Ordinal.count (Destruct(Node, 1, _x)) >= 0) || Is_a(Leaf, Destruct(Node, 1, _x))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x)))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_int tree_1234| (… expansions
• unroll
 expr (|count_int tree_1234| (|get.Node.1_1222| _x_1223)) expansions
• unroll
 expr (|count_int tree_1234| _x_1223) expansions
• unsat
(let ((a!1 (ite (>= (|count_int tree_1234| (|get.Node.0_1221| _x_1223)) 0)
(|count…

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 : int tree end
Instance (after 26 steps, 0.053s):
let (x : int tree) =
(Node
((Node ((Leaf ((-4812))), (Leaf (6652)))),
(Node
((Node ((Leaf ((-11210))), (Leaf ((-2997))))),
(Node ((Leaf (6202)), (Leaf (6167))))))))
Instance
proof attempt
ground_instances26
definitions0
inductions0
search_time
0.053s
details
Expand
smt_stats
 arith offset eqs 14 num checks 53 arith assert lower 512 arith patches_succ 3 arith pivots 446 rlimit count 59302 mk clause 594 datatype occurs check 94 mk bool var 2763 arith gcd tests 20 arith assert upper 365 datatype splits 100 decisions 981 arith add rows 1413 arith bound prop 8 propagations 1905 arith patches 4 interface eqs 9 conflicts 57 arith fixed eqs 266 datatype accessor ax 517 minimized lits 6 arith conflicts 9 arith assert diseq 147 datatype constructor ax 517 num allocs 8.07638e+07 final checks 57 added eqs 3313 del clause 421 arith ineq splits 1 arith eq adapter 437 memory 18.83 max memory 18.83
Expand
• start[0.053s] size :var_0: >= 5 && size :var_0: = 3 * sum_tree :var_0:
• unroll
 expr (sum_tree_47 x_52) expansions
• unroll
 expr (size_1244 x_52) expansions
• unroll
 expr (sum_tree_47 (|get.Node.1_1243| x_52)) expansions
• unroll
 expr (sum_tree_47 (|get.Node.0_1242| x_52)) expansions
• unroll
 expr (size_1244 (|get.Node.1_1243| x_52)) expansions
• unroll
 expr (size_1244 (|get.Node.0_1242| x_52)) expansions
• unroll
 expr (sum_tree_47 (|get.Node.1_1243| (|get.Node.1_1243| x_52))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.0_1242| (|get.Node.1_1243| x_52))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.1_1243| (|get.Node.0_1242| x_52))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.0_1242| (|get.Node.0_1242| x_52))) expansions
• unroll
 expr (size_1244 (|get.Node.1_1243| (|get.Node.1_1243| x_52))) expansions
• unroll
 expr (size_1244 (|get.Node.0_1242| (|get.Node.1_1243| x_52))) expansions
• unroll
 expr (size_1244 (|get.Node.1_1243| (|get.Node.0_1242| x_52))) expansions
• unroll
 expr (size_1244 (|get.Node.0_1242| (|get.Node.0_1242| x_52))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.1_1243| (|get.Node.1_1243| (|get.Node.1_1243| x_52)))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.0_1242| (|get.Node.1_1243| (|get.Node.1_1243| x_52)))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.1_1243| (|get.Node.0_1242| (|get.Node.1_1243| x_52)))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.0_1242| (|get.Node.0_1242| (|get.Node.1_1243| x_52)))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.1_1243| (|get.Node.1_1243| (|get.Node.0_1242| x_52)))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.0_1242| (|get.Node.1_1243| (|get.Node.0_1242| x_52)))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.1_1243| (|get.Node.0_1242| (|get.Node.0_1242| x_52)))) expansions
• unroll
 expr (sum_tree_47 (|get.Node.0_1242| (|get.Node.0_1242| (|get.Node.0_1242| x_52)))) expansions
• unroll
 expr (size_1244 (|get.Node.1_1243| (|get.Node.1_1243| (|get.Node.1_1243| x_52)))) expansions
• unroll
 expr (size_1244 (|get.Node.0_1242| (|get.Node.1_1243| (|get.Node.1_1243| x_52)))) expansions
• unroll
 expr (size_1244 (|get.Node.1_1243| (|get.Node.0_1242| (|get.Node.1_1243| x_52)))) expansions
• unroll
 expr (size_1244 (|get.Node.0_1242| (|get.Node.0_1242| (|get.Node.1_1243| x_52)))) expansions
• Sat (Some let (x : int tree) = (Node ((Node ((Leaf ((-4812))), (Leaf (6652)))), (Node ((Node ((Leaf ((-11210))), (Leaf ((-2997))))), (Node ((Leaf (6202)), (Leaf (6167)))))))) )

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

Ackermann and Admission Hints¶ 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 : int -> int -> int = <fun>
File "jupyter cell 18", line 1, characters 0-105:
Error: rejected definition for function ack, Imandra could not prove termination.
hint: 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))
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/

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 : int -> int -> int = <fun>
termination proof

Termination proof

call ack (m - 1) 1 from ack m n
originalack m n
suback (m - 1) 1
original ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if n >= 0 then n else 0)]
sub ordinalOrdinal.of_list [Ordinal.Int (if (m - 1) >= 0 then m - 1 else 0); Ordinal.Int (if 1 >= 0 then 1 else 0)]
path[n <= 0 && not (m <= 0)]
proof
detailed proof
ground_instances5
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 arith offset eqs 12 num checks 12 arith assert lower 19 arith pivots 9 rlimit count 26618 mk clause 76 datatype occurs check 77 mk bool var 215 arith assert upper 42 datatype splits 8 decisions 114 arith add rows 15 propagations 118 conflicts 21 arith fixed eqs 8 datatype accessor ax 31 arith conflicts 3 arith assert diseq 5 datatype constructor ax 18 num allocs 1.59659e+08 final checks 8 added eqs 225 del clause 21 arith eq adapter 33 memory 25.69 max memory 25.71
Expand
• start[0.016s]
n <= 0
&& not (m <= 0)
&& (if m >= 0 then m else 0) >= 0
&& (if n >= 0 then n else 0) >= 0
&& (if (m - 1) >= 0 then m - 1 else 0) >= 0
&& (if 1 >= 0 then 1 else 0) >= 0
==> not (1 <= 0 && not ((m - 1) <= 0))
&& not (not (1 <= 0) && not ((m - 1) <= 0))
&& not (not (1 <= 0) && not ((m - 1) <= 0))
|| Ordinal.( << )
(if (Ordinal.Int (if (m - 1) >= 0 then m - 1 else 0)) :: … = …
then … else …)
…
• simplify
 into (not ((((n <= 0 && not (m <= 0)) && (if m >= 0 then m else 0) >= 0) && (if n >= 0 then n else 0) >= 0) && (if m >= 1 then -1 + m else 0) >= 0) || m <= 1) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1)) (Ordinal.Int 1)) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1)) (Ordinal.Int (if n >= 0 then n else 0))) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) (|Ordinal.Int_93| 1)) expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0)) (|Ordinal.Int_93|… expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0… expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0… expansions
• unsat
(let ((a!1 (|Ordinal.shift_127|
(|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0…

call ack (m - 1) (ack m (n - 1)) from ack m n
originalack m n
suback (m - 1) (ack m (n - 1))
original ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if n >= 0 then n else 0)]
sub ordinalOrdinal.of_list [Ordinal.Int (if (m - 1) >= 0 then m - 1 else 0); Ordinal.Int (if ack m (n - 1) >= 0 then ack m (n - 1) else 0)]
path[not (n <= 0) && not (m <= 0)]
proof
detailed proof
ground_instances5
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 12 arith assert lower 72 arith pivots 20 rlimit count 19802 mk clause 94 datatype occurs check 98 mk bool var 229 arith assert upper 25 datatype splits 8 decisions 129 arith add rows 23 arith bound prop 1 propagations 172 conflicts 21 arith fixed eqs 24 datatype accessor ax 31 arith conflicts 2 arith assert diseq 3 datatype constructor ax 17 num allocs 1.44377e+08 final checks 8 added eqs 189 del clause 38 arith eq adapter 28 memory 22.63 max memory 25.71
Expand
• start[0.016s]
not (n <= 0)
&& not (m <= 0)
&& (if m >= 0 then m else 0) >= 0
&& (if n >= 0 then n else 0) >= 0
&& (if (m - 1) >= 0 then m - 1 else 0) >= 0
&& (if ack m (n - 1) >= 0 then ack m (n - 1) else 0) >= 0
==> not (ack m (n - 1) <= 0 && not ((m - 1) <= 0))
&& not (not (ack m (n - 1) <= 0) && not ((m - 1) <= 0))
&& not (not (ack m (n - 1) <= 0) && not ((m - 1) <= 0))
|| Ordinal.( << ) (if … then … else …) …
• simplify
 into (not (((((not (n <= 0) && not (m <= 0)) && (if m >= 0 then m else 0) >= 0) && (if n >= 0 then n else 0) >= 0) && (if m >= 1 then -1 + m else 0) >= 0) && (if ack m (-1 + n) >= 0 then ack m (-1 + n) else 0) >= 0) || not (ack m (-1 + n) <= 0 && not (m <= 1)) && not (not (ack m (-1 + n) <= 0) && not (m <= 1))) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1)) (Ordinal.Int (if ack m (-1 + n) >= 0 then ack m (-1 + n) else 0))) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1)) (Ordinal.Int (if n >= 0 then n else 0))) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) (|Ordinal.Int_93| 1)) expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0)) (|Ordinal.Int_93|… expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0… expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0… expansions
• unsat
(let ((a!1 (|Ordinal.shift_127|
(|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
…

call ack m (n - 1) from ack m n
originalack m n
suback m (n - 1)
original ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if n >= 0 then n else 0)]
sub ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0)]
path[not (n <= 0) && not (m <= 0)]
proof
detailed proof
ground_instances8
definitions0
inductions0
search_time
0.023s
details
Expand
smt_stats
 arith offset eqs 3 num checks 18 arith assert lower 27 arith pivots 18 rlimit count 12328 mk clause 184 datatype occurs check 211 mk bool var 392 arith assert upper 27 datatype splits 31 decisions 263 arith add rows 28 arith bound prop 2 propagations 278 interface eqs 1 conflicts 24 arith fixed eqs 18 datatype accessor ax 65 arith conflicts 1 arith assert diseq 6 datatype constructor ax 46 num allocs 1.08622e+08 final checks 16 added eqs 352 del clause 84 arith eq adapter 23 memory 25.71 max memory 25.71
Expand
• start[0.023s]
not (n <= 0)
&& not (m <= 0)
&& (if m >= 0 then m else 0) >= 0
&& (if n >= 0 then n else 0) >= 0
&& (if m >= 0 then m else 0) >= 0
&& (if (n - 1) >= 0 then n - 1 else 0) >= 0
==> not ((n - 1) <= 0 && not (m <= 0))
&& not (not ((n - 1) <= 0) && not (m <= 0))
&& not (not ((n - 1) <= 0) && not (m <= 0))
|| Ordinal.( << )
(if [Ordinal.Int (if m >= 0 then m else 0);
Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0)]
= []
then Ordinal.Int 0 else …)
…
• simplify
 into (not ((((not (n <= 0) && not (m <= 0)) && (if m >= 0 then m else 0) >= 0) && (if n >= 0 then n else 0) >= 0) && (if n >= 1 then -1 + n else 0) >= 0) || not (n <= 1 && not (m <= 0)) && not (not (n <= 1) && not (m <= 0))) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1)) (Ordinal.Int (if n >= 1 then -1 + n else 0))) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1)) (Ordinal.Int (if n >= 0 then n else 0))) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) (|Ordinal.Int_93| 1)) expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_127| (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0)) … expansions
• unsat
(let ((a!1 (|Ordinal.shift_127|
(|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
…

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 int | Cons of t * int * t
val pp : Format.formatter -> t -> unit
val of_int : int -> t
val ( ~$) : int -> 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 shift : t -> by:t -> t val is_valid : 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 -> int -> 'a list -> 'a list = <fun>
File "jupyter cell 25", line 1, characters 0-96:
Error: 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/

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 :
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)
[@@measure left_pad_measure n xs]
Out:
val left_pad : 'a -> int -> 'a list -> 'a list = <fun>
termination proof

Termination proof

call left_pad c n (c :: xs) from left_pad c n xs
originalleft_pad c n xs
subleft_pad c n (c :: xs)
original ordinalleft_pad_measure n xs
sub ordinalleft_pad_measure n (c :: xs)
path[not (List.length xs >= n)]
proof
detailed proof
ground_instances2
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 5 arith assert lower 10 arith pivots 5 rlimit count 1781 mk clause 7 datatype occurs check 16 mk bool var 36 arith assert upper 5 datatype splits 2 decisions 6 arith add rows 13 propagations 4 conflicts 3 arith fixed eqs 2 datatype accessor ax 5 arith conflicts 1 datatype constructor ax 2 num allocs 2.37079e+08 final checks 4 added eqs 13 del clause 4 arith eq adapter 3 memory 27.37 max memory 27.37
Expand
• start[0.013s]
not (List.length xs >= n)
&& (if (n - List.length xs) >= 0 then n - List.length xs else 0) >= 0
&& (if (n - List.length (… :: xs)) >= 0
then n - List.length (… :: xs) else 0)
>= 0
==> List.length (… :: xs) >= n
|| Ordinal.( << )
(Ordinal.Int
(if (n - List.length (… :: xs)) >= 0
then n - List.length (… :: xs) else 0))
(Ordinal.Int
(if (n - List.length xs) >= 0 then n - List.length xs else 0))
• simplify
 into (not ((not (List.length xs >= n) && (if (n + -1 * List.length xs) >= 0 then n + -1 * List.length xs else 0) >= 0) && (if (n + -1 * List.length (c :: xs)) >= 0 then n + -1 * List.length (c :: xs) else 0) >= 0) || List.length (c :: xs) >= n) || Ordinal.( << ) (Ordinal.Int (if (n + -1 * List.length (c :: xs)) >= 0 then n + -1 * List.length (c :: xs) else 0)) (Ordinal.Int (if (n + -1 * List.length xs) >= 0 then n + -1 * List.length xs else 0)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (+ n_1469 (* (- 1) (|List.length_1465| (|::_3| c_1468 xs_1470))))) (a!2 (>= (+ n_14… expansions
• unroll
 expr (|List.length_1465| (|::_3| c_1468 xs_1470)) expansions
• unsat
(let ((a!1 (+ n_1469 (* (- 1) (|List.length_1465| (|::_3| c_1468 xs_1470)))))
(a!5 (>= (+ n_14…

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

iml
definition
fun (c : 'a) ->
fun (n : int) ->
fun (xs : 'a list) ->
if List.length xs >= n then xs else left_pad c n (c :: xs)
def
type'a -> int -> 'a list -> 'a list
recursivetrue
call signatureleft_pad (c : 'a) (n : int) (xs : 'a list)
measured subset[n; xs]
parametrictrue
sub-function(s)
Expand
 name measure_fun.left_pad type int -> 'b list -> Ordinal.t recursive false call signature measure_fun.left_pad (n : int) (xs : 'b list) body left_pad_measure n xs parametric true validated in 0.001s location jupyter cell 28:1,0--130
validatedin 0.024s
locationjupyter cell 28:1,0--130
hashes