Well-founded Relations and Termination

In an earlier chapter on proofs of termination, we learned about how F* checks that recursive functions terminate. In this chapter, we see how the termination check arises from inductive types and structural recursion. Just as with equality, termination checking, a core feature of F*’s logic and proof system, finds its foundation in inductive types.

For more technical background on this topic, the following resources may be useful:

Thanks to Aseem Rastogi, Chantal Keller, and Catalin Hritcu, for providing some of the F* libraries presented in this chapter.

Well-founded Relations and Accessibility Predicates

A binary relation \(R\) on elements of type \(T\) is well-founded if there is no infinite sequence \(x_0, x_1, x_2, ...\), such that \(x_i~R~x_{i + 1}\), for all \(i\).

As explained earlier, when typechecking a recursive function f, F* requires the user to provide a measure, some function of the arguments of f, and checks that on a recursive call, the measure of the arguments is related to the measure of the formal parameters a built-in well-founded relation on F* terms. Since well-founded relations have no infinite descending chains, every chain of recursive calls related by such a relation must eventually terminate. However, this built-in well-founded relation, written << or precedes, is a derived notion.

In its most primitive form, the well-foundedness of a relation can be expressed in terms of an inductive type acc (short for “accessible”) shown below.

let binrel a = a -> a -> Type
noeq
type acc (#a:Type) (r:binrel a) (x0:a) : Type =
  | AccIntro : access_smaller:(x1:a -> r x1 x0 -> acc r x1) -> acc r x0

The type acc is parameterized by a type a; a binary relation r: a -> a -> Type on a; and an element of the type x:a. Informally, the relation r y x is provable when y is “smaller” than x.

The acc type has just one constructor AccIntro, whose only argument is a function of type y:a -> r y x -> acc r y. Intuitively, this says that in order to build an instance of acc r x0, you have to provide a function which can build a proof of acc r x1 for all x1:a smaller than x0. The only way to build such a function is one can avoid infinite regress, is if the chain x0 r x1 r x2 r ..., eventually terminates in some xn such that there are no elements smaller than it according to r.

In other words, if one can prove acc r x for all x:a, then this precisely captures the condition that there are no infinite descending r-related chains in a, or that r is well-founded. This is exactly what the definition below says, where is_well_founded is a classical (SMT-automatable) variant of well_founded.

let well_founded (#a:Type) (r:binrel a) = x:a -> acc r x
let is_well_founded (#a:Type) (r:binrel a) = forall x. squash (acc r x)

Well-founded Recursion

Given a relation r and proof of p:acc r x , one can define a recursive function on x whose termination can be established purely in terms of structural recursion on the proof p, even though the function may not itself be structurally recursive on x.

The combinator fix_F shown below illustrates this at work:

let rec fix_F (#aa:Type)
              (#r:binrel aa)
              (#p:(aa -> Type))
              (f: (x:aa -> (y:aa -> r y x -> p y) -> p x))              
              (x0:aa)
              (accessible_x0:acc r x0)
  : Tot (p x0) (decreases accessible_x0)
  = f x0 (fun y r_yx -> fix_F f y (accessible_x0.access_smaller y r_yx))

If f is a function such that every recursive call in the definition of f x is on an argument y, such that that y is smaller than x according to some relation r; and if starting from some argument x0, we have a proof of accessibility acc r x0 (i.e., no infinite descending r-chains starting at x0), then the fixpoint of f can be defined by structural recursion on the proof of accessible_x0.

  • fix_F is structurally recursive on accessible_x0 since the recursive call is on an element h1 y r_yx, i.e., a child node of the (possibly infinitely branching) tree rooted at AccIntro h1.

A slightly simpler version of fix_F is derivable if r is well-founded, i.e., r is accessible for all elements x:a.

let fix (#aa:Type) (#r:binrel aa) (rwf:well_founded r)
        (p:aa -> Type) (f:(x:aa -> (y:aa -> r y x -> p y) -> p x))
        (x:aa)
  : p x
  = fix_F f x (rwf x)

Some Well-founded Relations

We show how to buid some basic well-founded relations here. For starters, since F* already internalizes that the < ordering on natural numbers as part of its termination check, it is easy to prove that < is well-founded.

let lt_nat (x y:nat) : Type = x < y == true
let rec wf_lt_nat (x:nat)
  : acc lt_nat x
  = AccIntro (fun y _ -> wf_lt_nat y)

We can also define combinators to derive well-founded relations from other well-founded relations. For example, if a relation sub_r is a sub-relation of a well-founded relation r (meaning we have r x y whenever we have sub_r x y), then sub_r is well-founded too.

let subrel_wf (#a:Type) (#r #sub_r:binrel a)
              (sub_w:(x:a -> y:a -> sub_r x y -> r x y))
              (r_wf:well_founded r)
  : well_founded sub_r
  = let rec aux (x:a)
                (acc_r:acc r x)
      : Tot (acc sub_r x) (decreases acc_r)
      = AccIntro 
          (fun y sub_r_y_x ->
             aux y (acc_r.access_smaller y (sub_w y x sub_r_y_x)))
    in
    fun x -> aux x (r_wf x)

Another useful combinator derives the well-foundedness of a relation r: binrel b if it can be defined as the inverse image under some function f: a -> b of some other well-founded relation r: binrel.

let inverse_image (#a #b:Type) (r_b:binrel b) (f:a -> b) : binrel a =
  fun x y -> r_b (f x) (f y)

let inverse_image_wf (#a #b:Type) (#r_b:binrel b)
                     (f:a -> b)
                     (r_b_wf:well_founded r_b)
  : well_founded (inverse_image r_b f)
  = let rec aux (x:a)
                (acc_r_b:acc r_b (f x))
      : Tot (acc (inverse_image r_b f) x)
            (decreases acc_r_b)
      = AccIntro (fun y p -> aux y (acc_r_b.access_smaller (f y) p)) in
    fun x -> aux x (r_b_wf (f x))

For example, the > ordering on negative numbers can be proven well-founded by defining it as the inverse image of the < ordering on natural numbers.

let neg = x:int { x <= 0 }
let negate (x:neg) : nat = -x
let gt_neg : binrel neg = inverse_image lt_nat negate
let wf_gt_neg = inverse_image_wf negate wf_lt_nat

Termination Checking with Custom Well-founded Relations

In the F* library, FStar.LexicographicOrdering, several other relations are proven to be well-founded, including the lexicographic ordering on dependent pairs.

noeq
type lexicographic_order (#a:Type)
                         (#b:a -> Type)
                         (r_a:binrel a)
                         (r_b:(x:a -> binrel (b x)))
  : (x:a & b x) -> (x:a & b x) -> Type =
  | Left_lex:
    x1:a -> x2:a ->
    y1:b x1 -> y2:b x2 ->
    r_a x1 x2 ->
    lexicographic_order r_a r_b (| x1, y1 |) (| x2, y2 |)

  | Right_lex:
    x:a ->
    y1:b x -> y2:b x ->
    r_b x y1 y2 ->
    lexicographic_order r_a r_b (| x, y1 |) (| x, y2 |)

This order, defined as a binrel (x:a & b x), and is paramterized by a binary relation (r_a) on a and a family of relations (r_b) on b x, one for each x:a. It has two cases:

  • Left_lex: The first component of the pair decreases by r_a, and the second component is irrelevant.

  • Right_lex: The first component of the pair is invariant, but the second component decreases by r_b.

The proof is a little involved (see FStar.LexicographicOrdering.fst), but one can prove that it is well-founded when r_a and r_b are themselves well-founded, i.e.,

val lexicographic_order_wf (#a:Type) (#b:a -> Type)
                           (#r_a:binrel a)
                           (#r_b:(x:a -> binrel (b x)))
                           (wf_a:well_founded r_a)
                           (wf_b:(x:a -> well_founded (r_b x)))
  : well_founded (lexicographic_order r_a r_b)

But, with this well-foundedness proof in hand, we can define recursive functions with our own well-founded orders.

To illustrate, let’s define the ackermann function again (we saw it first here), this time using accessibilty and well-founded relations, rather than the built-in precedes relation.

//A type abbreviation for a pair of nats
//  we're using dependent pairs, even though there's no real dependence here
let nat_pair = (x:nat & nat)

//Making a lexicographic ordering from a pair of nat ordering
let lex_order_nat_pair 
  : binrel nat_pair
  = lexicographic_order lt_nat (fun _ -> lt_nat)

// The lex order on nat pairs is well-founded, using our general proof
// of lexicographic composition of well-founded orders
let lex_order_nat_pair_wf 
  : well_founded lex_order_nat_pair
  = lexicographic_order_wf wf_lt_nat (fun _ -> wf_lt_nat)

// A utility to introduce lt_nat
let mk_lt_nat (x:nat) (y:nat { x < y }) 
  : lt_nat x y
  = let _ : equals (x < y) true = Refl in
    ()
    
// A utility to make a lex ordering of nat pairs
let mk_lex_order_nat_pair (xy0:nat_pair) 
                          (xy1:nat_pair {
                            let (|x0, y0|) = xy0 in
                            let (|x1, y1|) = xy1 in
                            x0 < x1 \/ (x0 == x1 /\ y0 < y1)
                          })
  : lex_order_nat_pair xy0 xy1
  = let (|x0, y0|) = xy0 in
    let (|x1, y1|) = xy1 in
    if x0 < x1 then Left_lex x0 x1 y0 y1 (mk_lt_nat x0 x1)
    else Right_lex x0 y0 y1 (mk_lt_nat y0 y1)

// Defining ackermann, where `arec` is called for recursive calls
// on pairs that precede xy, lexicographically
let ackermann' (xy: nat_pair)
               (arec: (xy':nat_pair -> lex_order_nat_pair xy' xy -> nat))
  : nat
  = let (| x, y |) = xy in
    if x = 0 then y + 1
    else if y = 0 then arec (| x - 1, 1 |) (mk_lex_order_nat_pair _ _)
    else arec (| x - 1, arec (| x, y - 1|) (mk_lex_order_nat_pair _ _) |)
              (mk_lex_order_nat_pair _ _)

// Tie the knot with `fix`
let ackermann : nat_pair -> nat = fix lex_order_nat_pair_wf (fun _ -> nat) ackermann'

This version is way more verbose than the ackermann we saw earlier—but this version demonstrates that F*’s built-in support for the lexicographic orders over the precedes relation is semantically justified by a more primitive model of well-founded relations

To make user-defined well-founded orderings easier to work with, F* actually provides a variant of the decreases clause to work with well-founded relations. For example, one can use the following syntax to gain from F*’s built-in from SMT automation and termination checking, with the expressiveness of using ones own well-founded relation.

module L = FStar.LexicographicOrdering
let rec ackermann_wf (m n:nat)
   : Tot nat 
     (decreases 
       {:well-founded 
         L.lex (coerce_wf wf_lt_nat) (fun _ -> (coerce_wf wf_lt_nat)) (| m, n |) 
       })
  = if m = 0 then n + 1
    else if n = 0 then ackermann_wf (m - 1) 1
    else ackermann_wf (m - 1) (ackermann_wf m (n - 1))

To explain the syntax:

  • decreases {:well-founded p x}: Here, p is meant to be an instance for FStar.LexicographicOrdering.well_founded_relation, applied to some term x built from the formal parameters in scope.

  • In this case, we use the combinator L.lex to build a lexicographic ordering from wf_lt_nat (coercing it using a utility coerce_wf to turn the definitions used in our tutorial chapter here to the types expected by the FStar.LexicographicOrdering library).

We show the coercions below for completeness, though one would not necessarily need them outside the context of this tutorial.

module W = FStar.WellFounded
let rec coerce #a #r #x (p:acc #a r x)
  : Tot (W.acc r x) (decreases p)
  = W.AccIntro (fun y r -> coerce (p.access_smaller y r))

let coerce_wf #a #r (p: (x:a -> acc r x))
  : x:a -> W.acc r x
  = fun x -> coerce (p x)