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>
File "jupyter cell 1", line 1, characters 0-21:
Error: Validate: no measure provided, and Imandra cannot guess any.
Are you sure this function is actually terminating?

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`
originalmap f_0 xs
submap f_0 (List.tl xs)
original ordinalOrdinal.Int (Ordinal.count xs)
sub ordinalOrdinal.Int (Ordinal.count (List.tl xs))
path[not (xs = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
num checks7
arith assert lower5
arith pivots3
rlimit count1821
mk clause3
datatype occurs check21
mk bool var50
arith assert upper5
datatype splits3
decisions7
arith add rows7
propagations2
conflicts7
arith fixed eqs4
datatype accessor ax5
arith conflicts1
datatype constructor ax8
num allocs1365200595
final checks6
added eqs33
del clause1
arith eq adapter3
memory16.080000
max memory18.750000
Expand
  • start[0.015s]
      not (xs = []) && Ordinal.count xs >= 0 && Ordinal.count (List.tl xs) >= 0
      ==> List.tl xs = []
          || Ordinal.Int (Ordinal.count (List.tl xs)) Ordinal.<<
             Ordinal.Int (Ordinal.count xs)
  • simplify
    into
    (not
     ((not (xs = []) && Ordinal.count xs >= 0) && Ordinal.count (List.tl xs) >= 0)
     || List.tl xs = [])
    || Ordinal.Int (Ordinal.count (List.tl xs)) Ordinal.<<
       Ordinal.Int (Ordinal.count xs)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_121| (|Ordinal.Int_112|
                            (|count_`ty_1 list`_2466| (|get.::.1_2453| …
        expansions
        • unroll
          expr
          (|count_`ty_1 list`_2466| (|get.::.1_2453| xs_2461))
          expansions
          • unroll
            expr
            (|count_`ty_1 list`_2466| xs_2461)
            expansions
            • unsat
              (let ((a!1 (= (|count_`ty_1 list`_2466| xs_2461)
                            (+ 1 (|count_`ty_1 list`_2466| (|get.…

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

            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 : int -> int -> 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`
            originalsum_lst _x
            subsum_lst (List.tl _x)
            original ordinalOrdinal.Int (Ordinal.count _x)
            sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
            path[not (_x = [])]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.017s
            details
            Expand
            smt_stats
            num checks8
            arith assert lower17
            arith pivots9
            rlimit count4250
            mk clause19
            datatype occurs check21
            mk bool var78
            arith assert upper13
            datatype splits3
            decisions14
            arith add rows18
            propagations14
            conflicts9
            arith fixed eqs7
            datatype accessor ax5
            arith conflicts2
            datatype constructor ax8
            num allocs1406602049
            final checks6
            added eqs50
            del clause8
            arith eq adapter11
            memory16.290000
            max memory18.750000
            Expand
            • start[0.017s]
                not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                ==> List.tl _x = []
                    || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                       Ordinal.Int (Ordinal.count _x)
            • simplify
              into
              (not
               ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
               || List.tl _x = [])
              || Ordinal.Int (Ordinal.count (List.tl _x)) Ordinal.<<
                 Ordinal.Int (Ordinal.count _x)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                      (|count_`int list`_2489| (|get.::.1_2483| _…
                  expansions
                  • unroll
                    expr
                    (|count_`int list`_2489| (|get.::.1_2483| _x_2484))
                    expansions
                    • unroll
                      expr
                      (|count_`int list`_2489| _x_2484)
                      expansions
                      • unsat
                        (let ((a!1 (>= (ite (>= (|get.::.0_2482| _x_2484) 0)
                                            (|get.::.0_2482| _x_2484)
                         …

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

                      Termination proof

                      call `sum (x - 1)` from `sum x`
                      originalsum x
                      subsum (x - 1)
                      original ordinalOrdinal.Int (if x >= 0 then x else 0)
                      sub ordinalOrdinal.Int (if (x - 1) >= 0 then x - 1 else 0)
                      path[not (x <= 0)]
                      proof
                      detailed proof
                      ground_instances1
                      definitions0
                      inductions0
                      search_time
                      0.012s
                      details
                      Expand
                      smt_stats
                      num checks3
                      arith assert lower8
                      arith pivots2
                      rlimit count5281
                      mk clause4
                      datatype occurs check2
                      mk bool var20
                      arith assert upper3
                      decisions2
                      arith add rows3
                      propagations2
                      conflicts2
                      arith fixed eqs2
                      datatype accessor ax2
                      arith conflicts1
                      num allocs1446813921
                      final checks1
                      added eqs6
                      del clause4
                      arith eq adapter2
                      memory16.410000
                      max memory18.750000
                      Expand
                      • start[0.012s]
                          not (x <= 0)
                          && (if x >= 0 then x else 0) >= 0
                             && (if (x - 1) >= 0 then x - 1 else 0) >= 0
                          ==> (x - 1) <= 0
                              || Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0) Ordinal.<<
                                 Ordinal.Int (if x >= 0 then x else 0)
                      • simplify
                        into
                        (not
                         ((not (x <= 0) && (if x >= 0 then x else 0) >= 0)
                          && (if x >= 1 then -1 + x else 0) >= 0)
                         || x <= 1)
                        || Ordinal.Int (if x >= 1 then -1 + x else 0) Ordinal.<<
                           Ordinal.Int (if x >= 0 then x else 0)
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_121| (|Ordinal.Int_112| (ite (>= x_2495 1) (+ (- 1) x_2495) 0))
                                              (|Ord…
                            expansions
                            • unsat
                              (let ((a!1 (not (= x_2495 (ite (>= x_2495 0) x_2495 0))))
                                    (a!2 (+ x_2495 (* (- 1) (ite (>= x_2…

                            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>
                            File "jupyter cell 9", line 1, characters 0-63:
                            Error: rejected definition for function sum_oops,
                            Imandra could not prove termination. 
                            hint: problematic sub-call from `sum_oops x` to `sum_oops (x - 1)`
                             under path not (x = 0) is not decreasing (measured subset: (x))
                            

                            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`
                            originalsize _x
                            subsize (Destruct(Node, 0, _x))
                            original ordinalOrdinal.Int (Ordinal.count _x)
                            sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 0, _x)))
                            path[not Is_a(Leaf, _x)]
                            proof
                            detailed proof
                            ground_instances3
                            definitions0
                            inductions0
                            search_time
                            0.015s
                            details
                            Expand
                            smt_stats
                            num checks8
                            arith assert lower12
                            arith pivots9
                            rlimit count10961
                            mk clause16
                            datatype occurs check13
                            mk bool var73
                            arith assert upper7
                            datatype splits3
                            decisions14
                            arith add rows7
                            propagations11
                            conflicts6
                            arith fixed eqs3
                            datatype accessor ax13
                            arith conflicts2
                            datatype constructor ax11
                            num allocs1600525568
                            final checks4
                            added eqs47
                            del clause9
                            arith eq adapter6
                            memory19.250000
                            max memory19.250000
                            Expand
                            • start[0.015s]
                                not Is_a(Leaf, _x)
                                && Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 0, _x)) >= 0
                                ==> Is_a(Leaf, Destruct(Node, 0, _x)) && Is_a(Leaf, Destruct(Node, 0, _x))
                                    || Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))) Ordinal.<<
                                       Ordinal.Int (Ordinal.count _x)
                            • simplify
                              into
                              (not
                               ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0)
                                && Ordinal.count (Destruct(Node, 0, _x)) >= 0)
                               || Is_a(Leaf, Destruct(Node, 0, _x)))
                              || Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))) Ordinal.<<
                                 Ordinal.Int (Ordinal.count _x)
                              expansions
                              []
                              rewrite_steps
                                forward_chaining
                                • unroll
                                  expr
                                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                      (|count_`ty_0 tree`_2544| (|get.Node.0_2531…
                                  expansions
                                  • unroll
                                    expr
                                    (|count_`ty_0 tree`_2544| (|get.Node.0_2531| _x_2537))
                                    expansions
                                    • unroll
                                      expr
                                      (|count_`ty_0 tree`_2544| _x_2537)
                                      expansions
                                      • unsat
                                        (let ((a!1 (ite (>= (|count_`ty_0 tree`_2544| (|get.Node.1_2532| _x_2537)) 0)
                                                        (|coun…

                                      call `size (Destruct(Node, 1, _x))` from `size _x`
                                      originalsize _x
                                      subsize (Destruct(Node, 1, _x))
                                      original ordinalOrdinal.Int (Ordinal.count _x)
                                      sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 1, _x)))
                                      path[not Is_a(Leaf, _x)]
                                      proof
                                      detailed proof
                                      ground_instances3
                                      definitions0
                                      inductions0
                                      search_time
                                      0.016s
                                      details
                                      Expand
                                      smt_stats
                                      num checks8
                                      arith assert lower12
                                      arith pivots9
                                      rlimit count8747
                                      mk clause16
                                      datatype occurs check13
                                      mk bool var73
                                      arith assert upper7
                                      datatype splits3
                                      decisions14
                                      arith add rows7
                                      propagations11
                                      conflicts6
                                      arith fixed eqs3
                                      datatype accessor ax13
                                      arith conflicts2
                                      datatype constructor ax11
                                      num allocs1558172410
                                      final checks4
                                      added eqs47
                                      del clause9
                                      arith eq adapter6
                                      memory16.410000
                                      max memory18.750000
                                      Expand
                                      • start[0.016s]
                                          not Is_a(Leaf, _x)
                                          && Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 1, _x)) >= 0
                                          ==> Is_a(Leaf, Destruct(Node, 1, _x)) && Is_a(Leaf, Destruct(Node, 1, _x))
                                              || Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))) Ordinal.<<
                                                 Ordinal.Int (Ordinal.count _x)
                                      • simplify
                                        into
                                        (not
                                         ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0)
                                          && Ordinal.count (Destruct(Node, 1, _x)) >= 0)
                                         || Is_a(Leaf, Destruct(Node, 1, _x)))
                                        || Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))) Ordinal.<<
                                           Ordinal.Int (Ordinal.count _x)
                                        expansions
                                        []
                                        rewrite_steps
                                          forward_chaining
                                          • unroll
                                            expr
                                            (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                (|count_`ty_0 tree`_2544| (|get.Node.1_2532…
                                            expansions
                                            • unroll
                                              expr
                                              (|count_`ty_0 tree`_2544| (|get.Node.1_2532| _x_2537))
                                              expansions
                                              • unroll
                                                expr
                                                (|count_`ty_0 tree`_2544| _x_2537)
                                                expansions
                                                • unsat
                                                  (let ((a!1 (ite (>= (|count_`ty_0 tree`_2544| (|get.Node.0_2531| _x_2537)) 0)
                                                                  (|coun…

                                                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]:
                                                - : int tree -> bool = <fun>
                                                module CX : sig val x : Z.t tree end
                                                
                                                Instance (after 9 steps, 0.023s):
                                                 let x =
                                                   (Node
                                                      ((Node ((Leaf (7)), (Leaf (8)))),
                                                       (Node ((Leaf (10)), (Node ((Leaf (9)), (Leaf (11))))))))
                                                
                                                Instance
                                                proof attempt
                                                ground_instances9
                                                definitions0
                                                inductions0
                                                search_time
                                                0.023s
                                                details
                                                Expand
                                                smt_stats
                                                arith offset eqs4
                                                num checks19
                                                arith assert lower76
                                                arith pivots39
                                                rlimit count7257
                                                mk clause133
                                                datatype occurs check19
                                                mk bool var608
                                                arith assert upper66
                                                datatype splits19
                                                decisions103
                                                arith add rows87
                                                arith bound prop4
                                                propagations258
                                                conflicts20
                                                arith fixed eqs11
                                                datatype accessor ax112
                                                arith conflicts5
                                                arith assert diseq11
                                                datatype constructor ax112
                                                num allocs1648971753
                                                final checks18
                                                added eqs591
                                                del clause77
                                                arith eq adapter88
                                                memory16.810000
                                                max memory19.250000
                                                Expand
                                                • start[0.023s] size :var_0: = 5
                                                • unroll
                                                  expr
                                                  (size_2556 x_2549)
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (size_2556 (|get.Node.1_2555| x_2549))
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (size_2556 (|get.Node.0_2554| x_2549))
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (size_2556 (|get.Node.1_2555| (|get.Node.1_2555| x_2549)))
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (size_2556 (|get.Node.0_2554| (|get.Node.1_2555| x_2549)))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (size_2556 (|get.Node.1_2555| (|get.Node.0_2554| x_2549)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (size_2556 (|get.Node.0_2554| (|get.Node.0_2554| x_2549)))
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (size_2556 (|get.Node.1_2555| (|get.Node.1_2555| (|get.Node.1_2555| x_2549))))
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (size_2556 (|get.Node.0_2554| (|get.Node.1_2555| (|get.Node.1_2555| x_2549))))
                                                                  expansions
                                                                  • Sat (Some let x = (Node ((Node ((Leaf (7)), (Leaf (8)))), (Node ((Leaf (10)), (Node ((Leaf (9)), (Leaf (11)))))))) )
                                                                  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`
                                                                  originalsum_tree _x
                                                                  subsum_tree (Destruct(Node, 0, _x))
                                                                  original ordinalOrdinal.Int (Ordinal.count _x)
                                                                  sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 0, _x)))
                                                                  path[not Is_a(Leaf, _x)]
                                                                  proof
                                                                  detailed proof
                                                                  ground_instances3
                                                                  definitions0
                                                                  inductions0
                                                                  search_time
                                                                  0.016s
                                                                  details
                                                                  Expand
                                                                  smt_stats
                                                                  num checks8
                                                                  arith assert lower11
                                                                  arith pivots9
                                                                  rlimit count11947
                                                                  mk clause16
                                                                  datatype occurs check12
                                                                  mk bool var73
                                                                  arith assert upper8
                                                                  datatype splits3
                                                                  decisions14
                                                                  arith add rows7
                                                                  propagations11
                                                                  conflicts6
                                                                  arith fixed eqs3
                                                                  datatype accessor ax13
                                                                  arith conflicts2
                                                                  datatype constructor ax11
                                                                  num allocs1738910612
                                                                  final checks4
                                                                  added eqs47
                                                                  del clause9
                                                                  arith eq adapter6
                                                                  memory22.560000
                                                                  max memory22.560000
                                                                  Expand
                                                                  • start[0.016s]
                                                                      not Is_a(Leaf, _x)
                                                                      && Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 0, _x)) >= 0
                                                                      ==> Is_a(Leaf, Destruct(Node, 0, _x)) && Is_a(Leaf, Destruct(Node, 0, _x))
                                                                          || Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))) Ordinal.<<
                                                                             Ordinal.Int (Ordinal.count _x)
                                                                  • simplify
                                                                    into
                                                                    (not
                                                                     ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0)
                                                                      && Ordinal.count (Destruct(Node, 0, _x)) >= 0)
                                                                     || Is_a(Leaf, Destruct(Node, 0, _x)))
                                                                    || Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))) Ordinal.<<
                                                                       Ordinal.Int (Ordinal.count _x)
                                                                    expansions
                                                                    []
                                                                    rewrite_steps
                                                                      forward_chaining
                                                                      • unroll
                                                                        expr
                                                                        (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                            (|count_`int tree`_2598| (|get.Node.0_2554|…
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|count_`int tree`_2598| (|get.Node.0_2554| _x_2587))
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|count_`int tree`_2598| _x_2587)
                                                                            expansions
                                                                            • unsat
                                                                              (let ((a!1 (ite (>= (|count_`int tree`_2598| (|get.Node.1_2555| _x_2587)) 0)
                                                                                              (|count…

                                                                            call `sum_tree (Destruct(Node, 1, _x))` from `sum_tree _x`
                                                                            originalsum_tree _x
                                                                            subsum_tree (Destruct(Node, 1, _x))
                                                                            original ordinalOrdinal.Int (Ordinal.count _x)
                                                                            sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 1, _x)))
                                                                            path[not Is_a(Leaf, _x)]
                                                                            proof
                                                                            detailed proof
                                                                            ground_instances3
                                                                            definitions0
                                                                            inductions0
                                                                            search_time
                                                                            0.016s
                                                                            details
                                                                            Expand
                                                                            smt_stats
                                                                            num checks8
                                                                            arith assert lower12
                                                                            arith pivots9
                                                                            rlimit count9595
                                                                            mk clause16
                                                                            datatype occurs check12
                                                                            mk bool var73
                                                                            arith assert upper7
                                                                            datatype splits3
                                                                            decisions14
                                                                            arith add rows7
                                                                            propagations11
                                                                            conflicts6
                                                                            arith fixed eqs3
                                                                            datatype accessor ax13
                                                                            arith conflicts2
                                                                            datatype constructor ax11
                                                                            num allocs1694836857
                                                                            final checks4
                                                                            added eqs47
                                                                            del clause9
                                                                            arith eq adapter6
                                                                            memory19.780000
                                                                            max memory19.780000
                                                                            Expand
                                                                            • start[0.016s]
                                                                                not Is_a(Leaf, _x)
                                                                                && Ordinal.count _x >= 0 && Ordinal.count (Destruct(Node, 1, _x)) >= 0
                                                                                ==> Is_a(Leaf, Destruct(Node, 1, _x)) && Is_a(Leaf, Destruct(Node, 1, _x))
                                                                                    || Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))) Ordinal.<<
                                                                                       Ordinal.Int (Ordinal.count _x)
                                                                            • simplify
                                                                              into
                                                                              (not
                                                                               ((not Is_a(Leaf, _x) && Ordinal.count _x >= 0)
                                                                                && Ordinal.count (Destruct(Node, 1, _x)) >= 0)
                                                                               || Is_a(Leaf, Destruct(Node, 1, _x)))
                                                                              || Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))) Ordinal.<<
                                                                                 Ordinal.Int (Ordinal.count _x)
                                                                              expansions
                                                                              []
                                                                              rewrite_steps
                                                                                forward_chaining
                                                                                • unroll
                                                                                  expr
                                                                                  (|Ordinal.<<_121| (|Ordinal.Int_112|
                                                                                                      (|count_`int tree`_2598| (|get.Node.1_2555|…
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (|count_`int tree`_2598| (|get.Node.1_2555| _x_2587))
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (|count_`int tree`_2598| _x_2587)
                                                                                      expansions
                                                                                      • unsat
                                                                                        (let ((a!1 (ite (>= (|count_`int tree`_2598| (|get.Node.0_2554| _x_2587)) 0)
                                                                                                        (|count…

                                                                                      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.069s):
                                                                                       let x =
                                                                                         (Node
                                                                                            ((Node ((Leaf ((-7347))), (Leaf (4099)))),
                                                                                             (Node
                                                                                                ((Node ((Leaf ((-7523))), (Leaf (15358)))),
                                                                                                 (Node ((Leaf ((-9664))), (Leaf (5079))))))))
                                                                                      
                                                                                      Instance
                                                                                      proof attempt
                                                                                      ground_instances26
                                                                                      definitions0
                                                                                      inductions0
                                                                                      search_time
                                                                                      0.069s
                                                                                      details
                                                                                      Expand
                                                                                      smt_stats
                                                                                      arith offset eqs13
                                                                                      num checks53
                                                                                      arith assert lower462
                                                                                      arith patches_succ3
                                                                                      arith pivots428
                                                                                      rlimit count58306
                                                                                      mk clause546
                                                                                      datatype occurs check90
                                                                                      mk bool var2487
                                                                                      arith gcd tests25
                                                                                      arith assert upper339
                                                                                      datatype splits88
                                                                                      decisions949
                                                                                      arith add rows1376
                                                                                      arith bound prop4
                                                                                      propagations1645
                                                                                      arith patches6
                                                                                      interface eqs11
                                                                                      conflicts45
                                                                                      arith fixed eqs256
                                                                                      datatype accessor ax450
                                                                                      minimized lits4
                                                                                      arith conflicts9
                                                                                      arith assert diseq125
                                                                                      datatype constructor ax450
                                                                                      num allocs1801200462
                                                                                      final checks59
                                                                                      added eqs2911
                                                                                      del clause398
                                                                                      arith ineq splits3
                                                                                      arith eq adapter385
                                                                                      memory21.020000
                                                                                      max memory22.810000
                                                                                      Expand
                                                                                      • start[0.069s] size :var_0: >= 5 && size :var_0: = 3 * sum_tree :var_0:
                                                                                      • unroll
                                                                                        expr
                                                                                        (sum_tree_2581 x_2603)
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (size_2610 x_2603)
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (sum_tree_2581 (|get.Node.1_2609| x_2603))
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (sum_tree_2581 (|get.Node.0_2608| x_2603))
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (size_2610 (|get.Node.1_2609| x_2603))
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (size_2610 (|get.Node.0_2608| x_2603))
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (sum_tree_2581 (|get.Node.1_2609| (|get.Node.1_2609| x_2603)))
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (sum_tree_2581 (|get.Node.0_2608| (|get.Node.1_2609| x_2603)))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (sum_tree_2581 (|get.Node.1_2609| (|get.Node.0_2608| x_2603)))
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (sum_tree_2581 (|get.Node.0_2608| (|get.Node.0_2608| x_2603)))
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (size_2610 (|get.Node.1_2609| (|get.Node.1_2609| x_2603)))
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (size_2610 (|get.Node.0_2608| (|get.Node.1_2609| x_2603)))
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (size_2610 (|get.Node.1_2609| (|get.Node.0_2608| x_2603)))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (size_2610 (|get.Node.0_2608| (|get.Node.0_2608| x_2603)))
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (sum_tree_2581 (|get.Node.1_2609|
                                                                                                                                     (|get.Node.1_2609| (|get.Node.1_2609| x_2603))))
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (sum_tree_2581 (|get.Node.0_2608|
                                                                                                                                       (|get.Node.1_2609| (|get.Node.1_2609| x_2603))))
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (sum_tree_2581 (|get.Node.1_2609|
                                                                                                                                         (|get.Node.0_2608| (|get.Node.1_2609| x_2603))))
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (sum_tree_2581 (|get.Node.0_2608|
                                                                                                                                           (|get.Node.0_2608| (|get.Node.1_2609| x_2603))))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (sum_tree_2581 (|get.Node.0_2608|
                                                                                                                                             (|get.Node.1_2609| (|get.Node.0_2608| x_2603))))
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (sum_tree_2581 (|get.Node.1_2609|
                                                                                                                                               (|get.Node.1_2609| (|get.Node.0_2608| x_2603))))
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (sum_tree_2581 (|get.Node.1_2609|
                                                                                                                                                 (|get.Node.0_2608| (|get.Node.0_2608| x_2603))))
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (sum_tree_2581 (|get.Node.0_2608|
                                                                                                                                                   (|get.Node.0_2608| (|get.Node.0_2608| x_2603))))
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (size_2610 (|get.Node.1_2609| (|get.Node.1_2609| (|get.Node.1_2609| x_2603))))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (size_2610 (|get.Node.0_2608| (|get.Node.1_2609| (|get.Node.1_2609| x_2603))))
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (size_2610 (|get.Node.1_2609| (|get.Node.0_2608| (|get.Node.1_2609| x_2603))))
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (size_2610 (|get.Node.0_2608| (|get.Node.0_2608| (|get.Node.1_2609| x_2603))))
                                                                                                                                          expansions
                                                                                                                                          • Sat (Some let x = (Node ((Node ((Leaf ((-7347))), (Leaf (4099)))), (Node ((Node ((Leaf ((-7523))), (Leaf (15358)))), (Node ((Leaf ((-9664))), (Leaf (5079)))))))) )

                                                                                                                                          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 : int -> int -> int = <fun>
                                                                                                                                          File "jupyter cell 18", line 1, characters 0-105:
                                                                                                                                          Error: rejected definition for function ack, Imandra could not prove termination. 
                                                                                                                                          hint: problematic sub-call from `ack m n` to `ack m (n - 1)`  under path
                                                                                                                                          not (n <= 0) and not (m <= 0) is not decreasing (measured subset: (m))
                                                                                                                                          

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

                                                                                                                                          Termination proof

                                                                                                                                          call `ack (m - 1) 1` from `ack m n`
                                                                                                                                          originalack m n
                                                                                                                                          suback (m - 1) 1
                                                                                                                                          original ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if n >= 0 then n else 0)]
                                                                                                                                          sub ordinalOrdinal.of_list [Ordinal.Int (if (m - 1) >= 0 then m - 1 else 0); Ordinal.Int (if 1 >= 0 then 1 else 0)]
                                                                                                                                          path[n <= 0 && not (m <= 0)]
                                                                                                                                          proof
                                                                                                                                          detailed proof
                                                                                                                                          ground_instances5
                                                                                                                                          definitions2
                                                                                                                                          inductions0
                                                                                                                                          search_time
                                                                                                                                          0.022s
                                                                                                                                          details
                                                                                                                                          Expand
                                                                                                                                          smt_stats
                                                                                                                                          arith offset eqs13
                                                                                                                                          num checks12
                                                                                                                                          arith assert lower16
                                                                                                                                          arith pivots7
                                                                                                                                          rlimit count83653
                                                                                                                                          mk clause67
                                                                                                                                          datatype occurs check77
                                                                                                                                          mk bool var198
                                                                                                                                          arith assert upper44
                                                                                                                                          datatype splits8
                                                                                                                                          decisions87
                                                                                                                                          arith add rows12
                                                                                                                                          arith bound prop1
                                                                                                                                          propagations94
                                                                                                                                          conflicts20
                                                                                                                                          arith fixed eqs8
                                                                                                                                          datatype accessor ax28
                                                                                                                                          arith conflicts2
                                                                                                                                          arith assert diseq2
                                                                                                                                          datatype constructor ax15
                                                                                                                                          num allocs2054025659
                                                                                                                                          final checks8
                                                                                                                                          added eqs187
                                                                                                                                          del clause38
                                                                                                                                          arith eq adapter30
                                                                                                                                          memory27.390000
                                                                                                                                          max memory27.510000
                                                                                                                                          Expand
                                                                                                                                          • start[0.022s]
                                                                                                                                              n <= 0
                                                                                                                                              && not (m <= 0)
                                                                                                                                                 && (if m >= 0 then m else 0) >= 0
                                                                                                                                                    && (if n >= 0 then n else 0) >= 0
                                                                                                                                                       && (if (m - 1) >= 0 then m - 1 else 0) >= 0
                                                                                                                                                          && (if 1 >= 0 then 1 else 0) >= 0
                                                                                                                                              ==> not (1 <= 0 && not ((m - 1) <= 0))
                                                                                                                                                  && not (not (1 <= 0) && not ((m - 1) <= 0))
                                                                                                                                                     && not (not (1 <= 0) && not ((m - 1) <= 0))
                                                                                                                                                  || (if (Ordinal.Int (if (m - 1) >= 0 then m - 1 else 0)) :: … = …
                                                                                                                                                      then … else …)
                                                                                                                                                     Ordinal.<< …
                                                                                                                                          • simplify
                                                                                                                                            into
                                                                                                                                            (not
                                                                                                                                             ((((n <= 0 && not (m <= 0)) && (if m >= 0 then m else 0) >= 0)
                                                                                                                                               && (if n >= 0 then n else 0) >= 0)
                                                                                                                                              && (if m >= 1 then -1 + m else 0) >= 0)
                                                                                                                                             || m <= 1)
                                                                                                                                            || Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                               (Ordinal.Int 1) Ordinal.<<
                                                                                                                                               Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                               (Ordinal.Int (if n >= 0 then n else 0))
                                                                                                                                            expansions
                                                                                                                                            []
                                                                                                                                            rewrite_steps
                                                                                                                                              forward_chaining
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (|Ordinal.shift_146|
                                                                                                                                                  (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                  (|Ordinal.Int_112| 1))
                                                                                                                                                expansions
                                                                                                                                                Ordinal.zero
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                             (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                      …
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (|Ordinal.shift_146|
                                                                                                                                                    (|Ordinal.Int_112| (ite (>= m_2711 1) (+ (- 1) m_2711) 0))
                                                                                                                                                    (|Ordinal.Int_11…
                                                                                                                                                  expansions
                                                                                                                                                  Ordinal.zero
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                               (|Ordinal.Int_112| (ite (>= m_2711 1) (+ (- 1) m_2711) …
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                 (|Ordinal.Int_112| (ite (>= m_2711 1) (+ (- 1) m_2711) …
                                                                                                                                                    expansions
                                                                                                                                                    • unsat
                                                                                                                                                      (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                   (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                            …

                                                                                                                                                    call `ack (m - 1) (ack m (n - 1))` from `ack m n`
                                                                                                                                                    originalack m n
                                                                                                                                                    suback (m - 1) (ack m (n - 1))
                                                                                                                                                    original ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if n >= 0 then n else 0)]
                                                                                                                                                    sub ordinalOrdinal.of_list [Ordinal.Int (if (m - 1) >= 0 then m - 1 else 0); Ordinal.Int (if ack m (n - 1) >= 0 then ack m (n - 1) else 0)]
                                                                                                                                                    path[not (n <= 0) && not (m <= 0)]
                                                                                                                                                    proof
                                                                                                                                                    detailed proof
                                                                                                                                                    ground_instances5
                                                                                                                                                    definitions2
                                                                                                                                                    inductions0
                                                                                                                                                    search_time
                                                                                                                                                    0.030s
                                                                                                                                                    details
                                                                                                                                                    Expand
                                                                                                                                                    smt_stats
                                                                                                                                                    num checks12
                                                                                                                                                    arith assert lower72
                                                                                                                                                    arith pivots20
                                                                                                                                                    rlimit count77238
                                                                                                                                                    mk clause98
                                                                                                                                                    datatype occurs check98
                                                                                                                                                    mk bool var227
                                                                                                                                                    arith assert upper24
                                                                                                                                                    datatype splits8
                                                                                                                                                    decisions162
                                                                                                                                                    arith add rows21
                                                                                                                                                    arith bound prop2
                                                                                                                                                    propagations193
                                                                                                                                                    conflicts20
                                                                                                                                                    arith fixed eqs25
                                                                                                                                                    datatype accessor ax32
                                                                                                                                                    arith conflicts1
                                                                                                                                                    arith assert diseq4
                                                                                                                                                    datatype constructor ax18
                                                                                                                                                    num allocs1959982828
                                                                                                                                                    final checks8
                                                                                                                                                    added eqs209
                                                                                                                                                    del clause62
                                                                                                                                                    arith eq adapter29
                                                                                                                                                    memory27.350000
                                                                                                                                                    max memory27.510000
                                                                                                                                                    Expand
                                                                                                                                                    • start[0.030s]
                                                                                                                                                        not (n <= 0)
                                                                                                                                                        && not (m <= 0)
                                                                                                                                                           && (if m >= 0 then m else 0) >= 0
                                                                                                                                                              && (if n >= 0 then n else 0) >= 0
                                                                                                                                                                 && (if (m - 1) >= 0 then m - 1 else 0) >= 0
                                                                                                                                                                    && (if ack m (n - 1) >= 0 then ack m (n - 1) else 0) >= 0
                                                                                                                                                        ==> not (ack m (n - 1) <= 0 && not ((m - 1) <= 0))
                                                                                                                                                            && not (not (ack m (n - 1) <= 0) && not ((m - 1) <= 0))
                                                                                                                                                               && not (not (ack m (n - 1) <= 0) && not ((m - 1) <= 0))
                                                                                                                                                            || (if … then … else …) Ordinal.<< …
                                                                                                                                                    • simplify
                                                                                                                                                      into
                                                                                                                                                      (not
                                                                                                                                                       (((((not (n <= 0) && not (m <= 0)) && (if m >= 0 then m else 0) >= 0)
                                                                                                                                                          && (if n >= 0 then n else 0) >= 0)
                                                                                                                                                         && (if m >= 1 then -1 + m else 0) >= 0)
                                                                                                                                                        && (if ack m (-1 + n) >= 0 then ack m (-1 + n) else 0) >= 0)
                                                                                                                                                       || not (ack m (-1 + n) <= 0 && not (m <= 1))
                                                                                                                                                          && not (not (ack m (-1 + n) <= 0) && not (m <= 1)))
                                                                                                                                                      || Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                                         (Ordinal.Int (if ack m (-1 + n) >= 0 then ack m (-1 + n) else 0))
                                                                                                                                                         Ordinal.<<
                                                                                                                                                         Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                                         (Ordinal.Int (if n >= 0 then n else 0))
                                                                                                                                                      expansions
                                                                                                                                                      []
                                                                                                                                                      rewrite_steps
                                                                                                                                                        forward_chaining
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (|Ordinal.shift_146|
                                                                                                                                                            (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                            (|Ordinal.Int_112| 1))
                                                                                                                                                          expansions
                                                                                                                                                          Ordinal.zero
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                       (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                …
                                                                                                                                                          expansions
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (|Ordinal.shift_146|
                                                                                                                                                              (|Ordinal.Int_112| (ite (>= m_2711 1) (+ (- 1) m_2711) 0))
                                                                                                                                                              (|Ordinal.Int_11…
                                                                                                                                                            expansions
                                                                                                                                                            Ordinal.zero
                                                                                                                                                          • unroll
                                                                                                                                                            expr
                                                                                                                                                            (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                         (|Ordinal.Int_112| (ite (>= m_2711 1) (+ (- 1) m_2711) …
                                                                                                                                                            expansions
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                           (|Ordinal.Int_112| (ite (>= m_2711 1) (+ (- 1) m_2711) …
                                                                                                                                                              expansions
                                                                                                                                                              • unsat
                                                                                                                                                                (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                             (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                      …

                                                                                                                                                              call `ack m (n - 1)` from `ack m n`
                                                                                                                                                              originalack m n
                                                                                                                                                              suback m (n - 1)
                                                                                                                                                              original ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if n >= 0 then n else 0)]
                                                                                                                                                              sub ordinalOrdinal.of_list [Ordinal.Int (if m >= 0 then m else 0); Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0)]
                                                                                                                                                              path[not (n <= 0) && not (m <= 0)]
                                                                                                                                                              proof
                                                                                                                                                              detailed proof
                                                                                                                                                              ground_instances7
                                                                                                                                                              definitions1
                                                                                                                                                              inductions0
                                                                                                                                                              search_time
                                                                                                                                                              0.029s
                                                                                                                                                              details
                                                                                                                                                              Expand
                                                                                                                                                              smt_stats
                                                                                                                                                              arith offset eqs3
                                                                                                                                                              num checks16
                                                                                                                                                              arith assert lower22
                                                                                                                                                              arith pivots13
                                                                                                                                                              rlimit count69430
                                                                                                                                                              mk clause134
                                                                                                                                                              datatype occurs check175
                                                                                                                                                              mk bool var308
                                                                                                                                                              arith assert upper18
                                                                                                                                                              datatype splits23
                                                                                                                                                              decisions197
                                                                                                                                                              arith add rows22
                                                                                                                                                              arith bound prop2
                                                                                                                                                              propagations205
                                                                                                                                                              interface eqs1
                                                                                                                                                              conflicts21
                                                                                                                                                              arith fixed eqs15
                                                                                                                                                              datatype accessor ax52
                                                                                                                                                              arith conflicts1
                                                                                                                                                              arith assert diseq1
                                                                                                                                                              datatype constructor ax33
                                                                                                                                                              num allocs1903817411
                                                                                                                                                              final checks14
                                                                                                                                                              added eqs267
                                                                                                                                                              del clause94
                                                                                                                                                              arith eq adapter16
                                                                                                                                                              memory24.140000
                                                                                                                                                              max memory24.140000
                                                                                                                                                              Expand
                                                                                                                                                              • start[0.029s]
                                                                                                                                                                  not (n <= 0)
                                                                                                                                                                  && not (m <= 0)
                                                                                                                                                                     && (if m >= 0 then m else 0) >= 0
                                                                                                                                                                        && (if n >= 0 then n else 0) >= 0
                                                                                                                                                                           && (if m >= 0 then m else 0) >= 0
                                                                                                                                                                              && (if (n - 1) >= 0 then n - 1 else 0) >= 0
                                                                                                                                                                  ==> not ((n - 1) <= 0 && not (m <= 0))
                                                                                                                                                                      && not (not ((n - 1) <= 0) && not (m <= 0))
                                                                                                                                                                         && not (not ((n - 1) <= 0) && not (m <= 0))
                                                                                                                                                                      || (if [Ordinal.Int (if m >= 0 then m else 0);
                                                                                                                                                                              Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0)]
                                                                                                                                                                             = []
                                                                                                                                                                          then Ordinal.Int 0 else …)
                                                                                                                                                                         Ordinal.<< …
                                                                                                                                                              • simplify
                                                                                                                                                                into
                                                                                                                                                                (not
                                                                                                                                                                 ((((not (n <= 0) && not (m <= 0)) && (if m >= 0 then m else 0) >= 0)
                                                                                                                                                                   && (if n >= 0 then n else 0) >= 0)
                                                                                                                                                                  && (if n >= 1 then -1 + n else 0) >= 0)
                                                                                                                                                                 || not (n <= 1 && not (m <= 0)) && not (not (n <= 1) && not (m <= 0)))
                                                                                                                                                                || Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                                                   (Ordinal.Int (if n >= 1 then -1 + n else 0)) Ordinal.<<
                                                                                                                                                                   Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                                                   (Ordinal.Int (if n >= 0 then n else 0))
                                                                                                                                                                expansions
                                                                                                                                                                []
                                                                                                                                                                rewrite_steps
                                                                                                                                                                  forward_chaining
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                                 (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                          …
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (|Ordinal.shift_146|
                                                                                                                                                                        (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                        (|Ordinal.Int_112| 1))
                                                                                                                                                                      expansions
                                                                                                                                                                      Ordinal.zero
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                                   (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                            …
                                                                                                                                                                      expansions
                                                                                                                                                                      • unroll
                                                                                                                                                                        expr
                                                                                                                                                                        (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                                     (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                              …
                                                                                                                                                                        expansions
                                                                                                                                                                        • unroll
                                                                                                                                                                          expr
                                                                                                                                                                          (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                                       (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                                …
                                                                                                                                                                          expansions
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                                         (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                                  …
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                                           (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                                    …
                                                                                                                                                                              expansions
                                                                                                                                                                              • unsat
                                                                                                                                                                                (let ((a!1 (|Ordinal.shift_146|
                                                                                                                                                                                             (|Ordinal.Int_112| (ite (>= m_2711 0) m_2711 0))
                                                                                                                                                                                      …

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

                                                                                                                                                                              Measures and Ordinals

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

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

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

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

                                                                                                                                                                              In [20]:
                                                                                                                                                                              #show Ordinal
                                                                                                                                                                              
                                                                                                                                                                              Out[20]:
                                                                                                                                                                              module Ordinal :
                                                                                                                                                                                sig
                                                                                                                                                                                  type t = private Int of int | Cons of t * int * t
                                                                                                                                                                                  val pp : Format.formatter -> t -> unit
                                                                                                                                                                                  val of_int : int -> t
                                                                                                                                                                                  val ( ~$ ) : int -> t
                                                                                                                                                                                  val ( << ) : t -> t -> bool
                                                                                                                                                                                  val plus : t -> t -> t
                                                                                                                                                                                  val ( + ) : t -> t -> t
                                                                                                                                                                                  val of_list : t list -> t
                                                                                                                                                                                  val shift : t -> by:t -> t
                                                                                                                                                                                  val is_valid : t -> bool
                                                                                                                                                                                  val zero : t
                                                                                                                                                                                  val one : t
                                                                                                                                                                                  val omega : t
                                                                                                                                                                                  val omega_omega : t
                                                                                                                                                                                end
                                                                                                                                                                              

                                                                                                                                                                              Even though ordinals like $\omega$ are infinite, we may still compute with them in Imandra.

                                                                                                                                                                              In [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 -> int -> 'a list -> 'a list = <fun>
                                                                                                                                                                              File "jupyter cell 25", line 1, characters 0-96:
                                                                                                                                                                              Error: rejected definition for function left_pad,
                                                                                                                                                                              Imandra could not prove termination. 
                                                                                                                                                                              hint: problematic sub-call from `left_pad c n xs` to `left_pad c n (c :: xs)`
                                                                                                                                                                               under path not (List.length xs >= n) is not decreasing
                                                                                                                                                                              (measured subset: (xs))
                                                                                                                                                                              

                                                                                                                                                                              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 -> int -> 'a list -> 'a list = <fun>
                                                                                                                                                                              
                                                                                                                                                                              termination proof

                                                                                                                                                                              Termination proof

                                                                                                                                                                              call `left_pad c n (c :: xs)` from `left_pad c n xs`
                                                                                                                                                                              originalleft_pad c n xs
                                                                                                                                                                              subleft_pad c n (c :: xs)
                                                                                                                                                                              original ordinalleft_pad_measure n xs
                                                                                                                                                                              sub ordinalleft_pad_measure n (c :: xs)
                                                                                                                                                                              path[not (List.length xs >= n)]
                                                                                                                                                                              proof
                                                                                                                                                                              detailed proof
                                                                                                                                                                              ground_instances2
                                                                                                                                                                              definitions0
                                                                                                                                                                              inductions0
                                                                                                                                                                              search_time
                                                                                                                                                                              0.014s
                                                                                                                                                                              details
                                                                                                                                                                              Expand
                                                                                                                                                                              smt_stats
                                                                                                                                                                              num checks5
                                                                                                                                                                              arith assert lower8
                                                                                                                                                                              arith pivots5
                                                                                                                                                                              rlimit count88522
                                                                                                                                                                              mk clause7
                                                                                                                                                                              datatype occurs check16
                                                                                                                                                                              mk bool var36
                                                                                                                                                                              arith assert upper7
                                                                                                                                                                              datatype splits2
                                                                                                                                                                              decisions6
                                                                                                                                                                              arith add rows16
                                                                                                                                                                              propagations4
                                                                                                                                                                              conflicts3
                                                                                                                                                                              arith fixed eqs2
                                                                                                                                                                              datatype accessor ax5
                                                                                                                                                                              arith conflicts1
                                                                                                                                                                              datatype constructor ax2
                                                                                                                                                                              num allocs2226881815
                                                                                                                                                                              final checks4
                                                                                                                                                                              added eqs13
                                                                                                                                                                              del clause4
                                                                                                                                                                              arith eq adapter3
                                                                                                                                                                              memory28.300000
                                                                                                                                                                              max memory28.310000
                                                                                                                                                                              Expand
                                                                                                                                                                              • start[0.014s]
                                                                                                                                                                                  not (List.length xs >= n)
                                                                                                                                                                                  && (if (n - List.length xs) >= 0 then n - List.length xs else 0) >= 0
                                                                                                                                                                                     && (if (n - List.length (… :: xs)) >= 0
                                                                                                                                                                                         then n - List.length (… :: xs) else 0)
                                                                                                                                                                                        >= 0
                                                                                                                                                                                  ==> List.length (… :: xs) >= n
                                                                                                                                                                                      || Ordinal.Int
                                                                                                                                                                                         (if (n - List.length (… :: xs)) >= 0
                                                                                                                                                                                          then n - List.length (… :: xs) else 0)
                                                                                                                                                                                         Ordinal.<<
                                                                                                                                                                                         Ordinal.Int
                                                                                                                                                                                         (if (n - List.length xs) >= 0 then n - List.length xs else 0)
                                                                                                                                                                              • simplify
                                                                                                                                                                                into
                                                                                                                                                                                (not
                                                                                                                                                                                 ((not (List.length xs >= n)
                                                                                                                                                                                   && (if (n + -1 * List.length xs) >= 0 then n + -1 * List.length xs else 0)
                                                                                                                                                                                      >= 0)
                                                                                                                                                                                  && (if (n + -1 * List.length (c :: xs)) >= 0
                                                                                                                                                                                      then n + -1 * List.length (c :: xs) else 0)
                                                                                                                                                                                     >= 0)
                                                                                                                                                                                 || List.length (c :: xs) >= n)
                                                                                                                                                                                || Ordinal.Int
                                                                                                                                                                                   (if (n + -1 * List.length (c :: xs)) >= 0
                                                                                                                                                                                    then n + -1 * List.length (c :: xs) else 0)
                                                                                                                                                                                   Ordinal.<<
                                                                                                                                                                                   Ordinal.Int
                                                                                                                                                                                   (if (n + -1 * List.length xs) >= 0 then n + -1 * List.length xs else 0)
                                                                                                                                                                                expansions
                                                                                                                                                                                []
                                                                                                                                                                                rewrite_steps
                                                                                                                                                                                  forward_chaining
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (let ((a!1 (+ n_2835 (* (- 1) (|List.length_2831| (|::_3| c_2834 xs_2836)))))
                                                                                                                                                                                          (a!2 (>= (+ n_28…
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (|List.length_2831| (|::_3| c_2834 xs_2836))
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unsat
                                                                                                                                                                                        (let ((a!1 (+ (* (- 1) (|List.length_2831| (|::_3| c_2834 xs_2836))) n_2835))
                                                                                                                                                                                              (a!2 (<= (+ (|Li…

                                                                                                                                                                                      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 : 'a) ->
                                                                                                                                                                                       fun (n : int) ->
                                                                                                                                                                                        fun (xs : 'a list) ->
                                                                                                                                                                                         if List.length xs >= n then xs else left_pad c n (c :: xs)
                                                                                                                                                                                      def
                                                                                                                                                                                      nameleft_pad
                                                                                                                                                                                      type'a -> int -> 'a list -> 'a list
                                                                                                                                                                                      recursivetrue
                                                                                                                                                                                      call signatureleft_pad (c : 'a) (n : int) (xs : 'a list)
                                                                                                                                                                                      measured subset[n; xs]
                                                                                                                                                                                      parametrictrue
                                                                                                                                                                                      sub-function(s)
                                                                                                                                                                                      Expand
                                                                                                                                                                                      namemeasure_fun.left_pad
                                                                                                                                                                                      typeint -> 'b list -> Ordinal.t
                                                                                                                                                                                      recursivefalse
                                                                                                                                                                                      call signaturemeasure_fun.left_pad (n : int) (xs : 'b list)
                                                                                                                                                                                      body
                                                                                                                                                                                      left_pad_measure n xs
                                                                                                                                                                                      parametrictrue
                                                                                                                                                                                      validatedin 0.002s
                                                                                                                                                                                      locationjupyter cell 28:1,0--130
                                                                                                                                                                                      validatedin 0.059s
                                                                                                                                                                                      locationjupyter cell 28:1,0--130
                                                                                                                                                                                      hashes
                                                                                                                                                                                      left_pad9cfbc821149d2795b6f1e144858661801abf63fa1c6ef5afb79da741f113b5e2

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