# 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 -> int = <fun>
File "jupyter cell 1", line 1, characters 0-21Error: 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 (_cnt xs)
sub ordinalOrdinal.Int (_cnt (List.tl xs))
path[not Is_a([], xs)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.035s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 10 rlimit count 1551 arith-cheap-eqs 1 mk clause 11 datatype occurs check 12 mk bool var 36 arith-lower 4 datatype splits 1 decisions 4 propagations 6 arith-max-rows 2 conflicts 3 datatype accessor ax 7 datatype constructor ax 5 num allocs 688530 final checks 4 added eqs 26 del clause 9 arith eq adapter 3 arith-upper 5 memory 5.22 max memory 5.22
Expand
• start[0.035s]
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
not Is_a([], xs) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], xs) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list (const 0)_1710| xs_1699) expansions
• unroll
 expr (|count.list (const 0)_1710| (|get.::.1_1691| xs_1699)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_1710| (|get.::.… 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 : int -> int -> int -> int = <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 : int list -> int = <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 (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 18 arith-max-columns 16 arith-conflicts 2 rlimit count 2024 mk clause 20 datatype occurs check 12 mk bool var 56 arith-lower 15 arith-diseq 1 datatype splits 1 decisions 15 propagations 14 arith-max-rows 4 conflicts 7 datatype accessor ax 7 datatype constructor ax 5 num allocs 2.66978e+06 final checks 4 added eqs 38 del clause 13 arith eq adapter 10 arith-upper 12 memory 5.64 max memory 5.64
Expand
• start[0.015s]
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
not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list mk_nat_1756| _x_1745) expansions
• unroll
 expr (|count.list mk_nat_1756| (|get.::.1_1744| _x_1745)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list mk_nat_1756| (|get.::.1_1… expansions
• Unsat

In :
sum_lst [1;2;3]

Out:
- : int = 6

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

Out:
val sum : int -> int = <fun>

termination proof

### Termination proof

call sum (x - 1) from sum x
originalsum x
subsum (x - 1)
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.Int (_cnt (x - 1))
path[not (x <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.010s
details
Expand
smt_stats
 num checks 3 arith-make-feasible 5 arith-max-columns 11 arith-conflicts 1 rlimit count 988 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.82312e+06 final checks 1 added eqs 6 del clause 5 arith eq adapter 2 arith-upper 6 memory 5.91 max memory 5.91
Expand
• start[0.010s]
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.<<_126| (|Ordinal.Int_111| (ite (>= x_1785 1) (+ (- 1) x_1785) 0)) (|Ord… expansions
• Unsat

In :
sum 5

Out:
- : int = 15

In :
sum 100

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

termination proof

### Termination proof

call size (Destruct(Node, 0, _x)) from size _x
originalsize _x
subsize (Destruct(Node, 0, _x))
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (Destruct(Node, 0, _x)))
path[not Is_a(Leaf, _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.020s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 18 arith-max-columns 16 arith-conflicts 2 rlimit count 4780 mk clause 20 datatype occurs check 14 mk bool var 75 arith-lower 14 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 2.31718e+07 final checks 4 added eqs 59 del clause 13 arith eq adapter 10 arith-upper 13 memory 6.73 max memory 11.79
Expand
• start[0.020s]
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 (const 0)_1859| _x_1846) expansions
• unroll
 expr (|count.tree (const 0)_1859| (|get.Node.0_1839| _x_1846)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.tree (const 0)_1859| … expansions
• Unsat

call size (Destruct(Node, 1, _x)) from size _x
originalsize _x
subsize (Destruct(Node, 1, _x))
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (Destruct(Node, 1, _x)))
path[not Is_a(Leaf, _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 18 arith-max-columns 16 arith-conflicts 2 rlimit count 2390 mk clause 20 datatype occurs check 14 mk bool var 75 arith-lower 14 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.31065e+07 final checks 4 added eqs 59 del clause 13 arith eq adapter 10 arith-upper 13 memory 9.2 max memory 9.2
Expand
• start[0.015s]
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 (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 (const 0)_1859| _x_1846) expansions
• unroll
 expr (|count.tree (const 0)_1859| (|get.Node.1_1840| _x_1846)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.tree (const 0)_1859| … 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:
- : int tree -> bool = <fun>
module CX : sig val x : int tree end

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

Instance
proof attempt
ground_instances9
definitions0
inductions0
search_time
0.020s
details
Expand
smt_stats
 num checks 19 arith-make-feasible 62 arith-max-columns 35 arith-conflicts 8 rlimit count 7057 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 2.75828e+07 final checks 17 added eqs 606 del clause 65 arith eq adapter 80 arith-upper 112 memory 9.73 max memory 11.79
Expand
• start[0.020s] size ( :var_0: ) = 5
• unroll
 expr (size_1928 x_59) expansions
• unroll
 expr (size_1928 (|get.Node.1_1927| x_59)) expansions
• unroll
 expr (size_1928 (|get.Node.0_1926| x_59)) expansions
• unroll
 expr (size_1928 (|get.Node.1_1927| (|get.Node.1_1927| x_59))) expansions
• unroll
 expr (size_1928 (|get.Node.0_1926| (|get.Node.1_1927| x_59))) expansions
• unroll
 expr (size_1928 (|get.Node.1_1927| (|get.Node.0_1926| x_59))) expansions
• unroll
 expr (size_1928 (|get.Node.0_1926| (|get.Node.0_1926| x_59))) expansions
• unroll
 expr (size_1928 (|get.Node.1_1927| (|get.Node.1_1927| (|get.Node.1_1927| x_59)))) expansions
• unroll
 expr (size_1928 (|get.Node.0_1926| (|get.Node.1_1927| (|get.Node.1_1927| x_59)))) expansions
• Sat (Some let (x : int tree) = (Node ((Node ((Leaf (7)), (Leaf (8)))), (Node ((Leaf (10)), (Node ((Leaf (11)), (Leaf (9)))))))) )
In :
size CX.x

Out:
- : int = 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 : int tree -> int = <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 (_cnt _x)
sub ordinalOrdinal.Int (_cnt (Destruct(Node, 0, _x)))
path[not Is_a(Leaf, _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 19 arith-max-columns 17 arith-conflicts 2 rlimit count 4878 mk clause 20 datatype occurs check 14 mk bool var 75 arith-lower 14 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 4.75869e+07 final checks 4 added eqs 59 del clause 13 arith eq adapter 10 arith-upper 13 memory 9.94 max memory 12.48
Expand
• start[0.016s]
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 tree) = Destruct(Node, 0, _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 (|count.tree mk_nat_1964| _x_1951) expansions
• unroll
 expr (|count.tree mk_nat_1964| (|get.Node.0_1949| _x_1951)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.tree mk_nat_1964| (|get.Node.0… expansions
• Unsat

call sum_tree (Destruct(Node, 1, _x)) from sum_tree _x
originalsum_tree _x
subsum_tree (Destruct(Node, 1, _x))
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (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-make-feasible 18 arith-max-columns 16 arith-conflicts 2 rlimit count 2452 mk clause 20 datatype occurs check 14 mk bool var 75 arith-lower 14 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 3.70784e+07 final checks 4 added eqs 59 del clause 13 arith eq adapter 10 arith-upper 13 memory 9.89 max memory 11.79
Expand
• start[0.013s]
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 (|count.tree mk_nat_1964| _x_1951) expansions
• unroll
 expr (|count.tree mk_nat_1964| (|get.Node.1_1950| _x_1951)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.tree mk_nat_1964| (|get.Node.1… 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:
- : int tree -> bool = <fun>
module CX : sig val x : int tree end

Instance (after 26 steps, 0.054s):
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_instances26
definitions0
inductions0
search_time
0.054s
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 5.6576e+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 34595 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 13.65 max memory 13.65
Expand
• start[0.054s]
let (_x_0 : int) = size ( :var_0: ) in
_x_0 >= 5 && _x_0 = 3 * sum_tree ( :var_0: )
• unroll
 expr (sum_tree_61 x_69) expansions
• unroll
 expr (size_2033 x_69) expansions
• unroll
 expr (sum_tree_61 (|get.Node.1_2032| x_69)) expansions
• unroll
 expr (sum_tree_61 (|get.Node.0_2031| x_69)) expansions
• unroll
 expr (size_2033 (|get.Node.1_2032| x_69)) expansions
• unroll
 expr (size_2033 (|get.Node.0_2031| x_69)) expansions
• unroll
 expr (sum_tree_61 (|get.Node.1_2032| (|get.Node.1_2032| x_69))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.0_2031| (|get.Node.1_2032| x_69))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.1_2032| (|get.Node.0_2031| x_69))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.0_2031| (|get.Node.0_2031| x_69))) expansions
• unroll
 expr (size_2033 (|get.Node.1_2032| (|get.Node.1_2032| x_69))) expansions
• unroll
 expr (size_2033 (|get.Node.0_2031| (|get.Node.1_2032| x_69))) expansions
• unroll
 expr (size_2033 (|get.Node.1_2032| (|get.Node.0_2031| x_69))) expansions
• unroll
 expr (size_2033 (|get.Node.0_2031| (|get.Node.0_2031| x_69))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.1_2032| (|get.Node.1_2032| (|get.Node.1_2032| x_69)))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.0_2031| (|get.Node.1_2032| (|get.Node.1_2032| x_69)))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.1_2032| (|get.Node.0_2031| (|get.Node.1_2032| x_69)))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.0_2031| (|get.Node.0_2031| (|get.Node.1_2032| x_69)))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.1_2032| (|get.Node.1_2032| (|get.Node.0_2031| x_69)))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.0_2031| (|get.Node.1_2032| (|get.Node.0_2031| x_69)))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.1_2032| (|get.Node.0_2031| (|get.Node.0_2031| x_69)))) expansions
• unroll
 expr (sum_tree_61 (|get.Node.0_2031| (|get.Node.0_2031| (|get.Node.0_2031| x_69)))) expansions
• unroll
 expr (size_2033 (|get.Node.1_2032| (|get.Node.1_2032| (|get.Node.1_2032| x_69)))) expansions
• unroll
 expr (size_2033 (|get.Node.0_2031| (|get.Node.1_2032| (|get.Node.1_2032| x_69)))) expansions
• unroll
 expr (size_2033 (|get.Node.1_2032| (|get.Node.0_2031| (|get.Node.1_2032| x_69)))) expansions
• unroll
 expr (size_2033 (|get.Node.0_2031| (|get.Node.0_2031| (|get.Node.1_2032| x_69)))) expansions
• Sat (Some let (x : int tree) = (Node ((Node ((Leaf (56867)), (Leaf ((-46532))))), (Node ((Node ((Leaf ((-54829))), (Leaf ((-50521))))), (Node ((Leaf (107403)), (Leaf ((-12386))))))))) )

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

In :
size CX.x

Out:
- : int = 6

In :
3 * sum_tree CX.x

Out:
- : int = 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-105Error: 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))
[@@adm m,n]

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 (_cnt m); Ordinal.Int (_cnt n)]
sub ordinalOrdinal.of_list [Ordinal.Int (_cnt (m - 1)); Ordinal.Int (_cnt 1)]
path[n <= 0 && not (m <= 0)]
proof
detailed proof
ground_instances5
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 12 arith-make-feasible 21 arith-max-columns 20 rlimit count 19134 arith-cheap-eqs 8 mk clause 48 datatype occurs check 59 mk bool var 125 arith-lower 19 arith-diseq 8 datatype splits 4 decisions 53 arith-propagations 12 propagations 47 arith-bound-propagations-cheap 12 arith-max-rows 7 conflicts 13 datatype accessor ax 21 arith-bound-propagations-lp 1 datatype constructor ax 10 num allocs 1.11112e+08 final checks 8 added eqs 130 del clause 21 arith eq adapter 13 arith-upper 14 memory 19.67 max memory 19.68
Expand
• start[0.016s]
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 Is_a([], …) then … else …)
(if Is_a([], …) then … else …)
• ##### simplify
 into let (_x_0 : Ordinal.t) = Ordinal.Int 1 in (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))) || m <= 1 expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) (|Ordinal.Int_111| 1)) expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … expansions
• unroll
 expr (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) 0)) (|Ordinal.Int_11… expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) … expansions
• Unsat

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 (_cnt m); Ordinal.Int (_cnt n)]
sub ordinalOrdinal.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_instances5
definitions0
inductions0
search_time
0.022s
details
Expand
smt_stats
 num checks 11 arith-assume-eqs 1 arith-make-feasible 17 arith-max-columns 24 rlimit count 13850 arith-cheap-eqs 2 mk clause 76 datatype occurs check 78 mk bool var 123 arith-lower 6 arith-diseq 14 datatype splits 4 decisions 45 arith-propagations 14 propagations 74 interface eqs 1 arith-bound-propagations-cheap 14 arith-max-rows 9 conflicts 11 datatype accessor ax 21 arith-bound-propagations-lp 1 datatype constructor ax 9 num allocs 1.01531e+08 final checks 9 added eqs 99 del clause 27 arith eq adapter 12 arith-upper 28 time 0.001 memory 17.05 max memory 19.68
Expand
• start[0.022s]
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 Is_a([], …) then … else …)
(if Is_a([], …) then … else …)
• ##### simplify
 into let (_x_0 : int) = ack m (-1 + n) in let (_x_1 : bool) = _x_0 <= 0 in let (_x_2 : bool) = not (m <= 1) in let (_x_3 : Ordinal.t) = Ordinal.Int 1 in (not (not (n <= 0) && not (m <= 0)) || not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_3) (Ordinal.Int (if _x_0 >= 0 then _x_0 else 0))) (Ordinal.plus (Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) _x_3) (Ordinal.Int (if n >= 0 then n else 0))) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) (|Ordinal.Int_111| 1)) expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … expansions
• unroll
 expr (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) 0)) (|Ordinal.Int_11… expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) … expansions
• Unsat

call ack m (n - 1) from ack m n
originalack m n
suback m (n - 1)
original ordinalOrdinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
sub ordinalOrdinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt (n - 1))]
path[not (n <= 0) && not (m <= 0)]
proof
detailed proof
ground_instances7
definitions0
inductions0
search_time
0.020s
details
Expand
smt_stats
 num checks 16 arith-assume-eqs 1 arith-make-feasible 16 arith-max-columns 34 rlimit count 8170 arith-cheap-eqs 9 mk clause 82 datatype occurs check 141 mk bool var 194 arith-lower 9 arith-diseq 3 datatype splits 13 decisions 89 arith-propagations 3 propagations 75 interface eqs 1 arith-bound-propagations-cheap 3 arith-max-rows 16 conflicts 17 datatype accessor ax 35 arith-bound-propagations-lp 2 datatype constructor ax 20 num allocs 8.25557e+07 final checks 14 added eqs 157 del clause 47 arith eq adapter 11 arith-upper 14 memory 16.99 max memory 16.99
Expand
• start[0.020s]
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 Is_a([], …) then … else …)
(if Is_a([], …) then … else …)
• ##### simplify
 into let (_x_0 : bool) = n <= 1 in let (_x_1 : bool) = not (m <= 0) in let (_x_2 : Ordinal.t) = Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) (Ordinal.Int 1) in (not (_x_0 && _x_1) && not (not _x_0 && _x_1) || Ordinal.( << ) (Ordinal.plus _x_2 (Ordinal.Int (if n >= 1 then -1 + n else 0))) (Ordinal.plus _x_2 (Ordinal.Int (if n >= 0 then n else 0)))) || not (not (n <= 0) && _x_1) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … expansions
• unroll
 expr (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) (|Ordinal.Int_111| 1)) expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … expansions
• unroll
 expr (let ((a!1 (|Ordinal.shift_205| (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0)) … 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 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 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.

# Left pad¶

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-96Error: 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 : int -> '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)
[@@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-assume-eqs 2 arith-make-feasible 11 arith-max-columns 17 arith-conflicts 1 rlimit count 1814 arith-cheap-eqs 2 mk clause 14 datatype occurs check 12 mk bool var 36 arith-lower 7 datatype splits 2 decisions 9 arith-propagations 2 propagations 6 interface eqs 2 arith-bound-propagations-cheap 2 arith-max-rows 7 conflicts 3 datatype accessor ax 5 datatype constructor ax 2 num allocs 1.56895e+08 final checks 6 added eqs 21 del clause 10 arith eq adapter 5 arith-upper 9 memory 20.41 max memory 20.41
Expand
• start[0.013s]
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 (c :: 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 (c :: xs) in let (_x_2 : int) = n + -1 * _x_1 in let (_x_3 : int) = n + -1 * _x_0 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_2359 (* (- 1) (|List.length_2354| (|::_3| c_2358 xs_2360))))) (a!2 (>= (+ n_23… expansions
• unroll
 expr (|List.length_2354| (|::_3| c_2358 xs_2360)) 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:

### Fun: left_pad

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
nameleft_pad
type'a -> int -> 'a list -> 'a list
recursivetrue
def-depth4
def-ty-depth2
call signatureleft_pad (c : 'a) (n : int) (xs : 'a list)
measured subset[n; xs]
parametrictrue
validatedin 0.004s
locationjupyter cell 28:1,0--130
sub-function(s)
Expand
 name measure_fun.left_pad type int -> 'b list -> Ordinal.t recursive false def-depth 6 def-ty-depth 2 call signature measure_fun.left_pad (n : int) (xs : 'b list) body left_pad_measure n xs parametric true validated in 0.002s location jupyter cell 28:1,0--130
hashes
 left_pad KLd+2TQBjsVq4sqBwq8NCBsvd7pFxysqw2lxIwXz9WU measure_fun.left_pad lNG8FxDohlAvgDKWxv3iKnGTaXXQr0h8WTJWKQmONZU

Excellent! This concludes our brief introduction to program termination in Imandra.