Since Nils Anders Danielsson showed me how to use `Induction.WellFounded`

in Agda’s Standard Library, I have been studying issues related to well-founded recursion.

In dependently typed programming, we would like to ensure that proof terms are terminating. Apart from the type checker, Agda employs a separate termination checker. How it exactly works is still at times mysterious to me, but basically it recognises a program as terminating if some of its arguments become “structurally” smaller after each recursive call. This is already far more expressive than I thought — quite a number of programs can be written by structural recursion. Still, we occasionally need some more flexibility. One of such occasion was when I wished to express terminating unfolds in AoPA. For another example, consider this function mentioned in the paper Terminating General Recursion by Bengt Nordström:

$f\; (n,\; k)\; =\; if\; k\; \le \; n\; then\; n\; else\; f(f\; (n\; +\; 1,\; k),\; k)$

It is a variation of McCarthy’s 91 function, used as a popular example due to its non-trivial recursion pattern. Can we express this function in Agda while informing the termination checker that it does terminate?

Given a relation

### Accessibility

Given a binary relation `_<_ : a -> a -> Set`

, an element `x`

is in the *well-founded subset* of `<`

if there is no infinite chain of `x₁, x₂, x₃ ... `

such that `x > x₁ > x₂ > x₃ > ...`

. The relation is *well-founded* if all elements of `a`

are in its well-founded subset. The less-than ordering on natural number is well-founded, while the greater-than ordering is not. A more constructive way to talk about well-foundedness is via *accessibility*. Given a relation `_<_ : a -> a -> Set`

, the proposition `Acc _<_ x`

states that `x`

is accessible under relation `<`

. An element `x : a`

is accessible if all `y : a`

"smaller" than `x`

are accessible:

`data Acc {a : Set}(_<_ : a -> a -> Set) : a -> Set where`

acc : (x : a) -> (forall y -> y < x -> Acc _<_ y) -> Acc _<_ x

A relation `_<_ : a -> a -> Set`

is well-founded if all elements in `a`

are accessible:

`well-found : {a : Set} -> (a -> a -> Set) -> Set`

well-found _<_ = forall x -> Acc _<_ x

For an example, consider the less-than-or-equal-to ordering on natural numbers. It is usually modelled by a datatype stating that `0 ≤ n`

for all `n`

and that `1+m ≤ 1+n`

follows from `m ≤ n`

. The strictly-less-than ordering is defined by `m < n = 1+m ≤ n`

. For well-foundedness proofs, however, the following definitions turn out to be more convenient:

`data _≤′_ : ℕ -> ℕ -> Set where`

≤′-refl : forall {n} -> n ≤′ n

≤′-step : forall {m n} -> m ≤′ n -> m ≤′ suc n

`_<′_ : ℕ -> ℕ -> Set`

m <′ n = suc m ≤′ n

Let's prove that `<′`

is well-founded:

`ℕ<-wf : well-found _<′_`

ℕ<-wf n = acc n (access n)

where

access : (n : ℕ) -> (m : ℕ) -> m <′ n -> Acc _<′_ m

access zero m ()

access (suc n) .n ≤′-refl = acc n (access n)

access (suc n) m (≤′-step m<n) = access n m m<n

An operational intuition for `access`

: knowing that `m <′ n`

, `access`

demonstrates that it is possible to reach `m`

from `n`

in a finite number of steps.

### Well-Founded Recursion

As an inductively defined datatype, `Acc`

naturally induces a fold operator:

`acc-fold : {a : Set} (_<_ : a -> a -> Set) {P : a -> Set} ->`

((x : a) -> (forall y -> y < x -> P y) -> P x) ->

(z : a) -> Acc _<_ z -> P z

acc-fold _<_ Φ z (acc .z h) =

Φ z (\y y<z -> acc-fold _<_ Φ y (h y y<z))

Its type says that if we can provide a function `Φ`

that proves some property `P x`

for all `x`

provided that `P y`

has been proved for all `y < x`

, then `P`

holds for all accessible elements in `a`

. Recall strong induction.

When `<`

is well-founded, all elements are accessible. Therefore we can define:

`rec-wf : {a : Set} {_<_ : a -> a -> Set} {P : a -> Set} ->`

well-found _<_ ->

((x : a) -> ((y : a) -> y < x -> P y) -> P x) ->

(x : a) -> P x

rec-wf {a}{_<_} wf f x = acc-fold _<_ f x (wf x)

For an example, consider the function `div : ℕ -> ℕ -> ℕ`

performing integral division (but letting `div zero zero`

be `zero`

):

`div : ℕ -> ℕ -> ℕ`

div zero n = zero

div (suc m) zero = suc m

div (suc m) (suc n) = suc (div (suc m ∸ suc n) (suc n))

If we define `div`

by well-founded recursion with explicit fixed-point, it looks like:

`div-wf : ℕ -> ℕ -> ℕ`

div-wf m n = rec-wf ℕ<-wf (body n) m

where

body : (n : ℕ) -> (m : ℕ) -> ((k : ℕ) -> k <′ m -> ℕ) -> ℕ

body n zero rec = zero

body zero (suc m) rec = suc m

body (suc n) (suc m) rec =

suc (rec (suc m ∸ suc n) (sm-sn<sm m n))

where `sm-sn<sm : forall m n -> (m ∸ n) <′ suc m`

. Notice how `rec-wf ℕ<-wf`

behaves like a fixed-point operator taking the "fixed-point" of `body`

. The recursive call is replaced by a function `rec`

, having type `(m : ℕ) -> m <′ n -> ℕ`

. To call `rec`

, the programmer has to provide a proof that the argument is indeed getting smaller with respect to the relation `_<_`

.

The function could also be written without explicit fixed-point, but with explicit pattern matching with the accessibility proof:

`div-wf' : forall m -> ℕ -> Acc _<′_ m -> ℕ`

div-wf' zero n _ = zero

div-wf' (suc m) zero _ = suc m

div-wf' (suc m) (suc n) (acc .(suc m) h) =

suc (div-wf' (suc m ∸ suc n) (suc n)

(h (suc m ∸ suc n) (sm-sn<sm m n)))

### Upper-Bounded Reverse Ordering

As a practice, let us consider another ordering. For a given natural number `k`

, define `n ◁ m = m < n ≤ k`

. That is, for `m`

and `n`

upper-bounded by `k`

, the one closer to `k`

is considered smaller. Apparently `◁`

is well-founded. I tried to encode it in Agda by:

`_<_≤_ : ℕ -> ℕ -> ℕ -> Set`

m < n ≤ k = (m <′ n) × (n ≤′ k)

`◁ : ℕ -> ℕ -> ℕ -> Set`

(◁ k) m n = n < m ≤ k

However, the accessibility proof became very difficult to construct. I ended up defining yet another variation of the less-than-or-equal-to ordering:

`data _≤′′_ : ℕ -> ℕ -> Set where`

≤′′-refl : forall {n} -> n ≤′′ n

≤′′-step : forall {m n} -> suc m ≤′′ n -> m ≤′′ n

and defined `m < n ≤ k = (m <′′ n) × (n ≤′′ k)`

.

A number of properties can be proved about `≤′`

:

`m≤n⇒m≤1+n : forall {m n} -> m ≤′′ n -> m ≤′′ (suc n)`

m<n⇒¬n≤m : forall {m n} -> m <′′ n -> ¬ (n ≤′′ m)

¬[m<n∧n≤m] : forall {m n} -> ¬ (m <′′ n × n ≤′′ m)

≤′′-trans : forall {m n k} -> m ≤′′ n -> n ≤′′ k -> m ≤′′ k

≤′′-antisym : forall {m n} -> m ≤′′ n -> n ≤′′ m -> m ≡ n

Some of the properties above depends on the following:

`¬1+n≤n : forall {n} -> ¬ (suc n ≤′′ n)`

which I have not yet proved.

Now let us show that `◁ k`

is well-founded.

`ℕ◁-wf : forall k -> well-found (◁ k)`

ℕ◁-wf k m = acc m access

where

access : forall n -> (m < n ≤ k) -> Acc (◁ k) n

access n (m<n , n≤k) =

◁-access k m n (≤′′-trans m<n n≤k) (m<n , n≤k)

The function `◁-access`

needs, apart from proofs of `m < n`

and `n ≤ k`

, a proof of `m < k`

, which can be established by transitivity of `≤′`

. The definition is shown below:

`◁-access : forall k m n ->`

(m <′′ k) -> (m < n ≤ k) -> Acc (◁ k) n

◁-access .(suc m) m .(suc m) ≤′′-refl (≤′′-refl , 1+m≤1+m) =

acc (suc m)

(\y 1+m<y∧y≤1+m -> ⊥-elim (¬[m<n∧n≤m] 1+m<y∧y≤1+m))

◁-access k m .(suc m) (≤′′-step 1+m<k) (≤′′-refl , 1+m≤k) =

acc (suc m) (\y -> ◁-access k (suc m) y 1+m<k)

◁-access .(suc m) m n ≤′′-refl (≤′′-step 1+m<n , n≤1+m) =

acc n (⊥-elim (m<n⇒¬n≤m 1+m<n n≤1+m))

◁-access k m n (≤′′-step 1+m<k) (≤′′-step 1+m<n , n≤k) =

◁-access k (suc m) n 1+m<k (1+m<n , n≤k)

It is perhaps quite hard to understand unless you try to construct it yourself. The reader only needs to notice that in the two recursive calls to `◁-access`

(in the second and the last clause), the argument `m`

is incremented to `suc m`

. That is why we need to include a proof term of `m <′′ k`

as an argument, which becomes structurally smaller in the recursive calls. This is how we inform the termination checker that, although `m`

increases, the distance between `m`

and `k`

shrinks. The proof of `n ≤ k`

, on the other hand, is used to establish the contradictions in the first and the third clause.

### A Variation of McCarthy's 91 Function

Back to the function

`f k n with k ≤? n`

... | yes _ = n

... | no _ = f k (f k (suc n))

certainly does not pass the termination check.

In fact, the second argument (`n`

) to `f`

becomes smaller with respect to `◁ k`

. This is obvious for the inner recursive call (`f k (suc n)`

) since `k ≰ n`

implies `n < 1 + n ≤ k`

. To prove the termination of the outer recursive call, we have to show that `f k n`

actually computes the maximum of `k`

and `n`

. Since `k ≰ n`

, we have `f k (suc n) = k`

. Therefore, `f k (suc n)`

is smaller than `n`

with respect to `◁ k`

.

To prove the termination of `f`

we have to prove something about its result. One of the possible ways to do so is to define:

`P : ℕ -> ℕ -> Set`

P k n = ∃ ℕ (\fn -> n ≤′′ k -> fn ≡ k)

and extend the type of `f`

to:

`f : (k : ℕ) -> (n : ℕ) -> P k n`

Now that `f`

returns an existential type, we have to pattern math its result. A definition of `f`

may look like:

`f k = rec-wf (ℕ◁-wf k) body`

where

body : (i : ℕ) -> ((j : ℕ) -> i < j ≤ k -> P k j) -> P k i

body n rec with (k ≤′′? n)

... | inj₁ k≤n = exists n (\n≤k -> ≤′′-antisym n≤k k≤n)

... | inj₂ n<k with rec (1 + n) (≤′′-refl , n<k)

... | exists m 1+n≤k⇒m≡k with rec m (n<m , m≤k)

... | exists h m≤k⇒h≡k = exists h (\_ -> h≡k)

where

m≡k = 1+n≤k⇒m≡k n<k

n<m = ≡-subst (\i -> n <′′ i) (≡-sym m≡k) n<k

m≤k = ≡-subst (\i -> m ≤′′ i) m≡k ≤′′-ref

h≡k = m≤k⇒h≡k m≤k

However, Agda's scoping rule with the presence of both `with`

and `where`

still confuses me. Eventually I had to inline the subordinate proofs, which gives me:

`f : (k : ℕ) -> (n : ℕ) -> P k n`

f k = rec-wf (ℕ◁-wf k) body

where

body : (i : ℕ) -> ((j : ℕ) -> i < j ≤ k -> P k j) -> P k i

body n rec with (k ≤′′? n)

... | inj₁ k≤n = exists n (\n≤k -> ≤′′-antisym n≤k k≤n)

... | inj₂ n<k with rec (1 + n) (≤′′-refl , n<k)

... | exists m 1+n≤k⇒m≡k with 1+n≤k⇒m≡k n<k

... | m≡k with rec m (≡-subst (\i -> n <′′ i) (≡-sym m≡k) n<k ,

≡-subst (\i -> m ≤′′ i) m≡k ≤′′-refl)

... | exists h m≤k⇒h≡k =

exists h (\_ -> m≤k⇒h≡k (≡-subst (\i -> m ≤′′ i) m≡k ≤′′-refl))

Unfortunately it looks quite remote from the original `f`

. Nevertheless, it does pass the termination checker of Agda.

### Programs

- WellfoundRecursion.agda: the main program.
- DownwardLeq.agda: definition and properties of
`_≤′′_`

.

OlegPerhaps you might find it curious to see how the function f91 is handled in Twelf. Twelf can’t see that f91 is terminating either (let alone that this is the maximum function of two naturals). We have to make the explicit proof. We do not modify the function definition however. Rather, we state the desired property of f91 separately, and constructively prove it. The proof relies on structural induction (because Twelf can hardly do anything else).

Here is the proof

http://okmij.org/ftp/Computation/proving-f91.elf

ShinPost authorOleg, thanks for the Twelf code! It is new to me that termination of f91 can be proved using lexicographic induction, rather than downward induction. Perhaps that allows you to use a more natural definition of <: and <=:, while I had to create the funny ordering _≤′′_.

Meanwhile, as you can see, I have been studying expressing general recursion using coinductive types, which also allows me to prove termination separately from the program. I should try to redo your proof in Agda some day.