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\; (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 < 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.

Programs

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