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:5515656
final checks:4
added eqs:37
del clause:4
arith eq adapter:5
memory:15.370000
max memory:15.370000
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!

            ordinals

            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:10048117
            final checks:4
            added eqs:44
            del clause:14
            arith eq adapter:10
            memory:15.780000
            max memory:15.780000
            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:15588086
                      final checks:1
                      added eqs:4
                      del clause:5
                      arith eq adapter:2
                      memory:16.030000
                      max memory:16.030000
                      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:38390209
                            final checks:4
                            added eqs:47
                            del clause:9
                            arith eq adapter:6
                            memory:16.720000
                            max memory:16.720000
                            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:30152164
                                      final checks:4
                                      added eqs:47
                                      del clause:9
                                      arith eq adapter:6
                                      memory:16.680000
                                      max memory:16.680000
                                      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:48658982
                                                final checks:22
                                                added eqs:687
                                                del clause:78
                                                arith eq adapter:87
                                                memory:17.250000
                                                max memory:17.250000
                                                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:72325302
                                                                  final checks:4
                                                                  added eqs:47
                                                                  del clause:9
                                                                  arith eq adapter:6
                                                                  memory:17.380000
                                                                  max memory:17.380000
                                                                  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:60394852
                                                                            final checks:4
                                                                            added eqs:47
                                                                            del clause:9
                                                                            arith eq adapter:6
                                                                            memory:17.320000
                                                                            max memory:17.320000
                                                                            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:88503790
                                                                                      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.410000
                                                                                      max memory:18.510000
                                                                                      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
                                                                                                                                          

                                                                                                                                          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 [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))
                                                                                                                                            [@@adm m,n]
                                                                                                                                          
                                                                                                                                          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:169077732
                                                                                                                                          final checks:9
                                                                                                                                          added eqs:153
                                                                                                                                          del clause:17
                                                                                                                                          arith eq adapter:13
                                                                                                                                          memory:18.860000
                                                                                                                                          max memory:18.910000
                                                                                                                                          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:147388709
                                                                                                                                                        final checks:9
                                                                                                                                                        added eqs:203
                                                                                                                                                        del clause:28
                                                                                                                                                        arith eq adapter:14
                                                                                                                                                        memory:18.840000
                                                                                                                                                        max memory:18.910000
                                                                                                                                                        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:127047593
                                                                                                                                                                      final checks:15
                                                                                                                                                                      added eqs:359
                                                                                                                                                                      del clause:72
                                                                                                                                                                      arith eq adapter:19
                                                                                                                                                                      memory:18.910000
                                                                                                                                                                      max memory:18.910000
                                                                                                                                                                      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.

                                                                                                                                                                                          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 [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)
                                                                                                                                                                                          [@@measure left_pad_measure n 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`
                                                                                                                                                                                          original:left_pad c n xs
                                                                                                                                                                                          sub:left_pad c n (c :: xs)
                                                                                                                                                                                          original ordinal:left_pad_measure n 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:220747671
                                                                                                                                                                                          final checks:6
                                                                                                                                                                                          added eqs:23
                                                                                                                                                                                          del clause:12
                                                                                                                                                                                          arith eq adapter:5
                                                                                                                                                                                          memory:19.600000
                                                                                                                                                                                          max memory:19.600000
                                                                                                                                                                                          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.