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>

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

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

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

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

            Imandra accepts our function map and proves it terminating. Under the hood, Imandra uses ordinals in its termination analyses, beautiful mathematical objects representing equivalence classes of well-orderings. We'll discuss these more below!

            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.042s
            details:
            Expand
            smt_stats:
            num checks:8
            arith-make-feasible:18
            arith-max-columns:18
            arith-conflicts:2
            rlimit count:3725
            mk clause:25
            datatype occurs check:20
            mk bool var:80
            arith-lower:14
            datatype splits:1
            decisions:16
            propagations:26
            arith-max-rows:6
            conflicts:9
            datatype accessor ax:10
            minimized lits:1
            datatype constructor ax:9
            num allocs:2489161
            final checks:4
            added eqs:56
            del clause:11
            arith eq adapter:13
            arith-upper:16
            memory:5.150000
            max memory:5.150000
            Expand
            • start[0.042s]
                let (_x_0 : int) = count.list mk_nat _x in
                let (_x_1 : int list) = List.tl _x in
                let (_x_2 : int) = count.list mk_nat _x_1 in
                _x <> [] && _x_0 >= 0 && _x_2 >= 0
                ==> not (_x_1 <> [])
                    || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
            • simplify
              into:
              let (_x_0 : int list) = List.tl _x in
              let (_x_1 : int) = count.list mk_nat _x_0 in
              let (_x_2 : int) = count.list mk_nat _x in
              (not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
              || not ((_x <> [] && _x_2 >= 0) && _x_1 >= 0)
              expansions:
              []
              rewrite_steps:
                forward_chaining:
                • unroll
                  expr:
                  (|Ordinal.<<_129/client|
                    (|Ordinal.Int_114/client|
                      (|`count.list { Resolved_term.spec_idx = 0;…
                  expansions:
                  • unroll
                    expr:
                    (|`count.list { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty …
                    expansions:
                    • unroll
                      expr:
                      (|`count.list { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty …
                      expansions:
                      • Unsat
                      In [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.024s
                      details:
                      Expand
                      smt_stats:
                      num checks:3
                      arith-make-feasible:5
                      arith-max-columns:11
                      arith-conflicts:1
                      rlimit count:4795
                      mk clause:5
                      datatype occurs check:2
                      mk bool var:17
                      arith-lower:3
                      decisions:2
                      arith-propagations:3
                      propagations:2
                      arith-bound-propagations-cheap:3
                      arith-max-rows:4
                      conflicts:2
                      datatype accessor ax:2
                      num allocs:5853860
                      final checks:1
                      added eqs:6
                      del clause:5
                      arith eq adapter:2
                      arith-upper:6
                      memory:5.220000
                      max memory:7.770000
                      Expand
                      • start[0.024s]
                          let (_x_0 : int) = if x >= 0 then x else 0 in
                          let (_x_1 : int) = x - 1 in
                          let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
                          not (x <= 0) && _x_0 >= 0 && _x_2 >= 0
                          ==> _x_1 <= 0 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                      • simplify
                        into:
                        (x <= 0 || x <= 1)
                        || Ordinal.( << ) (Ordinal.Int (if x >= 1 then (-1) + x else 0))
                           (Ordinal.Int (if x >= 0 then x else 0))
                        expansions:
                        []
                        rewrite_steps:
                          forward_chaining:
                          • unroll
                            expr:
                            (|Ordinal.<<_129/client|
                              (|Ordinal.Int_114/client|
                                (ite (>= x_1723/server 1) (+ (- 1) x_1723/s…
                            expansions:
                            • Unsat
                            In [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>
                            
                            At jupyter cell 9:1,0--62
                            1 | let rec sum_oops x =
                            2 |  if x = 0 then 0
                            3 |  else x + sum_oops (x-1)
                            
                            Error[/server]:
                              unsupported: rejected definition for function sum_oops,
                                           Imandra could not prove termination. 
                                           hint: problematic sub-call from `sum_oops x`
                                           to `sum_oops (x - 1)`  under path not (x = 0) is not decreasing
                                           (measured subset: (x))
                              See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
                            ----------------------------------------------------------------------------
                            Context:
                              At jupyter cell 9:1,0--62
                              1 | let rec sum_oops x =
                              2 |  if x = 0 then 0
                              3 |  else x + sum_oops (x-1)
                              
                              Checking termination of function `sum_oops`
                            

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

                            Structural Recursions

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

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

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

                                                In [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.050s):
                                                let x : int tree =
                                                  Node (Node (Leaf 7, Leaf 8), Node (Leaf 10, Node (Leaf 11, Leaf 9)))
                                                
                                                Instance
                                                proof attempt
                                                ground_instances:9
                                                definitions:0
                                                inductions:0
                                                search_time:
                                                0.050s
                                                details:
                                                Expand
                                                smt_stats:
                                                num checks:19
                                                arith-make-feasible:62
                                                arith-max-columns:35
                                                arith-conflicts:8
                                                rlimit count:6752
                                                arith-cheap-eqs:4
                                                mk clause:149
                                                datatype occurs check:53
                                                mk bool var:563
                                                arith-lower:73
                                                arith-diseq:38
                                                datatype splits:20
                                                decisions:114
                                                arith-propagations:15
                                                propagations:292
                                                arith-bound-propagations-cheap:15
                                                arith-max-rows:13
                                                conflicts:18
                                                datatype accessor ax:105
                                                minimized lits:2
                                                arith-bound-propagations-lp:8
                                                datatype constructor ax:105
                                                num allocs:30671286
                                                final checks:17
                                                added eqs:606
                                                del clause:65
                                                arith eq adapter:80
                                                arith-upper:112
                                                memory:5.610000
                                                max memory:10.260000
                                                Expand
                                                • start[0.050s] size ( :var_0: ) = 5
                                                • unroll
                                                  expr:
                                                  (size_1854/server x_1379/client)
                                                  expansions:
                                                  • unroll
                                                    expr:
                                                    (size_1854/server (|get.Node.1_1853/server| x_1379/client))
                                                    expansions:
                                                    • unroll
                                                      expr:
                                                      (size_1854/server (|get.Node.0_1852/server| x_1379/client))
                                                      expansions:
                                                      • unroll
                                                        expr:
                                                        (size_1854/server (|get.Node.1_1853/server|
                                                                            (|get.Node.1_1853/server| x_1379/cli…
                                                        expansions:
                                                        • unroll
                                                          expr:
                                                          (size_1854/server (|get.Node.0_1852/server|
                                                                              (|get.Node.1_1853/server| x_1379/cli…
                                                          expansions:
                                                          • unroll
                                                            expr:
                                                            (size_1854/server (|get.Node.1_1853/server|
                                                                                (|get.Node.0_1852/server| x_1379/cli…
                                                            expansions:
                                                            • unroll
                                                              expr:
                                                              (size_1854/server (|get.Node.0_1852/server|
                                                                                  (|get.Node.0_1852/server| x_1379/cli…
                                                              expansions:
                                                              • unroll
                                                                expr:
                                                                (size_1854/server (|get.Node.1_1853/server|
                                                                                    (|get.Node.1_1853/server|
                                                                          …
                                                                expansions:
                                                                • unroll
                                                                  expr:
                                                                  (size_1854/server (|get.Node.0_1852/server|
                                                                                      (|get.Node.1_1853/server|
                                                                            …
                                                                  expansions:
                                                                  • Sat (Some let x : int tree = Node (Node (Leaf (Z.of_nativeint (7n)), Leaf (Z.of_nativeint (8n))), Node (Leaf (Z.of_nativeint (10n)), Node (Leaf (Z.of_nativeint (11n)), Leaf (Z.of_nativeint (9n))))) )
                                                                  In [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.022s
                                                                  details:
                                                                  Expand
                                                                  smt_stats:
                                                                  num checks:8
                                                                  arith-make-feasible:19
                                                                  arith-max-columns:17
                                                                  arith-conflicts:2
                                                                  rlimit count:11145
                                                                  mk clause:20
                                                                  datatype occurs check:15
                                                                  mk bool var:75
                                                                  arith-lower:13
                                                                  arith-diseq:1
                                                                  datatype splits:3
                                                                  decisions:19
                                                                  propagations:15
                                                                  arith-max-rows:4
                                                                  conflicts:7
                                                                  datatype accessor ax:13
                                                                  datatype constructor ax:11
                                                                  num allocs:50112340
                                                                  final checks:4
                                                                  added eqs:59
                                                                  del clause:13
                                                                  arith eq adapter:10
                                                                  arith-upper:14
                                                                  memory:5.670000
                                                                  max memory:10.260000
                                                                  Expand
                                                                  • start[0.022s]
                                                                      let (_x_0 : int) = count.tree mk_nat _x in
                                                                      let (_x_1 : int tree) = Destruct(Node, 0, _x) in
                                                                      let (_x_2 : int) = count.tree mk_nat _x_1 in
                                                                      let (_x_3 : bool) = Is_a(Leaf, _x_1) in
                                                                      not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
                                                                      ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                  • simplify
                                                                    into:
                                                                    let (_x_0 : int) = count.tree mk_nat _x in
                                                                    let (_x_1 : int tree) = Destruct(Node, 0, _x) in
                                                                    let (_x_2 : int) = count.tree mk_nat _x_1 in
                                                                    (not ((not Is_a(Leaf, _x) && _x_0 >= 0) && _x_2 >= 0)
                                                                     || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0))
                                                                    || Is_a(Leaf, _x_1)
                                                                    expansions:
                                                                    []
                                                                    rewrite_steps:
                                                                      forward_chaining:
                                                                      • unroll
                                                                        expr:
                                                                        (|`count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty …
                                                                        expansions:
                                                                        • unroll
                                                                          expr:
                                                                          (|`count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty …
                                                                          expansions:
                                                                          • unroll
                                                                            expr:
                                                                            (|Ordinal.<<_129/client|
                                                                              (|Ordinal.Int_114/client|
                                                                                (|`count.tree { Resolved_term.spec_idx = 0;…
                                                                            expansions:
                                                                            • Unsat
                                                                            call `sum_tree (Destruct(Node, 1, _x))` from `sum_tree _x`
                                                                            original:sum_tree _x
                                                                            sub:sum_tree (Destruct(Node, 1, _x))
                                                                            original ordinal:Ordinal.Int (_cnt _x)
                                                                            sub ordinal:Ordinal.Int (_cnt (Destruct(Node, 1, _x)))
                                                                            path:[not Is_a(Leaf, _x)]
                                                                            proof:
                                                                            detailed proof
                                                                            ground_instances:3
                                                                            definitions:0
                                                                            inductions:0
                                                                            search_time:
                                                                            0.025s
                                                                            details:
                                                                            Expand
                                                                            smt_stats:
                                                                            num checks:8
                                                                            arith-make-feasible:15
                                                                            arith-max-columns:17
                                                                            arith-conflicts:2
                                                                            rlimit count:8843
                                                                            mk clause:18
                                                                            datatype occurs check:14
                                                                            mk bool var:70
                                                                            arith-lower:8
                                                                            datatype splits:3
                                                                            decisions:14
                                                                            propagations:11
                                                                            arith-max-rows:4
                                                                            conflicts:6
                                                                            datatype accessor ax:13
                                                                            datatype constructor ax:11
                                                                            num allocs:40225932
                                                                            final checks:4
                                                                            added eqs:53
                                                                            del clause:11
                                                                            arith eq adapter:6
                                                                            arith-upper:11
                                                                            memory:5.690000
                                                                            max memory:10.260000
                                                                            Expand
                                                                            • start[0.025s]
                                                                                let (_x_0 : int) = count.tree mk_nat _x in
                                                                                let (_x_1 : int tree) = Destruct(Node, 1, _x) in
                                                                                let (_x_2 : int) = count.tree mk_nat _x_1 in
                                                                                let (_x_3 : bool) = Is_a(Leaf, _x_1) in
                                                                                not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
                                                                                ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                            • simplify
                                                                              into:
                                                                              let (_x_0 : int tree) = Destruct(Node, 1, _x) in
                                                                              let (_x_1 : int) = count.tree mk_nat _x_0 in
                                                                              let (_x_2 : int) = count.tree mk_nat _x in
                                                                              (Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                              || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0)
                                                                              expansions:
                                                                              []
                                                                              rewrite_steps:
                                                                                forward_chaining:
                                                                                • unroll
                                                                                  expr:
                                                                                  (|Ordinal.<<_129/client|
                                                                                    (|Ordinal.Int_114/client|
                                                                                      (|`count.tree { Resolved_term.spec_idx = 0;…
                                                                                  expansions:
                                                                                  • unroll
                                                                                    expr:
                                                                                    (|`count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty …
                                                                                    expansions:
                                                                                    • unroll
                                                                                      expr:
                                                                                      (|`count.tree { Resolved_term.spec_idx = 0; spec_arg = (v.cls (cls_ty: int -> int) mk_nat); spec_ty …
                                                                                      expansions:
                                                                                      • Unsat

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

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

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

                                                                                                                                          In [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>
                                                                                                                                          
                                                                                                                                          termination proof

                                                                                                                                          Termination proof

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

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

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

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

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

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

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

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

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

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

                                                                                                                                                                                                                                              Measures and Ordinals

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

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

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

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

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

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

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

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

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

                                                                                                                                                                                                                                                        In [29]:
                                                                                                                                                                                                                                                        #history left_pad
                                                                                                                                                                                                                                                        
                                                                                                                                                                                                                                                        Out[29]:
                                                                                                                                                                                                                                                        
                                                                                                                                                                                                                                                        

                                                                                                                                                                                                                                                        Fun: left_pad

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

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