# 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)
```