# 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 [1]:
let rec f x = f x + 1

Out[1]:
val f : 'a -> Z.t = <fun>
Error:
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/
At jupyter cell 1:1,0--21
1 | let rec f x = f x + 1
^^^^^^^^^^^^^^^^^^^^^


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

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

Out[2]:
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.012s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 5 arith tableau max rows: 4 arith tableau max columns: 11 arith pivots: 4 rlimit count: 1806 mk clause: 12 datatype occurs check: 12 mk bool var: 52 arith assert upper: 5 datatype splits: 1 decisions: 10 arith row summations: 7 propagations: 12 conflicts: 7 arith fixed eqs: 4 datatype accessor ax: 10 arith conflicts: 1 arith num rows: 4 datatype constructor ax: 8 num allocs: 5.51566e+06 final checks: 4 added eqs: 37 del clause: 4 arith eq adapter: 5 memory: 15.37 max memory: 15.37
Expand
• start[0.012s]
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.<<| (|Ordinal.Int_79/boot| (|count.list_409/server| (|get.::.1_390/server|… expansions:
• unroll
 expr: (|count.list_409/server| (|get.::.1_390/server| xs_398/server)) expansions:
• unroll
 expr: (|count.list_409/server| xs_398/server) 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 [3]:
let k x y z = if x > y then x + y else z - 1

Out[3]:
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 [4]:
let rec sum_lst = function
| [] -> 0
| x :: xs -> x + sum_lst xs

Out[4]:
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.013s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 6 arith tableau max columns: 17 arith pivots: 6 rlimit count: 2306 mk clause: 21 datatype occurs check: 12 mk bool var: 69 arith assert upper: 14 datatype splits: 1 decisions: 16 arith row summations: 16 propagations: 22 conflicts: 10 arith fixed eqs: 5 datatype accessor ax: 8 arith conflicts: 2 arith num rows: 6 datatype constructor ax: 9 num allocs: 1.00481e+07 final checks: 4 added eqs: 44 del clause: 14 arith eq adapter: 10 memory: 15.78 max memory: 15.78
Expand
• start[0.013s]
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.<<| (|Ordinal.Int_79/boot| (|count.list_455/server| (|get.::.1_443/server|… expansions:
• unroll
 expr: (|count.list_455/server| (|get.::.1_443/server| _x_444/server)) expansions:
• unroll
 expr: (|count.list_455/server| _x_444/server) expansions:
• Unsat
In [5]:
sum_lst [1;2;3]

Out[5]:
- : Z.t = 6

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

Out[6]:
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.010s
details:
Expand
smt_stats:
 num checks: 3 arith assert lower: 6 arith tableau max rows: 4 arith tableau max columns: 9 arith pivots: 2 rlimit count: 1099 mk clause: 5 datatype occurs check: 2 mk bool var: 17 arith assert upper: 3 decisions: 2 arith row summations: 3 propagations: 2 conflicts: 2 arith fixed eqs: 2 datatype accessor ax: 2 arith conflicts: 1 arith num rows: 4 num allocs: 1.55881e+07 final checks: 1 added eqs: 4 del clause: 5 arith eq adapter: 2 memory: 16.03 max memory: 16.03
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.<<| (|Ordinal.Int_79/boot| (ite (>= x_484/server 1) (+ (- 1) x_484/server)… expansions:
• Unsat
In [7]:
sum 5

Out[7]:
- : Z.t = 15

In [8]:
sum 100

Out[8]:
- : 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 [9]:
let rec sum_oops x =
if x = 0 then 0
else x + sum_oops (x-1)

Out[9]:
val sum_oops : Z.t -> Z.t = <fun>
Error:
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/
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)


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 [10]:
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree

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

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

Out[11]:
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.011s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 4 arith tableau max columns: 15 arith pivots: 9 rlimit count: 4396 mk clause: 16 datatype occurs check: 15 mk bool var: 68 arith assert upper: 8 datatype splits: 3 decisions: 14 arith row summations: 7 propagations: 11 conflicts: 6 arith fixed eqs: 3 datatype accessor ax: 13 arith conflicts: 2 arith num rows: 4 datatype constructor ax: 11 num allocs: 3.83902e+07 final checks: 4 added eqs: 47 del clause: 9 arith eq adapter: 6 memory: 16.72 max memory: 16.72
Expand
• start[0.011s]
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 : 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 not (not Is_a(Leaf, _x) && (_x_0 >= 0) && (_x_2 >= 0)) || Is_a(Leaf, _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.tree_559/server| (|ge… expansions:
• unroll
 expr: (|count.tree_559/server| (|get.Node.0_539/server| _x_546/server)) expansions:
• unroll
 expr: (|count.tree_559/server| _x_546/server) 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.015s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 4 arith tableau max columns: 15 arith pivots: 9 rlimit count: 2179 mk clause: 16 datatype occurs check: 14 mk bool var: 68 arith assert upper: 8 datatype splits: 3 decisions: 14 arith row summations: 7 propagations: 11 conflicts: 6 arith fixed eqs: 3 datatype accessor ax: 13 arith conflicts: 2 arith num rows: 4 datatype constructor ax: 11 num allocs: 3.01522e+07 final checks: 4 added eqs: 47 del clause: 9 arith eq adapter: 6 memory: 16.68 max memory: 16.68
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: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.tree_559/server| (|ge… expansions:
• unroll
 expr: (|count.tree_559/server| (|get.Node.1_540/server| _x_546/server)) expansions:
• unroll
 expr: (|count.tree_559/server| _x_546/server) expansions:
• Unsat

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

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

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

Instance (after 9 steps, 0.016s):
let x : int tree =
Node (Node (Leaf 13, Leaf 14), Node (Leaf 9, Node (Leaf 11, Leaf 10)))

Instance
proof attempt
ground_instances:9
definitions:0
inductions:0
search_time:
0.016s
details:
Expand
smt_stats:
 arith offset eqs: 6 num checks: 19 arith assert lower: 128 arith tableau max rows: 15 arith tableau max columns: 35 arith pivots: 65 rlimit count: 11221 mk clause: 152 datatype occurs check: 53 mk bool var: 612 arith assert upper: 82 datatype splits: 27 decisions: 135 arith row summations: 213 arith bound prop: 10 propagations: 329 interface eqs: 5 conflicts: 20 arith fixed eqs: 25 arith assume eqs: 5 datatype accessor ax: 115 arith conflicts: 9 arith num rows: 15 arith assert diseq: 48 datatype constructor ax: 115 num allocs: 4.8659e+07 final checks: 22 added eqs: 687 del clause: 78 arith eq adapter: 87 memory: 17.25 max memory: 17.25
Expand
• start[0.016s] size ( :var_0: ) = 5
• unroll
 expr: (size_628/server x_1294/client) expansions:
• unroll
 expr: (size_628/server (|get.Node.1_627/server| x_1294/client)) expansions:
• unroll
 expr: (size_628/server (|get.Node.0_626/server| x_1294/client)) expansions:
• unroll
 expr: (size_628/server (|get.Node.1_627/server| (|get.Node.1_627/server| x_1294/client)… expansions:
• unroll
 expr: (size_628/server (|get.Node.0_626/server| (|get.Node.1_627/server| x_1294/client)… expansions:
• unroll
 expr: (size_628/server (|get.Node.1_627/server| (|get.Node.0_626/server| x_1294/client)… expansions:
• unroll
 expr: (size_628/server (|get.Node.0_626/server| (|get.Node.0_626/server| x_1294/client)… expansions:
• unroll
 expr: (size_628/server (|get.Node.1_627/server| (|get.Node.1_627/server| … expansions:
• unroll
 expr: (size_628/server (|get.Node.0_626/server| (|get.Node.1_627/server| … expansions:
• Sat (Some let x : int tree = Node (Node (Leaf (Z.of_nativeint (13n)), Leaf (Z.of_nativeint (14n))), Node (Leaf (Z.of_nativeint (9n)), Node (Leaf (Z.of_nativeint (11n)), Leaf (Z.of_nativeint (10n))))) )
In [13]:
size CX.x

Out[13]:
- : Z.t = 5


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

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

Out[14]:
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.011s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 4 arith tableau max columns: 15 arith pivots: 9 rlimit count: 4530 mk clause: 16 datatype occurs check: 15 mk bool var: 68 arith assert upper: 8 datatype splits: 3 decisions: 14 arith row summations: 7 propagations: 11 conflicts: 6 arith fixed eqs: 3 datatype accessor ax: 13 arith conflicts: 2 arith num rows: 4 datatype constructor ax: 11 num allocs: 7.23253e+07 final checks: 4 added eqs: 47 del clause: 9 arith eq adapter: 6 memory: 17.38 max memory: 17.38
Expand
• start[0.011s]
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 in let (_x_2 : int) = count.tree mk_nat _x_0 in Is_a(Leaf, _x_0) || not (not Is_a(Leaf, _x) && (_x_1 >= 0) && (_x_2 >= 0)) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_1) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.tree_662/server| (|ge… expansions:
• unroll
 expr: (|count.tree_662/server| (|get.Node.0_647/server| _x_649/server)) expansions:
• unroll
 expr: (|count.tree_662/server| _x_649/server) 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.010s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 11 arith tableau max rows: 4 arith tableau max columns: 15 arith pivots: 9 rlimit count: 2241 mk clause: 16 datatype occurs check: 14 mk bool var: 68 arith assert upper: 8 datatype splits: 3 decisions: 14 arith row summations: 7 propagations: 11 conflicts: 6 arith fixed eqs: 3 datatype accessor ax: 13 arith conflicts: 2 arith num rows: 4 datatype constructor ax: 11 num allocs: 6.03949e+07 final checks: 4 added eqs: 47 del clause: 9 arith eq adapter: 6 memory: 17.32 max memory: 17.32
Expand
• start[0.010s]
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.<<| (|Ordinal.Int_79/boot| (|count.tree_662/server| (|ge… expansions:
• unroll
 expr: (|count.tree_662/server| (|get.Node.1_648/server| _x_649/server)) expansions:
• unroll
 expr: (|count.tree_662/server| _x_649/server) expansions:
• Unsat

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

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

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

Instance (after 26 steps, 0.034s):
let x : int tree =
Node
(Node (Leaf (-11632), Leaf 3554),
Node (Node (Leaf (-2131), Leaf 10877), Node (Leaf (-2997), Leaf 2331)))

Instance
proof attempt
ground_instances:26
definitions:0
inductions:0
search_time:
0.034s
details:
Expand
smt_stats:
 arith offset eqs: 11 arith assert lower: 522 arith patches_succ: 5 datatype occurs check: 243 datatype splits: 104 arith bound prop: 4 arith branch var: 2 propagations: 1896 arith patches: 7 interface eqs: 13 conflicts: 51 arith fixed eqs: 275 datatype constructor ax: 503 num allocs: 8.85038e+07 final checks: 61 added eqs: 3537 del clause: 440 num checks: 53 arith tableau max rows: 43 arith tableau max columns: 99 arith pivots: 459 rlimit count: 62843 mk clause: 600 mk bool var: 2742 arith gcd tests: 29 arith assert upper: 364 decisions: 901 arith row summations: 1457 arith assume eqs: 13 datatype accessor ax: 503 minimized lits: 6 arith conflicts: 9 arith num rows: 43 arith assert diseq: 157 arith ineq splits: 2 arith eq adapter: 420 memory: 18.41 max memory: 18.51
Expand
• start[0.034s]
let (_x_0 : int) = size ( :var_0: ) in
(_x_0 >= 5) && (_x_0 = 3 * sum_tree ( :var_0: ))
• unroll
 expr: (sum_tree_1296/client x_1301/client) expansions:
• unroll
 expr: (size_731/server x_1301/client) expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.1_730/server| x_1301/client)) expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.0_729/server| x_1301/client)) expansions:
• unroll
 expr: (size_731/server (|get.Node.1_730/server| x_1301/client)) expansions:
• unroll
 expr: (size_731/server (|get.Node.0_729/server| x_1301/client)) expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.1_730/server| (|get.Node.1_730/server| x_1301/client))) expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.0_729/server| (|get.Node.1_730/server| x_1301/client))) expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.1_730/server| (|get.Node.0_729/server| x_1301/client))) expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.0_729/server| (|get.Node.0_729/server| x_1301/client))) expansions:
• unroll
 expr: (size_731/server (|get.Node.1_730/server| (|get.Node.1_730/server| x_1301/client)… expansions:
• unroll
 expr: (size_731/server (|get.Node.0_729/server| (|get.Node.1_730/server| x_1301/client)… expansions:
• unroll
 expr: (size_731/server (|get.Node.1_730/server| (|get.Node.0_729/server| x_1301/client)… expansions:
• unroll
 expr: (size_731/server (|get.Node.0_729/server| (|get.Node.0_729/server| x_1301/client)… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.1_730/server| (|get.Node.1_730/server| (|get.Node.1_730/serve… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.0_729/server| (|get.Node.1_730/server| (|get.Node.1_730/serve… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.1_730/server| (|get.Node.0_729/server| (|get.Node.1_730/serve… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.0_729/server| (|get.Node.0_729/server| (|get.Node.1_730/serve… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.1_730/server| (|get.Node.1_730/server| (|get.Node.0_729/serve… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.0_729/server| (|get.Node.1_730/server| (|get.Node.0_729/serve… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.1_730/server| (|get.Node.0_729/server| (|get.Node.0_729/serve… expansions:
• unroll
 expr: (sum_tree_1296/client (|get.Node.0_729/server| (|get.Node.0_729/server| (|get.Node.0_729/serve… expansions:
• unroll
 expr: (size_731/server (|get.Node.1_730/server| (|get.Node.1_730/server| … expansions:
• unroll
 expr: (size_731/server (|get.Node.0_729/server| (|get.Node.1_730/server| … expansions:
• unroll
 expr: (size_731/server (|get.Node.1_730/server| (|get.Node.0_729/server| … expansions:
• unroll
 expr: (size_731/server (|get.Node.0_729/server| (|get.Node.0_729/server| … expansions:
• Sat (Some let x : int tree = Node (Node (Leaf (Z.of_nativeint (-11632n)), Leaf (Z.of_nativeint (3554n))), Node (Node (Leaf (Z.of_nativeint (-2131n)), Leaf (Z.of_nativeint (10877n))), Node (Leaf (Z.of_nativeint (-2997n)), Leaf (Z.of_nativeint (2331n))))) )

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

In [16]:
size CX.x

Out[16]:
- : Z.t = 6

In [17]:
3 * sum_tree CX.x

Out[17]:
- : 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 [18]:
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[18]:
val ack : Z.t -> Z.t -> Z.t = <fun>
Error:
unsupported: 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/
At jupyter cell 18:1,0--105
1 | let rec ack m n =
2 |   if m <= 0 then n + 1
3 |   else if n <= 0 then ack (m-1) 1
4 |   else ack (m-1) (ack m (n-1))


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 [19]:
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[19]:
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.014s
details:
Expand
smt_stats:
 arith offset eqs: 2 num checks: 12 arith assert lower: 10 arith tableau max rows: 7 arith tableau max columns: 19 arith pivots: 4 rlimit count: 24232 mk clause: 45 datatype occurs check: 66 mk bool var: 152 arith assert upper: 16 datatype splits: 8 decisions: 92 arith row summations: 6 arith bound prop: 2 propagations: 55 conflicts: 11 arith fixed eqs: 5 datatype accessor ax: 29 arith num rows: 7 arith assert diseq: 18 datatype constructor ax: 18 num allocs: 1.69078e+08 final checks: 9 added eqs: 153 del clause: 17 arith eq adapter: 13 memory: 18.86 max memory: 18.91
Expand
• start[0.014s]
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
let (_x_4 : Ordinal.t) = if … <> [] then … else … 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.( << ) _x_4 _x_4
• ###### simplify
 into: let (_x_0 : Ordinal.t) = Ordinal.Int 1 in not ((n <= 0) && not (m <= 0)) || 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))) || (m <= 1) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/server 1) (+ (- 1) m_796/s… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/server 0) m_796/server 0))… 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.015s
details:
Expand
smt_stats:
 num checks: 12 arith assert lower: 32 arith tableau max rows: 10 arith tableau max columns: 24 arith pivots: 13 rlimit count: 18126 mk clause: 69 datatype occurs check: 88 mk bool var: 194 arith assert upper: 10 datatype splits: 8 decisions: 93 arith row summations: 15 propagations: 118 conflicts: 13 arith fixed eqs: 9 datatype accessor ax: 36 arith conflicts: 1 arith num rows: 10 arith assert diseq: 12 datatype constructor ax: 23 num allocs: 1.47389e+08 final checks: 9 added eqs: 203 del clause: 28 arith eq adapter: 14 memory: 18.84 max memory: 18.91
Expand
• start[0.015s]
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
let (_x_5 : Ordinal.t) = if … <> [] then … else … 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.( << ) _x_5 _x_5
• ###### 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: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/server 1) (+ (- 1) m_796/s… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/server 0) m_796/server 0))… 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:8
definitions:0
inductions:0
search_time:
0.017s
details:
Expand
smt_stats:
 arith offset eqs: 3 num checks: 18 arith assert lower: 23 arith tableau max rows: 16 arith tableau max columns: 37 arith pivots: 17 rlimit count: 11147 mk clause: 115 datatype occurs check: 165 mk bool var: 346 arith assert upper: 22 datatype splits: 26 decisions: 146 arith row summations: 27 arith bound prop: 3 propagations: 128 conflicts: 23 arith fixed eqs: 14 datatype accessor ax: 68 arith conflicts: 3 arith num rows: 16 arith assert diseq: 3 datatype constructor ax: 51 num allocs: 1.27048e+08 final checks: 15 added eqs: 359 del clause: 72 arith eq adapter: 19 memory: 18.91 max memory: 18.91
Expand
• start[0.017s]
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
let (_x_5 : Ordinal.t) = if … <> [] then … else … 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.( << ) _x_5 _x_5
• ###### 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 … 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| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/server 0) m_796/server 0))… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… expansions:
• unroll
 expr: (let ((a!1 (|Ordinal.shift| (|Ordinal.Int_79/boot| (ite (>= m_796/serv… 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 [20]:
#show Ordinal

Out[20]:
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 [21]: Ordinal.omega  Out[21]: - : Ordinal.t = ω  In [22]: Ordinal.(omega + omega)  Out[22]: - : Ordinal.t = 2·ω  In [23]: let o1 = Ordinal.(omega + omega_omega + shift omega ~by:(omega + one))  Out[23]: val o1 : Ordinal.t = ω^(ω + 1)  In [24]: Ordinal.(o1 << omega_omega)  Out[24]: - : 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 [25]:
let rec left_pad c n xs =
if List.length xs >= n then
xs
else
left_pad c n (c :: xs)

Out[25]:
val left_pad : 'a -> Z.t -> 'a list -> 'a list = <fun>
Error:
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/
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)


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 [26]:
let left_pad_measure n xs =
Ordinal.of_int (n - List.length xs)

Out[26]:
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 [27]:
left_pad_measure 5 [1;2;3]

Out[27]:
- : Ordinal.t = 2


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

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

Out[28]:
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:2
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 arith offset eqs: 2 num checks: 5 arith assert lower: 10 arith tableau max rows: 7 arith tableau max columns: 14 arith pivots: 8 rlimit count: 2232 mk clause: 15 datatype occurs check: 12 mk bool var: 36 arith assert upper: 7 datatype splits: 2 decisions: 10 arith row summations: 21 propagations: 6 interface eqs: 2 conflicts: 3 arith fixed eqs: 4 arith assume eqs: 2 datatype accessor ax: 5 arith conflicts: 1 arith num rows: 7 datatype constructor ax: 2 num allocs: 2.20748e+08 final checks: 6 added eqs: 23 del clause: 12 arith eq adapter: 5 memory: 19.6 max memory: 19.6
Expand
• start[0.010s]
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_1049/server (* (- 1) (|List.length_1044/server| (|::|… expansions:
• unroll
 expr: (|List.length_1044/server| (|::| c_1048/server xs_1050/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 [29]:
#history left_pad

Out[29]:

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