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?
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/

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

In [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.014s
details
Expand
smt_stats
num checks7
arith assert lower5
arith pivots3
rlimit count1817
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 allocs933581
final checks6
added eqs33
del clause1
arith eq adapter3
memory5.900000
max memory5.900000
Expand
  • start[0.014s]
      not (xs = []) && Ordinal.count xs >= 0 && Ordinal.count (List.tl xs) >= 0
      ==> List.tl xs = []
          || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl xs)))
             (Ordinal.Int (Ordinal.count xs))
  • simplify
    into
    (not
     ((not (xs = []) && Ordinal.count xs >= 0) && Ordinal.count (List.tl xs) >= 0)
     || List.tl xs = [])
    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl xs)))
       (Ordinal.Int (Ordinal.count xs))
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_1 list`_1112|
                                              …
        expansions
        • unroll
          expr
          (|count_`ty_1 list`_1112| (|get.::.1_1095| xs_1103))
          expansions
          • unroll
            expr
            (|count_`ty_1 list`_1112| xs_1103)
            expansions
            • unsat
              (let ((a!1 (= (|count_`ty_1 list`_1112| xs_1103)
                            (+ 1 (|count_`ty_1 list`_1112| (|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.014s
            details
            Expand
            smt_stats
            num checks8
            arith assert lower17
            arith pivots10
            rlimit count2400
            mk clause19
            datatype occurs check21
            mk bool var79
            arith assert upper12
            datatype splits3
            decisions13
            arith add rows16
            arith bound prop1
            propagations13
            conflicts9
            arith fixed eqs7
            datatype accessor ax5
            arith conflicts2
            datatype constructor ax8
            num allocs2898972
            final checks6
            added eqs47
            del clause7
            arith eq adapter10
            memory9.490000
            max memory9.490000
            Expand
            • start[0.014s]
                not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
                ==> List.tl _x = []
                    || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                       (Ordinal.Int (Ordinal.count _x))
            • simplify
              into
              (not
               ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0)
               || List.tl _x = [])
              || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
                 (Ordinal.Int (Ordinal.count _x))
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`int list`_1131|
                                                        (…
                  expansions
                  • unroll
                    expr
                    (|count_`int list`_1131| (|get.::.1_1121| _x_1122))
                    expansions
                    • unroll
                      expr
                      (|count_`int list`_1131| _x_1122)
                      expansions
                      • unsat
                        (let ((a!1 (>= (ite (>= (|get.::.0_1120| _x_1122) 0)
                                            (|get.::.0_1120| _x_1122)
                         …

                      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.010s
                      details
                      Expand
                      smt_stats
                      num checks3
                      arith assert lower8
                      arith pivots2
                      rlimit count1027
                      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 allocs7576567
                      final checks1
                      added eqs6
                      del clause4
                      arith eq adapter2
                      memory9.910000
                      max memory9.910000
                      Expand
                      • start[0.010s]
                          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.( << ) (Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0))
                                 (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.( << ) (Ordinal.Int (if x >= 1 then -1 + x else 0))
                           (Ordinal.Int (if x >= 0 then x else 0))
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_102| (|Ordinal.Int_93| (ite (>= x_1135 1) (+ (- 1) x_1135) 0))
                                              (|Ordi…
                            expansions
                            • unsat
                              (let ((a!1 (not (= x_1135 (ite (>= x_1135 0) x_1135 0))))
                                    (a!2 (+ x_1135 (* (- 1) (ite (>= x_1…

                            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))
                            See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
                            

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

                            Structural Recursions

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

                            In [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.011s
                            details
                            Expand
                            smt_stats
                            num checks8
                            arith assert lower11
                            arith pivots9
                            rlimit count4468
                            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 allocs27479179
                            final checks4
                            added eqs47
                            del clause9
                            arith eq adapter6
                            memory13.700000
                            max memory13.700000
                            Expand
                            • start[0.011s]
                                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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))))
                                       (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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))))
                                 (Ordinal.Int (Ordinal.count _x))
                              expansions
                              []
                              rewrite_steps
                                forward_chaining
                                • unroll
                                  expr
                                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 tree`_1185|
                                                                        …
                                  expansions
                                  • unroll
                                    expr
                                    (|count_`ty_0 tree`_1185| (|get.Node.0_1168| _x_1174))
                                    expansions
                                    • unroll
                                      expr
                                      (|count_`ty_0 tree`_1185| _x_1174)
                                      expansions
                                      • unsat
                                        (let ((a!1 (ite (>= (|count_`ty_0 tree`_1185| (|get.Node.1_1169| _x_1174)) 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.011s
                                      details
                                      Expand
                                      smt_stats
                                      num checks8
                                      arith assert lower11
                                      arith pivots9
                                      rlimit count2234
                                      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 allocs22494930
                                      final checks4
                                      added eqs47
                                      del clause9
                                      arith eq adapter6
                                      memory10.800000
                                      max memory13.550000
                                      Expand
                                      • start[0.011s]
                                          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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))))
                                                 (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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))))
                                           (Ordinal.Int (Ordinal.count _x))
                                        expansions
                                        []
                                        rewrite_steps
                                          forward_chaining
                                          • unroll
                                            expr
                                            (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`ty_0 tree`_1185|
                                                                                  …
                                            expansions
                                            • unroll
                                              expr
                                              (|count_`ty_0 tree`_1185| (|get.Node.1_1169| _x_1174))
                                              expansions
                                              • unroll
                                                expr
                                                (|count_`ty_0 tree`_1185| _x_1174)
                                                expansions
                                                • unsat
                                                  (let ((a!1 (ite (>= (|count_`ty_0 tree`_1185| (|get.Node.0_1168| _x_1174)) 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 : int tree end
                                                
                                                Instance (after 9 steps, 0.021s):
                                                 let (x : int tree) =
                                                   (Node
                                                      ((Node ((Leaf (9)), (Leaf (8)))),
                                                       (Node ((Leaf (7)), (Node ((Leaf (10)), (Leaf (11))))))))
                                                
                                                Instance
                                                proof attempt
                                                ground_instances9
                                                definitions0
                                                inductions0
                                                search_time
                                                0.021s
                                                details
                                                Expand
                                                smt_stats
                                                arith offset eqs2
                                                num checks19
                                                arith assert lower134
                                                arith pivots73
                                                rlimit count11137
                                                mk clause168
                                                datatype occurs check17
                                                mk bool var725
                                                arith assert upper83
                                                datatype splits36
                                                decisions132
                                                arith add rows204
                                                arith bound prop7
                                                propagations401
                                                interface eqs4
                                                conflicts23
                                                arith fixed eqs26
                                                datatype accessor ax135
                                                arith conflicts6
                                                arith assert diseq52
                                                datatype constructor ax135
                                                num allocs34946674
                                                final checks22
                                                added eqs724
                                                del clause101
                                                arith eq adapter95
                                                memory17.290000
                                                max memory17.290000
                                                Expand
                                                • start[0.021s] size :var_0: = 5
                                                • unroll
                                                  expr
                                                  (size_1195 x_45)
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (size_1195 (|get.Node.1_1194| x_45))
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (size_1195 (|get.Node.0_1193| x_45))
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (size_1195 (|get.Node.1_1194| (|get.Node.1_1194| x_45)))
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (size_1195 (|get.Node.0_1193| (|get.Node.1_1194| x_45)))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (size_1195 (|get.Node.1_1194| (|get.Node.0_1193| x_45)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (size_1195 (|get.Node.0_1193| (|get.Node.0_1193| x_45)))
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (size_1195 (|get.Node.1_1194| (|get.Node.1_1194| (|get.Node.1_1194| x_45))))
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (size_1195 (|get.Node.0_1193| (|get.Node.1_1194| (|get.Node.1_1194| x_45))))
                                                                  expansions
                                                                  • Sat (Some let (x : int tree) = (Node ((Node ((Leaf (9)), (Leaf (8)))), (Node ((Leaf (7)), (Node ((Leaf (10)), (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.013s
                                                                  details
                                                                  Expand
                                                                  smt_stats
                                                                  num checks8
                                                                  arith assert lower11
                                                                  arith pivots9
                                                                  rlimit count4704
                                                                  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 allocs68596021
                                                                  final checks4
                                                                  added eqs47
                                                                  del clause9
                                                                  arith eq adapter6
                                                                  memory14.780000
                                                                  max memory17.570000
                                                                  Expand
                                                                  • start[0.013s]
                                                                      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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))))
                                                                             (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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 0, _x))))
                                                                       (Ordinal.Int (Ordinal.count _x))
                                                                    expansions
                                                                    []
                                                                    rewrite_steps
                                                                      forward_chaining
                                                                      • unroll
                                                                        expr
                                                                        (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`int tree`_1234|
                                                                                                              (…
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|count_`int tree`_1234| (|get.Node.0_1221| _x_1223))
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|count_`int tree`_1234| _x_1223)
                                                                            expansions
                                                                            • unsat
                                                                              (let ((a!1 (ite (>= (|count_`int tree`_1234| (|get.Node.1_1222| _x_1223)) 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.013s
                                                                            details
                                                                            Expand
                                                                            smt_stats
                                                                            num checks8
                                                                            arith assert lower11
                                                                            arith pivots9
                                                                            rlimit count2352
                                                                            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 allocs53861525
                                                                            final checks4
                                                                            added eqs47
                                                                            del clause9
                                                                            arith eq adapter6
                                                                            memory14.700000
                                                                            max memory17.290000
                                                                            Expand
                                                                            • start[0.013s]
                                                                                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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))))
                                                                                       (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.( << ) (Ordinal.Int (Ordinal.count (Destruct(Node, 1, _x))))
                                                                                 (Ordinal.Int (Ordinal.count _x))
                                                                              expansions
                                                                              []
                                                                              rewrite_steps
                                                                                forward_chaining
                                                                                • unroll
                                                                                  expr
                                                                                  (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_`int tree`_1234|
                                                                                                                        (…
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (|count_`int tree`_1234| (|get.Node.1_1222| _x_1223))
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (|count_`int tree`_1234| _x_1223)
                                                                                      expansions
                                                                                      • unsat
                                                                                        (let ((a!1 (ite (>= (|count_`int tree`_1234| (|get.Node.0_1221| _x_1223)) 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 : int tree end
                                                                                      
                                                                                      Instance (after 26 steps, 0.053s):
                                                                                       let (x : int tree) =
                                                                                         (Node
                                                                                            ((Node ((Leaf ((-4812))), (Leaf (6652)))),
                                                                                             (Node
                                                                                                ((Node ((Leaf ((-11210))), (Leaf ((-2997))))),
                                                                                                 (Node ((Leaf (6202)), (Leaf (6167))))))))
                                                                                      
                                                                                      Instance
                                                                                      proof attempt
                                                                                      ground_instances26
                                                                                      definitions0
                                                                                      inductions0
                                                                                      search_time
                                                                                      0.053s
                                                                                      details
                                                                                      Expand
                                                                                      smt_stats
                                                                                      arith offset eqs14
                                                                                      num checks53
                                                                                      arith assert lower512
                                                                                      arith patches_succ3
                                                                                      arith pivots446
                                                                                      rlimit count59302
                                                                                      mk clause594
                                                                                      datatype occurs check94
                                                                                      mk bool var2763
                                                                                      arith gcd tests20
                                                                                      arith assert upper365
                                                                                      datatype splits100
                                                                                      decisions981
                                                                                      arith add rows1413
                                                                                      arith bound prop8
                                                                                      propagations1905
                                                                                      arith patches4
                                                                                      interface eqs9
                                                                                      conflicts57
                                                                                      arith fixed eqs266
                                                                                      datatype accessor ax517
                                                                                      minimized lits6
                                                                                      arith conflicts9
                                                                                      arith assert diseq147
                                                                                      datatype constructor ax517
                                                                                      num allocs80763776
                                                                                      final checks57
                                                                                      added eqs3313
                                                                                      del clause421
                                                                                      arith ineq splits1
                                                                                      arith eq adapter437
                                                                                      memory18.830000
                                                                                      max memory18.830000
                                                                                      Expand
                                                                                      • start[0.053s] size :var_0: >= 5 && size :var_0: = 3 * sum_tree :var_0:
                                                                                      • unroll
                                                                                        expr
                                                                                        (sum_tree_47 x_52)
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (size_1244 x_52)
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (sum_tree_47 (|get.Node.1_1243| x_52))
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (sum_tree_47 (|get.Node.0_1242| x_52))
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (size_1244 (|get.Node.1_1243| x_52))
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (size_1244 (|get.Node.0_1242| x_52))
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (sum_tree_47 (|get.Node.1_1243| (|get.Node.1_1243| x_52)))
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (sum_tree_47 (|get.Node.0_1242| (|get.Node.1_1243| x_52)))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (sum_tree_47 (|get.Node.1_1243| (|get.Node.0_1242| x_52)))
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (sum_tree_47 (|get.Node.0_1242| (|get.Node.0_1242| x_52)))
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (size_1244 (|get.Node.1_1243| (|get.Node.1_1243| x_52)))
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (size_1244 (|get.Node.0_1242| (|get.Node.1_1243| x_52)))
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (size_1244 (|get.Node.1_1243| (|get.Node.0_1242| x_52)))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (size_1244 (|get.Node.0_1242| (|get.Node.0_1242| x_52)))
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (sum_tree_47 (|get.Node.1_1243| (|get.Node.1_1243| (|get.Node.1_1243| x_52))))
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (sum_tree_47 (|get.Node.0_1242| (|get.Node.1_1243| (|get.Node.1_1243| x_52))))
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (sum_tree_47 (|get.Node.1_1243| (|get.Node.0_1242| (|get.Node.1_1243| x_52))))
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (sum_tree_47 (|get.Node.0_1242| (|get.Node.0_1242| (|get.Node.1_1243| x_52))))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (sum_tree_47 (|get.Node.1_1243| (|get.Node.1_1243| (|get.Node.0_1242| x_52))))
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (sum_tree_47 (|get.Node.0_1242| (|get.Node.1_1243| (|get.Node.0_1242| x_52))))
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (sum_tree_47 (|get.Node.1_1243| (|get.Node.0_1242| (|get.Node.0_1242| x_52))))
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (sum_tree_47 (|get.Node.0_1242| (|get.Node.0_1242| (|get.Node.0_1242| x_52))))
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (size_1244 (|get.Node.1_1243| (|get.Node.1_1243| (|get.Node.1_1243| x_52))))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (size_1244 (|get.Node.0_1242| (|get.Node.1_1243| (|get.Node.1_1243| x_52))))
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (size_1244 (|get.Node.1_1243| (|get.Node.0_1242| (|get.Node.1_1243| x_52))))
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (size_1244 (|get.Node.0_1242| (|get.Node.0_1242| (|get.Node.1_1243| x_52))))
                                                                                                                                          expansions
                                                                                                                                          • Sat (Some let (x : int tree) = (Node ((Node ((Leaf ((-4812))), (Leaf (6652)))), (Node ((Node ((Leaf ((-11210))), (Leaf ((-2997))))), (Node ((Leaf (6202)), (Leaf (6167)))))))) )

                                                                                                                                          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))
                                                                                                                                          See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
                                                                                                                                          

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

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

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

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

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

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

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

                                                                                                                                          In [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
                                                                                                                                          definitions0
                                                                                                                                          inductions0
                                                                                                                                          search_time
                                                                                                                                          0.016s
                                                                                                                                          details
                                                                                                                                          Expand
                                                                                                                                          smt_stats
                                                                                                                                          arith offset eqs12
                                                                                                                                          num checks12
                                                                                                                                          arith assert lower19
                                                                                                                                          arith pivots9
                                                                                                                                          rlimit count26618
                                                                                                                                          mk clause76
                                                                                                                                          datatype occurs check77
                                                                                                                                          mk bool var215
                                                                                                                                          arith assert upper42
                                                                                                                                          datatype splits8
                                                                                                                                          decisions114
                                                                                                                                          arith add rows15
                                                                                                                                          propagations118
                                                                                                                                          conflicts21
                                                                                                                                          arith fixed eqs8
                                                                                                                                          datatype accessor ax31
                                                                                                                                          arith conflicts3
                                                                                                                                          arith assert diseq5
                                                                                                                                          datatype constructor ax18
                                                                                                                                          num allocs159659460
                                                                                                                                          final checks8
                                                                                                                                          added eqs225
                                                                                                                                          del clause21
                                                                                                                                          arith eq adapter33
                                                                                                                                          memory25.690000
                                                                                                                                          max memory25.710000
                                                                                                                                          Expand
                                                                                                                                          • start[0.016s]
                                                                                                                                              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))
                                                                                                                                                  || Ordinal.( << )
                                                                                                                                                     (if (Ordinal.Int (if (m - 1) >= 0 then m - 1 else 0)) :: … = …
                                                                                                                                                      then … else …)
                                                                                                                                                     …
                                                                                                                                          • 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.( << )
                                                                                                                                               (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                                (Ordinal.Int 1))
                                                                                                                                               (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_127|
                                                                                                                                                  (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                  (|Ordinal.Int_93| 1))
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                               (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                         …
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (|Ordinal.shift_127|
                                                                                                                                                      (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0))
                                                                                                                                                      (|Ordinal.Int_93|…
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                   (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0…
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                     (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0…
                                                                                                                                                        expansions
                                                                                                                                                        • unsat
                                                                                                                                                          (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                       (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 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
                                                                                                                                                        definitions0
                                                                                                                                                        inductions0
                                                                                                                                                        search_time
                                                                                                                                                        0.016s
                                                                                                                                                        details
                                                                                                                                                        Expand
                                                                                                                                                        smt_stats
                                                                                                                                                        num checks12
                                                                                                                                                        arith assert lower72
                                                                                                                                                        arith pivots20
                                                                                                                                                        rlimit count19802
                                                                                                                                                        mk clause94
                                                                                                                                                        datatype occurs check98
                                                                                                                                                        mk bool var229
                                                                                                                                                        arith assert upper25
                                                                                                                                                        datatype splits8
                                                                                                                                                        decisions129
                                                                                                                                                        arith add rows23
                                                                                                                                                        arith bound prop1
                                                                                                                                                        propagations172
                                                                                                                                                        conflicts21
                                                                                                                                                        arith fixed eqs24
                                                                                                                                                        datatype accessor ax31
                                                                                                                                                        arith conflicts2
                                                                                                                                                        arith assert diseq3
                                                                                                                                                        datatype constructor ax17
                                                                                                                                                        num allocs144377457
                                                                                                                                                        final checks8
                                                                                                                                                        added eqs189
                                                                                                                                                        del clause38
                                                                                                                                                        arith eq adapter28
                                                                                                                                                        memory22.630000
                                                                                                                                                        max memory25.710000
                                                                                                                                                        Expand
                                                                                                                                                        • start[0.016s]
                                                                                                                                                            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))
                                                                                                                                                                || Ordinal.( << ) (if … then … else …) …
                                                                                                                                                        • 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.( << )
                                                                                                                                                             (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.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_127|
                                                                                                                                                                (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                (|Ordinal.Int_93| 1))
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                             (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                       …
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (|Ordinal.shift_127|
                                                                                                                                                                    (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0))
                                                                                                                                                                    (|Ordinal.Int_93|…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                 (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0…
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                   (|Ordinal.Int_93| (ite (>= m_1337 1) (+ (- 1) m_1337) 0…
                                                                                                                                                                      expansions
                                                                                                                                                                      • unsat
                                                                                                                                                                        (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                     (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 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_instances8
                                                                                                                                                                      definitions0
                                                                                                                                                                      inductions0
                                                                                                                                                                      search_time
                                                                                                                                                                      0.023s
                                                                                                                                                                      details
                                                                                                                                                                      Expand
                                                                                                                                                                      smt_stats
                                                                                                                                                                      arith offset eqs3
                                                                                                                                                                      num checks18
                                                                                                                                                                      arith assert lower27
                                                                                                                                                                      arith pivots18
                                                                                                                                                                      rlimit count12328
                                                                                                                                                                      mk clause184
                                                                                                                                                                      datatype occurs check211
                                                                                                                                                                      mk bool var392
                                                                                                                                                                      arith assert upper27
                                                                                                                                                                      datatype splits31
                                                                                                                                                                      decisions263
                                                                                                                                                                      arith add rows28
                                                                                                                                                                      arith bound prop2
                                                                                                                                                                      propagations278
                                                                                                                                                                      interface eqs1
                                                                                                                                                                      conflicts24
                                                                                                                                                                      arith fixed eqs18
                                                                                                                                                                      datatype accessor ax65
                                                                                                                                                                      arith conflicts1
                                                                                                                                                                      arith assert diseq6
                                                                                                                                                                      datatype constructor ax46
                                                                                                                                                                      num allocs108621755
                                                                                                                                                                      final checks16
                                                                                                                                                                      added eqs352
                                                                                                                                                                      del clause84
                                                                                                                                                                      arith eq adapter23
                                                                                                                                                                      memory25.710000
                                                                                                                                                                      max memory25.710000
                                                                                                                                                                      Expand
                                                                                                                                                                      • start[0.023s]
                                                                                                                                                                          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))
                                                                                                                                                                              || Ordinal.( << )
                                                                                                                                                                                 (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 …)
                                                                                                                                                                                 …
                                                                                                                                                                      • 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.( << )
                                                                                                                                                                           (Ordinal.plus (Ordinal.shift (Ordinal.Int …) (Ordinal.Int 1))
                                                                                                                                                                            (Ordinal.Int (if n >= 1 then -1 + n else 0)))
                                                                                                                                                                           (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_127|
                                                                                                                                                                                         (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                   …
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (|Ordinal.shift_127|
                                                                                                                                                                                (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                (|Ordinal.Int_93| 1))
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                             (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                       …
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                               (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                         …
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                                 (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                           …
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                                   (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                             …
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                                     (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                               …
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • unroll
                                                                                                                                                                                          expr
                                                                                                                                                                                          (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                                       (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 0))
                                                                                                                                                                                                 …
                                                                                                                                                                                          expansions
                                                                                                                                                                                          • unsat
                                                                                                                                                                                            (let ((a!1 (|Ordinal.shift_127|
                                                                                                                                                                                                         (|Ordinal.Int_93| (ite (>= m_1337 0) m_1337 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 = Int of int | Cons of t * int * t
                                                                                                                                                                                              val pp : Format.formatter -> t -> unit
                                                                                                                                                                                              val of_int : int -> t
                                                                                                                                                                                              val ( ~$ ) : int -> t
                                                                                                                                                                                              val ( << ) : t -> t -> bool
                                                                                                                                                                                              val plus : t -> t -> t
                                                                                                                                                                                              val simple_plus : t -> t -> t
                                                                                                                                                                                              val ( + ) : t -> t -> t
                                                                                                                                                                                              val of_list : t list -> t
                                                                                                                                                                                              val pair : t -> t -> t
                                                                                                                                                                                              val 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))
                                                                                                                                                                                          See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
                                                                                                                                                                                          

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

                                                                                                                                                                                          In [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.013s
                                                                                                                                                                                          details
                                                                                                                                                                                          Expand
                                                                                                                                                                                          smt_stats
                                                                                                                                                                                          num checks5
                                                                                                                                                                                          arith assert lower10
                                                                                                                                                                                          arith pivots5
                                                                                                                                                                                          rlimit count1781
                                                                                                                                                                                          mk clause7
                                                                                                                                                                                          datatype occurs check16
                                                                                                                                                                                          mk bool var36
                                                                                                                                                                                          arith assert upper5
                                                                                                                                                                                          datatype splits2
                                                                                                                                                                                          decisions6
                                                                                                                                                                                          arith add rows13
                                                                                                                                                                                          propagations4
                                                                                                                                                                                          conflicts3
                                                                                                                                                                                          arith fixed eqs2
                                                                                                                                                                                          datatype accessor ax5
                                                                                                                                                                                          arith conflicts1
                                                                                                                                                                                          datatype constructor ax2
                                                                                                                                                                                          num allocs237078548
                                                                                                                                                                                          final checks4
                                                                                                                                                                                          added eqs13
                                                                                                                                                                                          del clause4
                                                                                                                                                                                          arith eq adapter3
                                                                                                                                                                                          memory27.370000
                                                                                                                                                                                          max memory27.370000
                                                                                                                                                                                          Expand
                                                                                                                                                                                          • start[0.013s]
                                                                                                                                                                                              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.( << )
                                                                                                                                                                                                     (Ordinal.Int
                                                                                                                                                                                                      (if (n - List.length (… :: xs)) >= 0
                                                                                                                                                                                                       then n - List.length (… :: xs) else 0))
                                                                                                                                                                                                     (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.( << )
                                                                                                                                                                                               (Ordinal.Int
                                                                                                                                                                                                (if (n + -1 * List.length (c :: xs)) >= 0
                                                                                                                                                                                                 then n + -1 * List.length (c :: xs) else 0))
                                                                                                                                                                                               (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_1469 (* (- 1) (|List.length_1465| (|::_3| c_1468 xs_1470)))))
                                                                                                                                                                                                      (a!2 (>= (+ n_14…
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • unroll
                                                                                                                                                                                                  expr
                                                                                                                                                                                                  (|List.length_1465| (|::_3| c_1468 xs_1470))
                                                                                                                                                                                                  expansions
                                                                                                                                                                                                  • unsat
                                                                                                                                                                                                    (let ((a!1 (+ n_1469 (* (- 1) (|List.length_1465| (|::_3| c_1468 xs_1470)))))
                                                                                                                                                                                                          (a!5 (>= (+ n_14…

                                                                                                                                                                                                  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.001s
                                                                                                                                                                                                  locationjupyter cell 28:1,0--130
                                                                                                                                                                                                  validatedin 0.024s
                                                                                                                                                                                                  locationjupyter cell 28:1,0--130
                                                                                                                                                                                                  hashes
                                                                                                                                                                                                  left_pad0b49e24ef04bcf995b0047befe1e9e023e51eb42a971f82bb18ae5b0584bc592
                                                                                                                                                                                                  measure_fun.left_pad524fd3e52e9e7db867b10ee347a05d1d4c23e942f215ddd919b8262369e74e4e

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