Proofs of termination

A well-founded partial order on terms

In order to prove a function terminating in F* one provides a measure: a pure expression depending on the function’s arguments. F* checks that this measure strictly decreases on each recursive call. The measure for the arguments of the call is compared to the measure for the previous call according to a well-founded partial order on F* terms. We write v1 << v2 when v1 precedes v2 in this order.

Since the measure strictly decreases on each recursive call, and there are no infinite descending chains, this guarantees that the function eventually stops making recursive calls, i.e., it terminates.

Why length terminates

Let’s look again at the definition of length and see how F* checks that it terminates, i.e.,

let rec length #a (l:list a)
  : nat
  = match l with
    | [] -> 0
    | _ :: tl -> 1 + length tl

First off, the definition of length above makes use of various syntactic shorthands to hide some details. If we were to write it out fully, it would be as shown below:

let rec length #a (l:list a)
  : Tot nat (decreases l)
  = match l with
    | [] -> 0
    | _ :: tl -> length tl

The main difference is on the second line. As opposed to just writing the result type of length, in full detail, we write Tot nat (decreases l). This states two things

• The Tot nat part states that length is a total function returning a nat, just as the nat did before.

• The additional (decreases l) specifying a measure, i.e., the quantity that decreases at each recursive call according the well-founded relation <<.

To check the definition, F* gives the recursively bound name (length in this case) a type that’s guarded by the measure. I.e., for the body of the function, length has the following type:

#a:Type -> m:list a{ m << l } -> nat

This is to say that when using length to make a recursive call, we can only apply it to an argument m << l, i.e., the recursive call can only be made on an argument m that precedes the current argument l. This is enough to ensure that the recursive calls will eventually bottom out, since there are no infinite descending chains related by <<.

In the case of length, we need to prove at the recursive call length tl that tl : (m : list a { m << l }), or, equivalently that tl << l is valid. But, from the sub-term ordering on inductive types, l = Cons _ tl, so tl << l is indeed provable and everything checks out.

Lexicographic orderings

F* also provides a convenience to enhance the well-founded ordering << to lexicographic combinations of <<. That is, given two lists of terms v1, ..., vn and u1, ..., un, F* accepts that the following lexicographic ordering:

v1 << u1 ‌‌\/ (v1 == u1 /\ (v2 << u2 ‌‌\/ (v2 == u2 /\ ( ... vn << un))))

is also well-founded. In fact, it is possible to prove in F* that this ordering is well-founded, provided << is itself well-founded.

Lexicographic ordering are common enough that F* provides special support to make it convenient to use them. In particular, the notation:

%[v1; v2; ...; vn] << %[u1; u2; ...; un]

is shorthand for:

v1 << u1 ‌‌\/ (v1 == u1 /\ (v2 << u2 ‌‌\/ (v2 == u2 /\ ( ... vn << un))))

Let’s have a look at lexicographic orderings at work in proving that the classic ackermann function terminates on all inputs.

let rec ackermann (m n:nat)
  : Tot nat (decreases %[m;n])
  = if m=0 then n + 1
    else if n = 0 then ackermann (m - 1) 1
    else ackermann (m - 1) (ackermann m (n - 1))

The decreases %[m;n] syntax tells F* to use the lexicographic ordering on the pair of arguments m, n as the measure to prove this function terminating.

When defining ackermann m n, for each recursive call of the form ackermann m' n', F* checks that %[m';n'] << %[m;n], i.e., F* checks that either

• m' << m, or

• m' = m and n' << n

There are three recursive calls to consider:

1. ackermann (m - 1) 1: In this case, since we know that m > 0, we have m - 1 << m, due to the ordering on natural numbers. Since the ordering is lexicographic, the second argument is irrelevant for termination.

2. ackermann m (n - 1): In this case, the first argument remained the same (i.e., it’s still m), but we know that n > 0 so n - 1 << n by the natural number ordering.

3. ackermann (m - 1) (ackermann m (n - 1)): Again, like in the first case, the first argument m - 1 << m, and the second is irrelevant for termination.

Default measures

As we saw earlier, F* allows you to write the following code, with no decreases clause, and it still accepts it.

let rec length #a (l:list a)
  : nat
  = match l with
    | [] -> 0
    | _ :: tl -> 1 + length tl

For that matter, you can leave out the decreases clause in ackermann and F* is okay with it.

let rec ackermann (m n:nat)
  : nat
  = if m=0 then n + 1
    else if n = 0 then ackermann (m - 1) 1
    else ackermann (m - 1) (ackermann m (n - 1))

This is because F* uses a simple heuristic to choose the decreases clause, if the user didn’t provide one.

The default decreases clause for a total, recursive function is the lexicographic ordering of all the non-function-typed arguments, taken in order from left to right.

That is, the default decreases clause for ackermann is exactly decreases %[m; n]; and the default for length is just decreases %[a; l] (which is equivalent to decreases l). So, you needn’t write it.

On the other hand, it you were to flip the order of arguments to ackermann, then the default choice of the measure would not be correct—so, you’ll have to write it explicitly, as shown below.

let rec ackermann_flip (n m:nat)
  : Tot nat (decreases %[m;n])
  = if m=0 then n + 1
    else if n = 0 then ackermann_flip 1 (m - 1)
    else ackermann_flip (ackermann (n - 1) m) (m - 1)

Mutual recursion

F* also supports mutual recursion and the same check of proving that a measure of the arguments decreases on each (mutually) recursive call applies.

For example, one can write the following code to define a binary tree that stores an integer at each internal node—the keyword and allows defining several types that depend mutually on each other.

To increment all the integers in the tree, we can write the mutually recursive functions, again using and to define incr_tree and incr_node to depend mutually on each other. F* is able to prove that these functions terminate, just by using the default measure as usual.

type tree =
  | Terminal : tree
  | Internal : node -> tree

and node = {
  left : tree;
  data : int;
  right : tree
}

let rec incr_tree (x:tree)
  : tree
  = match x with
    | Terminal -> Terminal
    | Internal node -> Internal (incr_node node)

and incr_node (n:node)
  : node
  = {
      left = incr_tree n.left;
      data = n.data + 1;
      right = incr_tree n.right
    }

let rec foo (l:list int)
  : Tot int (decreases %[l;0])
  = match l with
    | [] -> 0
    | x :: xs -> bar xs
and bar (l:list int)
  : Tot int (decreases %[l;1])
  = foo l

The termination check, precisely

Having seen a few examples at work, we can now describe how the termination check works in general.

When defining a recursive function

i.e., \(\mathsf{f}\) is a function with several arguments \(\mathsf{x1:t1}, ..., \mathsf{x_n:t_n}\), returning \(\mathsf{r}\) with measure \(\mathsf{m}\), mutually recursively with other functions of several arguments at type:

we check the definition of the function body of \(\mathsf{f}\) (i.e., \(\mathsf{e}\)) with all the mutually recursive functions in scope, but at types that restrict their domain, in the following sense:

That is, each function in the mutually recursive group can only be applied to arguments that precede the current formal parameters of \(\mathsf{f}\) according to the annotated measures of each function.

Exercise: Fibonacci in linear time

Click here for the exercise file.

Here’s a function to compute the \(n\)-th Fibonacci number.

let rec fibonacci (n:nat)
  : nat
  = if n <= 1
    then 1
    else fibonacci (n - 1) + fibonacci (n - 2)

Here’s a more efficient, tail-recursive, linear-time variant.

let rec fib a b n =
   match n with
   | 0 -> a
   | _ -> fib b (a+b) (n-1)

let fibonacci n = fib 1 1 n

Add annotations to the functions to get F* to accept them, in particular, proving that fib terminates.

let rec fib (a b n:nat)
  : Tot nat (decreases n)
  = match n with
    | 0 -> a
    | _ -> fib b (a+b) (n-1)

let fibonacci (n:nat) : nat = fib 1 1 n

Exercise: Tail-recursive reversal

Click here for the exercise file.

Here is a function to reverse a list:

let rec rev #a (l:list a)
  : list a
  = match l with
    | [] -> []
    | hd::tl -> append (rev tl) hd

But, it is not very efficient, since it is not tail recursive and, worse, it is quadratic, it traverses the reversed tail of the list each time to add the first element to the end of it.

This version is more efficient, because it is tail recursive and linear.

let rec rev_aux l1 l2 =
  match l2 with
  | []     -> l1
  | hd :: tl -> rev_aux (hd :: l1) tl

let rev l = rev_aux [] l

Add type annotations to rev_aux and rev, proving, in particular, that rev_aux terminates.

let rec rev_aux #a (l1 l2:list a)
  : Tot (list a) (decreases l2)
  = match l2 with
    | []     -> l1
    | hd :: tl -> rev_aux (hd :: l1) tl

let rev #a (l:list a) : list a = rev_aux [] l