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 ≤ 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

2 thoughts on “Well-Founded Recursion and Accessibility

  1. Oleg

    Perhaps 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

    Reply
  2. Shin Post author

    Oleg, 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.

    Reply

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>