# Well-Founded Recursion and Accessibility

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 \left(n, k\right) = if k \le n then n else f\left(f \left(n + 1, k\right), k\right)$

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 < that has been shown to be well-founded, we know that a recursively defined function is terminating if its arguments becomes “smaller” with respect to < at each recursive call. We can encode such well-founded recursion in Agda’s style of structural recusion. The earliest paper I could find about such encoding is Terminating General Recursion by Bengt Nordström. It may have appeared in other forms, however.

### 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 mentioned in the beginning, whose native Agda translation:

```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.