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 -> int = <fun>
File "jupyter cell 1", line 1, characters 0-21Error: 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 (_cnt xs)
sub ordinalOrdinal.Int (_cnt (List.tl xs))
path[not Is_a([], xs)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.035s
details
Expand
smt_stats
num checks7
arith-make-feasible7
arith-max-columns10
rlimit count1551
arith-cheap-eqs1
mk clause11
datatype occurs check12
mk bool var36
arith-lower4
datatype splits1
decisions4
propagations6
arith-max-rows2
conflicts3
datatype accessor ax7
datatype constructor ax5
num allocs688530
final checks4
added eqs26
del clause9
arith eq adapter3
arith-upper5
memory5.220000
max memory5.220000
Expand
  • start[0.035s]
      let (_x_0 : int) = count.list (const 0) xs in
      let (_x_1 : ty_1 list) = List.tl xs in
      let (_x_2 : int) = count.list (const 0) _x_1 in
      not Is_a([], xs) && _x_0 >= 0 && _x_2 >= 0
      ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into
    let (_x_0 : ty_1 list) = List.tl xs in
    let (_x_1 : int) = count.list (const 0) _x_0 in
    let (_x_2 : int) = count.list (const 0) xs in
    (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
    || not ((not Is_a([], xs) && _x_2 >= 0) && _x_1 >= 0)
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|`count.list (const 0)[0]`_1710| xs_1699)
        expansions
        • unroll
          expr
          (|`count.list (const 0)[0]`_1710| (|get.::.1_1691| xs_1699))
          expansions
          • unroll
            expr
            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                (|`count.list (const 0)[0]`_1710| (|get.::.…
            expansions
            • Unsat

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

            ordinals

            Before we do so, let's return to that function f that Imandra rejected.

            Inconsistent non-terminating functions

            Imagine if Imandra allowed every possible recursive function to be admitted into its logic, even those that didn't terminate. If that were the case, we could easily define the following function:

            let rec f x = f x + 1 (note the binding strength of f, i.e., this is equivalent to let rec f x = (f x) + 1)

            With this function admitted, we could then use its defining equation f x = f x + 1 to derive a contradiction, e.g., by subtracting f x from both sides to derive 0 = 1:

            f x       = f x + 1
            f x - f x = f x + 1 - f x  
            0         = 1
            

            This inconsistency arises because, actually, such a function f cannot "exist"!

            You may be wondering: Why does consistency matter?

            Soundness, Consistency and Conservative Extensions

            Imandra is both a programming language and a logic. A crucial property of a logic is soundness. For a logic to be sound, every theorem provable in the logic must be true. An unsound theorem prover would be of little use!

            As we're developing programs and reasoning about them in Imandra, we're extending Imandra's logical world by defining types, functions, modules, and proving theorems. At any given time, this collection of all definitions and theorems is referred to as Imandra's current theory. It's important to ensure this current theory T is consistent, i.e., that there exists no statement P such that both P and (not P) are provable from T. If we weren't sure if T were consistent, then we would never know if a "theorem" was provable because it was true, or simply because T proves false (and false implies everything!).

            Imandra's definitional principle is designed to ensure this consistency, by enforcing certain restrictions on our definitions. In the parlance of mathematical logic, Imandra's definitional principle ensures that every definitional extension of Imandra's current theory is a conservative extension.

            There are two main rules Imandra enforces for ensuring consistency:

            • Every defined type must be well-founded.
            • Every defined function must be total (i.e., terminating on all possible inputs).

            In this notebook, we'll focus on the latter: proving program termination!

            Termination ensures existence

            Thankfully, a deep theorem of mathematical logic tells us that admitting terminating (also known as total) functions cannot lead us to inconsistency.

            To admit a new function into Imandra's logic, Imandra must be able to prove that it always terminates. For most common patterns of recursion, Imandra is able to prove termination automatically. For others, users may need to give Imandra help in the form of hints and measures.

            Let's get our hands dirty

            Let's define a few functions and see what this is like. First, let's observe that non-recursive functions are always admissible (provided we're not dealing with redefinition):

            In [3]:
            let k x y z = if x > y then x + y else z - 1
            
            Out[3]:
            val k : int -> int -> int -> int = <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 : int list -> int = <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 (_cnt _x)
            sub ordinalOrdinal.Int (_cnt (List.tl _x))
            path[not Is_a([], _x)]
            proof
            detailed proof
            ground_instances3
            definitions0
            inductions0
            search_time
            0.015s
            details
            Expand
            smt_stats
            num checks8
            arith-make-feasible18
            arith-max-columns16
            arith-conflicts2
            rlimit count2024
            mk clause20
            datatype occurs check12
            mk bool var56
            arith-lower15
            arith-diseq1
            datatype splits1
            decisions15
            propagations14
            arith-max-rows4
            conflicts7
            datatype accessor ax7
            datatype constructor ax5
            num allocs2669778
            final checks4
            added eqs38
            del clause13
            arith eq adapter10
            arith-upper12
            memory5.640000
            max memory5.640000
            Expand
            • start[0.015s]
                let (_x_0 : int) = count.list mk_nat _x in
                let (_x_1 : int list) = List.tl _x in
                let (_x_2 : int) = count.list mk_nat _x_1 in
                not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
                ==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
            • simplify
              into
              let (_x_0 : int list) = List.tl _x in
              let (_x_1 : int) = count.list mk_nat _x_0 in
              let (_x_2 : int) = count.list mk_nat _x in
              (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
              || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0)
              expansions
              []
              rewrite_steps
                forward_chaining
                • unroll
                  expr
                  (|`count.list mk_nat[0]`_1756| _x_1745)
                  expansions
                  • unroll
                    expr
                    (|`count.list mk_nat[0]`_1756| (|get.::.1_1744| _x_1745))
                    expansions
                    • unroll
                      expr
                      (|Ordinal.<<_126| (|Ordinal.Int_111|
                                          (|`count.list mk_nat[0]`_1756| (|get.::.1_1…
                      expansions
                      • Unsat

                      In [5]:
                      sum_lst [1;2;3]
                      
                      Out[5]:
                      - : int = 6
                      
                      In [6]:
                      let rec sum x = 
                       if x <= 0 then 0
                       else x + sum(x-1)
                      
                      Out[6]:
                      val sum : int -> int = <fun>
                      
                      termination proof

                      Termination proof

                      call `sum (x - 1)` from `sum x`
                      originalsum x
                      subsum (x - 1)
                      original ordinalOrdinal.Int (_cnt x)
                      sub ordinalOrdinal.Int (_cnt (x - 1))
                      path[not (x <= 0)]
                      proof
                      detailed proof
                      ground_instances1
                      definitions0
                      inductions0
                      search_time
                      0.010s
                      details
                      Expand
                      smt_stats
                      num checks3
                      arith-make-feasible5
                      arith-max-columns11
                      arith-conflicts1
                      rlimit count988
                      mk clause5
                      datatype occurs check2
                      mk bool var17
                      arith-lower3
                      decisions2
                      arith-propagations3
                      propagations2
                      arith-bound-propagations-cheap3
                      arith-max-rows4
                      conflicts2
                      datatype accessor ax2
                      num allocs5823115
                      final checks1
                      added eqs6
                      del clause5
                      arith eq adapter2
                      arith-upper6
                      memory5.910000
                      max memory5.910000
                      Expand
                      • start[0.010s]
                          let (_x_0 : int) = if x >= 0 then x else 0 in
                          let (_x_1 : int) = x - 1 in
                          let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
                          not (x <= 0) && _x_0 >= 0 && _x_2 >= 0
                          ==> _x_1 <= 0 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                      • simplify
                        into
                        (x <= 0 || x <= 1)
                        || Ordinal.( << ) (Ordinal.Int (if x >= 1 then -1 + x else 0))
                           (Ordinal.Int (if x >= 0 then x else 0))
                        expansions
                        []
                        rewrite_steps
                          forward_chaining
                          • unroll
                            expr
                            (|Ordinal.<<_126| (|Ordinal.Int_111| (ite (>= x_1785 1) (+ (- 1) x_1785) 0))
                                              (|Ord…
                            expansions
                            • Unsat

                            In [7]:
                            sum 5
                            
                            Out[7]:
                            - : int = 15
                            
                            In [8]:
                            sum 100
                            
                            Out[8]:
                            - : int = 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 : int -> int = <fun>
                            File "jupyter cell 9", line 1, characters 0-63Error: 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 -> int = <fun>
                            
                            termination proof

                            Termination proof

                            call `size (Destruct(Node, 0, _x))` from `size _x`
                            originalsize _x
                            subsize (Destruct(Node, 0, _x))
                            original ordinalOrdinal.Int (_cnt _x)
                            sub ordinalOrdinal.Int (_cnt (Destruct(Node, 0, _x)))
                            path[not Is_a(Leaf, _x)]
                            proof
                            detailed proof
                            ground_instances3
                            definitions0
                            inductions0
                            search_time
                            0.020s
                            details
                            Expand
                            smt_stats
                            num checks8
                            arith-make-feasible18
                            arith-max-columns16
                            arith-conflicts2
                            rlimit count4780
                            mk clause20
                            datatype occurs check14
                            mk bool var75
                            arith-lower14
                            arith-diseq1
                            datatype splits3
                            decisions19
                            propagations15
                            arith-max-rows4
                            conflicts7
                            datatype accessor ax13
                            datatype constructor ax11
                            num allocs23171778
                            final checks4
                            added eqs59
                            del clause13
                            arith eq adapter10
                            arith-upper13
                            memory6.730000
                            max memory11.790000
                            Expand
                            • start[0.020s]
                                let (_x_0 : int) = count.tree (const 0) _x in
                                let (_x_1 : ty_0 tree) = Destruct(Node, 0, _x) in
                                let (_x_2 : int) = count.tree (const 0) _x_1 in
                                let (_x_3 : bool) = Is_a(Leaf, _x_1) in
                                not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
                                ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                            • simplify
                              into
                              let (_x_0 : ty_0 tree) = Destruct(Node, 0, _x) in
                              let (_x_1 : int) = count.tree (const 0) _x_0 in
                              let (_x_2 : int) = count.tree (const 0) _x in
                              (Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                              || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0)
                              expansions
                              []
                              rewrite_steps
                                forward_chaining
                                • unroll
                                  expr
                                  (|`count.tree (const 0)[0]`_1859| _x_1846)
                                  expansions
                                  • unroll
                                    expr
                                    (|`count.tree (const 0)[0]`_1859| (|get.Node.0_1839| _x_1846))
                                    expansions
                                    • unroll
                                      expr
                                      (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                          (|`count.tree (const 0)[0]`_1859|
                                               …
                                      expansions
                                      • Unsat

                                      call `size (Destruct(Node, 1, _x))` from `size _x`
                                      originalsize _x
                                      subsize (Destruct(Node, 1, _x))
                                      original ordinalOrdinal.Int (_cnt _x)
                                      sub ordinalOrdinal.Int (_cnt (Destruct(Node, 1, _x)))
                                      path[not Is_a(Leaf, _x)]
                                      proof
                                      detailed proof
                                      ground_instances3
                                      definitions0
                                      inductions0
                                      search_time
                                      0.015s
                                      details
                                      Expand
                                      smt_stats
                                      num checks8
                                      arith-make-feasible18
                                      arith-max-columns16
                                      arith-conflicts2
                                      rlimit count2390
                                      mk clause20
                                      datatype occurs check14
                                      mk bool var75
                                      arith-lower14
                                      arith-diseq1
                                      datatype splits3
                                      decisions19
                                      propagations15
                                      arith-max-rows4
                                      conflicts7
                                      datatype accessor ax13
                                      datatype constructor ax11
                                      num allocs13106544
                                      final checks4
                                      added eqs59
                                      del clause13
                                      arith eq adapter10
                                      arith-upper13
                                      memory9.200000
                                      max memory9.200000
                                      Expand
                                      • start[0.015s]
                                          let (_x_0 : int) = count.tree (const 0) _x in
                                          let (_x_1 : ty_0 tree) = Destruct(Node, 1, _x) in
                                          let (_x_2 : int) = count.tree (const 0) _x_1 in
                                          let (_x_3 : bool) = Is_a(Leaf, _x_1) in
                                          not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
                                          ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                      • simplify
                                        into
                                        let (_x_0 : ty_0 tree) = Destruct(Node, 1, _x) in
                                        let (_x_1 : int) = count.tree (const 0) _x_0 in
                                        let (_x_2 : int) = count.tree (const 0) _x in
                                        (Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                        || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0)
                                        expansions
                                        []
                                        rewrite_steps
                                          forward_chaining
                                          • unroll
                                            expr
                                            (|`count.tree (const 0)[0]`_1859| _x_1846)
                                            expansions
                                            • unroll
                                              expr
                                              (|`count.tree (const 0)[0]`_1859| (|get.Node.1_1840| _x_1846))
                                              expansions
                                              • unroll
                                                expr
                                                (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                    (|`count.tree (const 0)[0]`_1859|
                                                         …
                                                expansions
                                                • Unsat

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

                                                In [12]:
                                                instance (fun (x : int tree) -> size x = 5)
                                                
                                                Out[12]:
                                                - : int tree -> bool = <fun>
                                                module CX : sig val x : int tree end
                                                
                                                Instance (after 9 steps, 0.020s):
                                                 let (x : int tree) =
                                                  (Node
                                                     ((Node ((Leaf (7)), (Leaf (8)))),
                                                      (Node ((Leaf (10)), (Node ((Leaf (11)), (Leaf (9))))))))
                                                
                                                Instance
                                                proof attempt
                                                ground_instances9
                                                definitions0
                                                inductions0
                                                search_time
                                                0.020s
                                                details
                                                Expand
                                                smt_stats
                                                num checks19
                                                arith-make-feasible62
                                                arith-max-columns35
                                                arith-conflicts8
                                                rlimit count7057
                                                arith-cheap-eqs4
                                                mk clause149
                                                datatype occurs check53
                                                mk bool var563
                                                arith-lower73
                                                arith-diseq38
                                                datatype splits20
                                                decisions114
                                                arith-propagations15
                                                propagations292
                                                arith-bound-propagations-cheap15
                                                arith-max-rows13
                                                conflicts18
                                                datatype accessor ax105
                                                minimized lits2
                                                arith-bound-propagations-lp8
                                                datatype constructor ax105
                                                num allocs27582750
                                                final checks17
                                                added eqs606
                                                del clause65
                                                arith eq adapter80
                                                arith-upper112
                                                memory9.730000
                                                max memory11.790000
                                                Expand
                                                • start[0.020s] size ( :var_0: ) = 5
                                                • unroll
                                                  expr
                                                  (size_1928 x_59)
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (size_1928 (|get.Node.1_1927| x_59))
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (size_1928 (|get.Node.0_1926| x_59))
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (size_1928 (|get.Node.1_1927| (|get.Node.1_1927| x_59)))
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (size_1928 (|get.Node.0_1926| (|get.Node.1_1927| x_59)))
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (size_1928 (|get.Node.1_1927| (|get.Node.0_1926| x_59)))
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (size_1928 (|get.Node.0_1926| (|get.Node.0_1926| x_59)))
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (size_1928 (|get.Node.1_1927| (|get.Node.1_1927| (|get.Node.1_1927| x_59))))
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (size_1928 (|get.Node.0_1926| (|get.Node.1_1927| (|get.Node.1_1927| x_59))))
                                                                  expansions
                                                                  • Sat (Some let (x : int tree) = (Node ((Node ((Leaf (7)), (Leaf (8)))), (Node ((Leaf (10)), (Node ((Leaf (11)), (Leaf (9)))))))) )
                                                                  In [13]:
                                                                  size CX.x
                                                                  
                                                                  Out[13]:
                                                                  - : int = 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 : int tree -> int = <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 (_cnt _x)
                                                                  sub ordinalOrdinal.Int (_cnt (Destruct(Node, 0, _x)))
                                                                  path[not Is_a(Leaf, _x)]
                                                                  proof
                                                                  detailed proof
                                                                  ground_instances3
                                                                  definitions0
                                                                  inductions0
                                                                  search_time
                                                                  0.016s
                                                                  details
                                                                  Expand
                                                                  smt_stats
                                                                  num checks8
                                                                  arith-make-feasible19
                                                                  arith-max-columns17
                                                                  arith-conflicts2
                                                                  rlimit count4878
                                                                  mk clause20
                                                                  datatype occurs check14
                                                                  mk bool var75
                                                                  arith-lower14
                                                                  arith-diseq1
                                                                  datatype splits3
                                                                  decisions19
                                                                  propagations15
                                                                  arith-max-rows4
                                                                  conflicts7
                                                                  datatype accessor ax13
                                                                  datatype constructor ax11
                                                                  num allocs47586916
                                                                  final checks4
                                                                  added eqs59
                                                                  del clause13
                                                                  arith eq adapter10
                                                                  arith-upper13
                                                                  memory9.940000
                                                                  max memory12.480000
                                                                  Expand
                                                                  • start[0.016s]
                                                                      let (_x_0 : int) = count.tree mk_nat _x in
                                                                      let (_x_1 : int tree) = Destruct(Node, 0, _x) in
                                                                      let (_x_2 : int) = count.tree mk_nat _x_1 in
                                                                      let (_x_3 : bool) = Is_a(Leaf, _x_1) in
                                                                      not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
                                                                      ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                  • simplify
                                                                    into
                                                                    let (_x_0 : int tree) = Destruct(Node, 0, _x) in
                                                                    let (_x_1 : int) = count.tree mk_nat _x_0 in
                                                                    let (_x_2 : int) = count.tree mk_nat _x in
                                                                    (Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                    || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0)
                                                                    expansions
                                                                    []
                                                                    rewrite_steps
                                                                      forward_chaining
                                                                      • unroll
                                                                        expr
                                                                        (|`count.tree mk_nat[0]`_1964| _x_1951)
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|`count.tree mk_nat[0]`_1964| (|get.Node.0_1949| _x_1951))
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                (|`count.tree mk_nat[0]`_1964| (|get.Node.0…
                                                                            expansions
                                                                            • Unsat

                                                                            call `sum_tree (Destruct(Node, 1, _x))` from `sum_tree _x`
                                                                            originalsum_tree _x
                                                                            subsum_tree (Destruct(Node, 1, _x))
                                                                            original ordinalOrdinal.Int (_cnt _x)
                                                                            sub ordinalOrdinal.Int (_cnt (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-make-feasible18
                                                                            arith-max-columns16
                                                                            arith-conflicts2
                                                                            rlimit count2452
                                                                            mk clause20
                                                                            datatype occurs check14
                                                                            mk bool var75
                                                                            arith-lower14
                                                                            arith-diseq1
                                                                            datatype splits3
                                                                            decisions19
                                                                            propagations15
                                                                            arith-max-rows4
                                                                            conflicts7
                                                                            datatype accessor ax13
                                                                            datatype constructor ax11
                                                                            num allocs37078401
                                                                            final checks4
                                                                            added eqs59
                                                                            del clause13
                                                                            arith eq adapter10
                                                                            arith-upper13
                                                                            memory9.890000
                                                                            max memory11.790000
                                                                            Expand
                                                                            • start[0.013s]
                                                                                let (_x_0 : int) = count.tree mk_nat _x in
                                                                                let (_x_1 : int tree) = Destruct(Node, 1, _x) in
                                                                                let (_x_2 : int) = count.tree mk_nat _x_1 in
                                                                                let (_x_3 : bool) = Is_a(Leaf, _x_1) in
                                                                                not Is_a(Leaf, _x) && _x_0 >= 0 && _x_2 >= 0
                                                                                ==> _x_3 && _x_3 || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
                                                                            • simplify
                                                                              into
                                                                              let (_x_0 : int tree) = Destruct(Node, 1, _x) in
                                                                              let (_x_1 : int) = count.tree mk_nat _x_0 in
                                                                              let (_x_2 : int) = count.tree mk_nat _x in
                                                                              (Is_a(Leaf, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2))
                                                                              || not ((not Is_a(Leaf, _x) && _x_2 >= 0) && _x_1 >= 0)
                                                                              expansions
                                                                              []
                                                                              rewrite_steps
                                                                                forward_chaining
                                                                                • unroll
                                                                                  expr
                                                                                  (|`count.tree mk_nat[0]`_1964| _x_1951)
                                                                                  expansions
                                                                                  • unroll
                                                                                    expr
                                                                                    (|`count.tree mk_nat[0]`_1964| (|get.Node.1_1950| _x_1951))
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (|Ordinal.<<_126| (|Ordinal.Int_111|
                                                                                                          (|`count.tree mk_nat[0]`_1964| (|get.Node.1…
                                                                                      expansions
                                                                                      • Unsat

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

                                                                                      In [15]:
                                                                                      instance (fun x -> size x >= 5 && size x = 3 * sum_tree x)
                                                                                      
                                                                                      Out[15]:
                                                                                      - : int tree -> bool = <fun>
                                                                                      module CX : sig val x : int tree end
                                                                                      
                                                                                      Instance (after 26 steps, 0.054s):
                                                                                       let (x : int tree) =
                                                                                        (Node
                                                                                           ((Node ((Leaf (56867)), (Leaf ((-46532))))),
                                                                                            (Node
                                                                                               ((Node ((Leaf ((-54829))), (Leaf ((-50521))))),
                                                                                                (Node ((Leaf (107403)), (Leaf ((-12386)))))))))
                                                                                      
                                                                                      Instance
                                                                                      proof attempt
                                                                                      ground_instances26
                                                                                      definitions0
                                                                                      inductions0
                                                                                      search_time
                                                                                      0.054s
                                                                                      details
                                                                                      Expand
                                                                                      smt_stats
                                                                                      arith-assume-eqs43
                                                                                      arith-make-feasible345
                                                                                      arith-max-columns102
                                                                                      arith-conflicts23
                                                                                      arith-gcd-calls17
                                                                                      datatype occurs check277
                                                                                      arith-lower452
                                                                                      arith-diseq197
                                                                                      datatype splits83
                                                                                      arith-propagations96
                                                                                      arith-patches-success9
                                                                                      propagations1963
                                                                                      arith-patches16
                                                                                      interface eqs43
                                                                                      arith-bound-propagations-cheap96
                                                                                      conflicts51
                                                                                      datatype constructor ax478
                                                                                      arith-gomory-cuts2
                                                                                      num allocs56576026
                                                                                      final checks95
                                                                                      added eqs3307
                                                                                      del clause542
                                                                                      arith-branch3
                                                                                      arith-gcd-conflict1
                                                                                      num checks53
                                                                                      arith-cube-calls2
                                                                                      arith-hnf-calls2
                                                                                      rlimit count34595
                                                                                      arith-cheap-eqs38
                                                                                      mk clause812
                                                                                      mk bool var2791
                                                                                      decisions976
                                                                                      arith-max-rows46
                                                                                      datatype accessor ax478
                                                                                      minimized lits4
                                                                                      arith-bound-propagations-lp8
                                                                                      arith eq adapter463
                                                                                      arith-upper643
                                                                                      time0.001000
                                                                                      memory13.650000
                                                                                      max memory13.650000
                                                                                      Expand
                                                                                      • start[0.054s]
                                                                                          let (_x_0 : int) = size ( :var_0: ) in
                                                                                          _x_0 >= 5 && _x_0 = 3 * sum_tree ( :var_0: )
                                                                                      • unroll
                                                                                        expr
                                                                                        (sum_tree_61 x_69)
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (size_2033 x_69)
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (sum_tree_61 (|get.Node.1_2032| x_69))
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (sum_tree_61 (|get.Node.0_2031| x_69))
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (size_2033 (|get.Node.1_2032| x_69))
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (size_2033 (|get.Node.0_2031| x_69))
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (sum_tree_61 (|get.Node.1_2032| (|get.Node.1_2032| x_69)))
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (sum_tree_61 (|get.Node.0_2031| (|get.Node.1_2032| x_69)))
                                                                                                      expansions
                                                                                                      • unroll
                                                                                                        expr
                                                                                                        (sum_tree_61 (|get.Node.1_2032| (|get.Node.0_2031| x_69)))
                                                                                                        expansions
                                                                                                        • unroll
                                                                                                          expr
                                                                                                          (sum_tree_61 (|get.Node.0_2031| (|get.Node.0_2031| x_69)))
                                                                                                          expansions
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (size_2033 (|get.Node.1_2032| (|get.Node.1_2032| x_69)))
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (size_2033 (|get.Node.0_2031| (|get.Node.1_2032| x_69)))
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (size_2033 (|get.Node.1_2032| (|get.Node.0_2031| x_69)))
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (size_2033 (|get.Node.0_2031| (|get.Node.0_2031| x_69)))
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (sum_tree_61 (|get.Node.1_2032| (|get.Node.1_2032| (|get.Node.1_2032| x_69))))
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (sum_tree_61 (|get.Node.0_2031| (|get.Node.1_2032| (|get.Node.1_2032| x_69))))
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (sum_tree_61 (|get.Node.1_2032| (|get.Node.0_2031| (|get.Node.1_2032| x_69))))
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (sum_tree_61 (|get.Node.0_2031| (|get.Node.0_2031| (|get.Node.1_2032| x_69))))
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (sum_tree_61 (|get.Node.1_2032| (|get.Node.1_2032| (|get.Node.0_2031| x_69))))
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (sum_tree_61 (|get.Node.0_2031| (|get.Node.1_2032| (|get.Node.0_2031| x_69))))
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (sum_tree_61 (|get.Node.1_2032| (|get.Node.0_2031| (|get.Node.0_2031| x_69))))
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (sum_tree_61 (|get.Node.0_2031| (|get.Node.0_2031| (|get.Node.0_2031| x_69))))
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (size_2033 (|get.Node.1_2032| (|get.Node.1_2032| (|get.Node.1_2032| x_69))))
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (size_2033 (|get.Node.0_2031| (|get.Node.1_2032| (|get.Node.1_2032| x_69))))
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (size_2033 (|get.Node.1_2032| (|get.Node.0_2031| (|get.Node.1_2032| x_69))))
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (size_2033 (|get.Node.0_2031| (|get.Node.0_2031| (|get.Node.1_2032| x_69))))
                                                                                                                                          expansions
                                                                                                                                          • Sat (Some let (x : int tree) = (Node ((Node ((Leaf (56867)), (Leaf ((-46532))))), (Node ((Node ((Leaf ((-54829))), (Leaf ((-50521))))), (Node ((Leaf (107403)), (Leaf ((-12386))))))))) )

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

                                                                                                                                          In [16]:
                                                                                                                                          size CX.x
                                                                                                                                          
                                                                                                                                          Out[16]:
                                                                                                                                          - : int = 6
                                                                                                                                          
                                                                                                                                          In [17]:
                                                                                                                                          3 * sum_tree CX.x
                                                                                                                                          
                                                                                                                                          Out[17]:
                                                                                                                                          - : int = 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-105Error: 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 (_cnt m); Ordinal.Int (_cnt n)]
                                                                                                                                          sub ordinalOrdinal.of_list [Ordinal.Int (_cnt (m - 1)); Ordinal.Int (_cnt 1)]
                                                                                                                                          path[n <= 0 && not (m <= 0)]
                                                                                                                                          proof
                                                                                                                                          detailed proof
                                                                                                                                          ground_instances5
                                                                                                                                          definitions0
                                                                                                                                          inductions0
                                                                                                                                          search_time
                                                                                                                                          0.016s
                                                                                                                                          details
                                                                                                                                          Expand
                                                                                                                                          smt_stats
                                                                                                                                          num checks12
                                                                                                                                          arith-make-feasible21
                                                                                                                                          arith-max-columns20
                                                                                                                                          rlimit count19134
                                                                                                                                          arith-cheap-eqs8
                                                                                                                                          mk clause48
                                                                                                                                          datatype occurs check59
                                                                                                                                          mk bool var125
                                                                                                                                          arith-lower19
                                                                                                                                          arith-diseq8
                                                                                                                                          datatype splits4
                                                                                                                                          decisions53
                                                                                                                                          arith-propagations12
                                                                                                                                          propagations47
                                                                                                                                          arith-bound-propagations-cheap12
                                                                                                                                          arith-max-rows7
                                                                                                                                          conflicts13
                                                                                                                                          datatype accessor ax21
                                                                                                                                          arith-bound-propagations-lp1
                                                                                                                                          datatype constructor ax10
                                                                                                                                          num allocs111111898
                                                                                                                                          final checks8
                                                                                                                                          added eqs130
                                                                                                                                          del clause21
                                                                                                                                          arith eq adapter13
                                                                                                                                          arith-upper14
                                                                                                                                          memory19.670000
                                                                                                                                          max memory19.680000
                                                                                                                                          Expand
                                                                                                                                          • start[0.016s]
                                                                                                                                              let (_x_0 : int) = m - 1 in
                                                                                                                                              let (_x_1 : bool) = 1 <= 0 in
                                                                                                                                              let (_x_2 : bool) = not (_x_0 <= 0) in
                                                                                                                                              let (_x_3 : bool) = not (not _x_1 && _x_2) in
                                                                                                                                              n <= 0
                                                                                                                                              && not (m <= 0)
                                                                                                                                                 && (if m >= 0 then m else 0) >= 0
                                                                                                                                                    && (if n >= 0 then n else 0) >= 0
                                                                                                                                                       && (if _x_0 >= 0 then _x_0 else 0) >= 0
                                                                                                                                                          && (if 1 >= 0 then 1 else 0) >= 0
                                                                                                                                              ==> not (_x_1 && _x_2) && _x_3 && _x_3
                                                                                                                                                  || Ordinal.( << ) (if Is_a([], …) then … else …)
                                                                                                                                                     (if Is_a([], …) then … else …)
                                                                                                                                          • simplify
                                                                                                                                            into
                                                                                                                                            let (_x_0 : Ordinal.t) = Ordinal.Int 1 in
                                                                                                                                            (Ordinal.( << ) (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_0) _x_0)
                                                                                                                                             (Ordinal.plus (Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) _x_0)
                                                                                                                                              (Ordinal.Int (if n >= 0 then n else 0)))
                                                                                                                                             || not (n <= 0 && not (m <= 0)))
                                                                                                                                            || m <= 1
                                                                                                                                            expansions
                                                                                                                                            []
                                                                                                                                            rewrite_steps
                                                                                                                                              forward_chaining
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (|Ordinal.shift_205|
                                                                                                                                                  (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                  (|Ordinal.Int_111| 1))
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                               (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                        …
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (|Ordinal.shift_205|
                                                                                                                                                      (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) 0))
                                                                                                                                                      (|Ordinal.Int_11…
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                   (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) …
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                     (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) …
                                                                                                                                                        expansions
                                                                                                                                                        • Unsat

                                                                                                                                                        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 (_cnt m); Ordinal.Int (_cnt n)]
                                                                                                                                                        sub ordinalOrdinal.of_list [Ordinal.Int (_cnt (m - 1)); Ordinal.Int (_cnt (ack m (n - 1)))]
                                                                                                                                                        path[not (n <= 0) && not (m <= 0)]
                                                                                                                                                        proof
                                                                                                                                                        detailed proof
                                                                                                                                                        ground_instances5
                                                                                                                                                        definitions0
                                                                                                                                                        inductions0
                                                                                                                                                        search_time
                                                                                                                                                        0.022s
                                                                                                                                                        details
                                                                                                                                                        Expand
                                                                                                                                                        smt_stats
                                                                                                                                                        num checks11
                                                                                                                                                        arith-assume-eqs1
                                                                                                                                                        arith-make-feasible17
                                                                                                                                                        arith-max-columns24
                                                                                                                                                        rlimit count13850
                                                                                                                                                        arith-cheap-eqs2
                                                                                                                                                        mk clause76
                                                                                                                                                        datatype occurs check78
                                                                                                                                                        mk bool var123
                                                                                                                                                        arith-lower6
                                                                                                                                                        arith-diseq14
                                                                                                                                                        datatype splits4
                                                                                                                                                        decisions45
                                                                                                                                                        arith-propagations14
                                                                                                                                                        propagations74
                                                                                                                                                        interface eqs1
                                                                                                                                                        arith-bound-propagations-cheap14
                                                                                                                                                        arith-max-rows9
                                                                                                                                                        conflicts11
                                                                                                                                                        datatype accessor ax21
                                                                                                                                                        arith-bound-propagations-lp1
                                                                                                                                                        datatype constructor ax9
                                                                                                                                                        num allocs101530970
                                                                                                                                                        final checks9
                                                                                                                                                        added eqs99
                                                                                                                                                        del clause27
                                                                                                                                                        arith eq adapter12
                                                                                                                                                        arith-upper28
                                                                                                                                                        time0.001000
                                                                                                                                                        memory17.050000
                                                                                                                                                        max memory19.680000
                                                                                                                                                        Expand
                                                                                                                                                        • start[0.022s]
                                                                                                                                                            let (_x_0 : int) = m - 1 in
                                                                                                                                                            let (_x_1 : int) = ack m (n - 1) in
                                                                                                                                                            let (_x_2 : bool) = _x_1 <= 0 in
                                                                                                                                                            let (_x_3 : bool) = not (_x_0 <= 0) in
                                                                                                                                                            let (_x_4 : bool) = not (not _x_2 && _x_3) in
                                                                                                                                                            not (n <= 0)
                                                                                                                                                            && not (m <= 0)
                                                                                                                                                               && (if m >= 0 then m else 0) >= 0
                                                                                                                                                                  && (if n >= 0 then n else 0) >= 0
                                                                                                                                                                     && (if _x_0 >= 0 then _x_0 else 0) >= 0
                                                                                                                                                                        && (if _x_1 >= 0 then _x_1 else 0) >= 0
                                                                                                                                                            ==> not (_x_2 && _x_3) && _x_4 && _x_4
                                                                                                                                                                || Ordinal.( << ) (if Is_a([], …) then … else …)
                                                                                                                                                                   (if Is_a([], …) then … else …)
                                                                                                                                                        • simplify
                                                                                                                                                          into
                                                                                                                                                          let (_x_0 : int) = ack m (-1 + n) in
                                                                                                                                                          let (_x_1 : bool) = _x_0 <= 0 in
                                                                                                                                                          let (_x_2 : bool) = not (m <= 1) in
                                                                                                                                                          let (_x_3 : Ordinal.t) = Ordinal.Int 1 in
                                                                                                                                                          (not (not (n <= 0) && not (m <= 0))
                                                                                                                                                           || not (_x_1 && _x_2) && not (not _x_1 && _x_2))
                                                                                                                                                          || Ordinal.( << )
                                                                                                                                                             (Ordinal.plus (Ordinal.shift (Ordinal.Int …) _x_3)
                                                                                                                                                              (Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)))
                                                                                                                                                             (Ordinal.plus (Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) _x_3)
                                                                                                                                                              (Ordinal.Int (if n >= 0 then n else 0)))
                                                                                                                                                          expansions
                                                                                                                                                          []
                                                                                                                                                          rewrite_steps
                                                                                                                                                            forward_chaining
                                                                                                                                                            • unroll
                                                                                                                                                              expr
                                                                                                                                                              (|Ordinal.shift_205|
                                                                                                                                                                (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                (|Ordinal.Int_111| 1))
                                                                                                                                                              expansions
                                                                                                                                                              • unroll
                                                                                                                                                                expr
                                                                                                                                                                (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                             (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                      …
                                                                                                                                                                expansions
                                                                                                                                                                • unroll
                                                                                                                                                                  expr
                                                                                                                                                                  (|Ordinal.shift_205|
                                                                                                                                                                    (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) 0))
                                                                                                                                                                    (|Ordinal.Int_11…
                                                                                                                                                                  expansions
                                                                                                                                                                  • unroll
                                                                                                                                                                    expr
                                                                                                                                                                    (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                 (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) …
                                                                                                                                                                    expansions
                                                                                                                                                                    • unroll
                                                                                                                                                                      expr
                                                                                                                                                                      (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                   (|Ordinal.Int_111| (ite (>= m_2101 1) (+ (- 1) m_2101) …
                                                                                                                                                                      expansions
                                                                                                                                                                      • Unsat

                                                                                                                                                                      call `ack m (n - 1)` from `ack m n`
                                                                                                                                                                      originalack m n
                                                                                                                                                                      suback m (n - 1)
                                                                                                                                                                      original ordinalOrdinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt n)]
                                                                                                                                                                      sub ordinalOrdinal.of_list [Ordinal.Int (_cnt m); Ordinal.Int (_cnt (n - 1))]
                                                                                                                                                                      path[not (n <= 0) && not (m <= 0)]
                                                                                                                                                                      proof
                                                                                                                                                                      detailed proof
                                                                                                                                                                      ground_instances7
                                                                                                                                                                      definitions0
                                                                                                                                                                      inductions0
                                                                                                                                                                      search_time
                                                                                                                                                                      0.020s
                                                                                                                                                                      details
                                                                                                                                                                      Expand
                                                                                                                                                                      smt_stats
                                                                                                                                                                      num checks16
                                                                                                                                                                      arith-assume-eqs1
                                                                                                                                                                      arith-make-feasible16
                                                                                                                                                                      arith-max-columns34
                                                                                                                                                                      rlimit count8170
                                                                                                                                                                      arith-cheap-eqs9
                                                                                                                                                                      mk clause82
                                                                                                                                                                      datatype occurs check141
                                                                                                                                                                      mk bool var194
                                                                                                                                                                      arith-lower9
                                                                                                                                                                      arith-diseq3
                                                                                                                                                                      datatype splits13
                                                                                                                                                                      decisions89
                                                                                                                                                                      arith-propagations3
                                                                                                                                                                      propagations75
                                                                                                                                                                      interface eqs1
                                                                                                                                                                      arith-bound-propagations-cheap3
                                                                                                                                                                      arith-max-rows16
                                                                                                                                                                      conflicts17
                                                                                                                                                                      datatype accessor ax35
                                                                                                                                                                      arith-bound-propagations-lp2
                                                                                                                                                                      datatype constructor ax20
                                                                                                                                                                      num allocs82555740
                                                                                                                                                                      final checks14
                                                                                                                                                                      added eqs157
                                                                                                                                                                      del clause47
                                                                                                                                                                      arith eq adapter11
                                                                                                                                                                      arith-upper14
                                                                                                                                                                      memory16.990000
                                                                                                                                                                      max memory16.990000
                                                                                                                                                                      Expand
                                                                                                                                                                      • start[0.020s]
                                                                                                                                                                          let (_x_0 : bool) = not (m <= 0) in
                                                                                                                                                                          let (_x_1 : bool) = (if m >= 0 then m else 0) >= 0 in
                                                                                                                                                                          let (_x_2 : int) = n - 1 in
                                                                                                                                                                          let (_x_3 : bool) = _x_2 <= 0 in
                                                                                                                                                                          let (_x_4 : bool) = not (not _x_3 && _x_0) in
                                                                                                                                                                          not (n <= 0)
                                                                                                                                                                          && _x_0
                                                                                                                                                                             && _x_1
                                                                                                                                                                                && (if n >= 0 then n else 0) >= 0
                                                                                                                                                                                   && _x_1 && (if _x_2 >= 0 then _x_2 else 0) >= 0
                                                                                                                                                                          ==> not (_x_3 && _x_0) && _x_4 && _x_4
                                                                                                                                                                              || Ordinal.( << ) (if Is_a([], …) then … else …)
                                                                                                                                                                                 (if Is_a([], …) then … else …)
                                                                                                                                                                      • simplify
                                                                                                                                                                        into
                                                                                                                                                                        let (_x_0 : bool) = n <= 1 in
                                                                                                                                                                        let (_x_1 : bool) = not (m <= 0) in
                                                                                                                                                                        let (_x_2 : Ordinal.t)
                                                                                                                                                                            = Ordinal.shift (Ordinal.Int (if m >= 0 then m else 0)) (Ordinal.Int 1)
                                                                                                                                                                        in
                                                                                                                                                                        (not (_x_0 && _x_1) && not (not _x_0 && _x_1)
                                                                                                                                                                         || Ordinal.( << )
                                                                                                                                                                            (Ordinal.plus _x_2 (Ordinal.Int (if n >= 1 then -1 + n else 0)))
                                                                                                                                                                            (Ordinal.plus _x_2 (Ordinal.Int (if n >= 0 then n else 0))))
                                                                                                                                                                        || not (not (n <= 0) && _x_1)
                                                                                                                                                                        expansions
                                                                                                                                                                        []
                                                                                                                                                                        rewrite_steps
                                                                                                                                                                          forward_chaining
                                                                                                                                                                          • unroll
                                                                                                                                                                            expr
                                                                                                                                                                            (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                         (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                                  …
                                                                                                                                                                            expansions
                                                                                                                                                                            • unroll
                                                                                                                                                                              expr
                                                                                                                                                                              (|Ordinal.shift_205|
                                                                                                                                                                                (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                                (|Ordinal.Int_111| 1))
                                                                                                                                                                              expansions
                                                                                                                                                                              • unroll
                                                                                                                                                                                expr
                                                                                                                                                                                (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                             (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                                      …
                                                                                                                                                                                expansions
                                                                                                                                                                                • unroll
                                                                                                                                                                                  expr
                                                                                                                                                                                  (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                               (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                                        …
                                                                                                                                                                                  expansions
                                                                                                                                                                                  • unroll
                                                                                                                                                                                    expr
                                                                                                                                                                                    (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                                 (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                                          …
                                                                                                                                                                                    expansions
                                                                                                                                                                                    • unroll
                                                                                                                                                                                      expr
                                                                                                                                                                                      (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                                   (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                                            …
                                                                                                                                                                                      expansions
                                                                                                                                                                                      • unroll
                                                                                                                                                                                        expr
                                                                                                                                                                                        (let ((a!1 (|Ordinal.shift_205|
                                                                                                                                                                                                     (|Ordinal.Int_111| (ite (>= m_2101 0) m_2101 0))
                                                                                                                                                                                              …
                                                                                                                                                                                        expansions
                                                                                                                                                                                        • Unsat

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

                                                                                                                                                                                        Measures and Ordinals

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

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

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

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

                                                                                                                                                                                        In [20]:
                                                                                                                                                                                        #show Ordinal
                                                                                                                                                                                        
                                                                                                                                                                                        Out[20]:
                                                                                                                                                                                        module Ordinal :
                                                                                                                                                                                          sig
                                                                                                                                                                                            type t = Int of 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 triple : t -> t -> t -> t
                                                                                                                                                                                            val quad : t -> t -> t -> t -> t
                                                                                                                                                                                            val shift : t -> by:t -> t
                                                                                                                                                                                            val is_valid : t -> bool
                                                                                                                                                                                            val is_valid_rec : t -> bool
                                                                                                                                                                                            val zero : t
                                                                                                                                                                                            val one : t
                                                                                                                                                                                            val omega : t
                                                                                                                                                                                            val omega_omega : t
                                                                                                                                                                                          end
                                                                                                                                                                                        

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

                                                                                                                                                                                        In [21]:
                                                                                                                                                                                        Ordinal.omega
                                                                                                                                                                                        
                                                                                                                                                                                        Out[21]:
                                                                                                                                                                                        - : Ordinal.t = ω
                                                                                                                                                                                        
                                                                                                                                                                                        In [22]:
                                                                                                                                                                                        Ordinal.(omega + omega)
                                                                                                                                                                                        
                                                                                                                                                                                        Out[22]:
                                                                                                                                                                                        - : Ordinal.t = 2·ω
                                                                                                                                                                                        
                                                                                                                                                                                        In [23]:
                                                                                                                                                                                        let o1 = Ordinal.(omega + omega_omega + shift omega ~by:(omega + one))
                                                                                                                                                                                        
                                                                                                                                                                                        Out[23]:
                                                                                                                                                                                        val o1 : Ordinal.t = ω^(ω + 1)
                                                                                                                                                                                        
                                                                                                                                                                                        In [24]:
                                                                                                                                                                                        Ordinal.(o1 << omega_omega)
                                                                                                                                                                                        
                                                                                                                                                                                        Out[24]:
                                                                                                                                                                                        - : bool = false
                                                                                                                                                                                        

                                                                                                                                                                                        Ordinals are fundamental to program termination because they represent well-founded orderings (well-orders).

                                                                                                                                                                                        If we can prove that a function's recursive calls always get smaller with respect to some well-founded ordering, then we know the function will always terminate.

                                                                                                                                                                                        The fundamental well-founded relation in Imandra is Ordinal.(<<). This is the strict, well-founded ordering relation on the ordinals up to $\epsilon_0$:

                                                                                                                                                                                        Let's consider an example famous recursive function that we can't admit with a lexicographic order and see how we can write our own measure function and communicate it to Imandra.

                                                                                                                                                                                        Left pad

                                                                                                                                                                                        Consider the following function left_pad:

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

                                                                                                                                                                                        If we give this function to Imandra without any hints, it will not be able to prove it terminating.

                                                                                                                                                                                        In [25]:
                                                                                                                                                                                        let rec left_pad c n xs =
                                                                                                                                                                                          if List.length xs >= n then
                                                                                                                                                                                            xs
                                                                                                                                                                                          else
                                                                                                                                                                                            left_pad c n (c :: xs)
                                                                                                                                                                                        
                                                                                                                                                                                        Out[25]:
                                                                                                                                                                                        val left_pad : 'a -> int -> 'a list -> 'a list = <fun>
                                                                                                                                                                                        File "jupyter cell 25", line 1, characters 0-96Error: 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 : int -> '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-assume-eqs2
                                                                                                                                                                                        arith-make-feasible11
                                                                                                                                                                                        arith-max-columns17
                                                                                                                                                                                        arith-conflicts1
                                                                                                                                                                                        rlimit count1814
                                                                                                                                                                                        arith-cheap-eqs2
                                                                                                                                                                                        mk clause14
                                                                                                                                                                                        datatype occurs check12
                                                                                                                                                                                        mk bool var36
                                                                                                                                                                                        arith-lower7
                                                                                                                                                                                        datatype splits2
                                                                                                                                                                                        decisions9
                                                                                                                                                                                        arith-propagations2
                                                                                                                                                                                        propagations6
                                                                                                                                                                                        interface eqs2
                                                                                                                                                                                        arith-bound-propagations-cheap2
                                                                                                                                                                                        arith-max-rows7
                                                                                                                                                                                        conflicts3
                                                                                                                                                                                        datatype accessor ax5
                                                                                                                                                                                        datatype constructor ax2
                                                                                                                                                                                        num allocs156894637
                                                                                                                                                                                        final checks6
                                                                                                                                                                                        added eqs21
                                                                                                                                                                                        del clause10
                                                                                                                                                                                        arith eq adapter5
                                                                                                                                                                                        arith-upper9
                                                                                                                                                                                        memory20.410000
                                                                                                                                                                                        max memory20.410000
                                                                                                                                                                                        Expand
                                                                                                                                                                                        • start[0.013s]
                                                                                                                                                                                            let (_x_0 : int) = List.length xs in
                                                                                                                                                                                            let (_x_1 : int) = n - _x_0 in
                                                                                                                                                                                            let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
                                                                                                                                                                                            let (_x_3 : int) = List.length (c :: xs) in
                                                                                                                                                                                            let (_x_4 : int) = n - _x_3 in
                                                                                                                                                                                            let (_x_5 : int) = if _x_4 >= 0 then _x_4 else 0 in
                                                                                                                                                                                            not (_x_0 >= n) && _x_2 >= 0 && _x_5 >= 0
                                                                                                                                                                                            ==> _x_3 >= n || Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_2)
                                                                                                                                                                                        • simplify
                                                                                                                                                                                          into
                                                                                                                                                                                          let (_x_0 : int) = List.length xs in
                                                                                                                                                                                          let (_x_1 : int) = List.length (c :: xs) in
                                                                                                                                                                                          let (_x_2 : int) = n + -1 * _x_1 in
                                                                                                                                                                                          let (_x_3 : int) = n + -1 * _x_0 in
                                                                                                                                                                                          (_x_0 >= n || _x_1 >= n)
                                                                                                                                                                                          || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0))
                                                                                                                                                                                             (Ordinal.Int (if _x_3 >= 0 then _x_3 else 0))
                                                                                                                                                                                          expansions
                                                                                                                                                                                          []
                                                                                                                                                                                          rewrite_steps
                                                                                                                                                                                            forward_chaining
                                                                                                                                                                                            • unroll
                                                                                                                                                                                              expr
                                                                                                                                                                                              (let ((a!1 (+ n_2359 (* (- 1) (|List.length_2354| (|::_3| c_2358 xs_2360)))))
                                                                                                                                                                                                    (a!2 (>= (+ n_23…
                                                                                                                                                                                              expansions
                                                                                                                                                                                              • unroll
                                                                                                                                                                                                expr
                                                                                                                                                                                                (|List.length_2354| (|::_3| c_2358 xs_2360))
                                                                                                                                                                                                expansions
                                                                                                                                                                                                • Unsat

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

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

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

                                                                                                                                                                                                Fun: left_pad

                                                                                                                                                                                                iml
                                                                                                                                                                                                definition
                                                                                                                                                                                                fun (c : '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
                                                                                                                                                                                                def-depth4
                                                                                                                                                                                                def-ty-depth2
                                                                                                                                                                                                call signatureleft_pad (c : 'a) (n : int) (xs : 'a list)
                                                                                                                                                                                                measured subset[n; xs]
                                                                                                                                                                                                parametrictrue
                                                                                                                                                                                                validatedin 0.004s
                                                                                                                                                                                                locationjupyter cell 28:1,0--130
                                                                                                                                                                                                sub-function(s)
                                                                                                                                                                                                Expand
                                                                                                                                                                                                namemeasure_fun.left_pad
                                                                                                                                                                                                typeint -> 'b list -> Ordinal.t
                                                                                                                                                                                                recursivefalse
                                                                                                                                                                                                def-depth6
                                                                                                                                                                                                def-ty-depth2
                                                                                                                                                                                                call signaturemeasure_fun.left_pad (n : int) (xs : 'b list)
                                                                                                                                                                                                body
                                                                                                                                                                                                left_pad_measure n xs
                                                                                                                                                                                                parametrictrue
                                                                                                                                                                                                validatedin 0.002s
                                                                                                                                                                                                locationjupyter cell 28:1,0--130
                                                                                                                                                                                                hashes
                                                                                                                                                                                                left_padKLd+2TQBjsVq4sqBwq8NCBsvd7pFxysqw2lxIwXz9WU
                                                                                                                                                                                                measure_fun.left_padlNG8FxDohlAvgDKWxv3iKnGTaXXQr0h8WTJWKQmONZU

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