Accessibility and Strong Induction

Accessibility becomes more accessible if one compares it with the proof of "induction implies strong induction". The ordinary induction principle on natural numbers is

Note that when proving P(n+1) we can only presuppose P(n). On the other hand, strong induction permits us presuppose P(0) through P(n) when proving P(n+1):

The two induction principles are equivalent. Proof of "strong induction implies ordinary induction" is trivial. As for the reverse direction, we can first rewrite "∀k<n. P(k)" in the premise of strong induction more intuitively as Q(n) = P(0) ∧ P(1) ∧ ... ∧ P(n-1). The strategy now is proving "∀n. Q(n)" from the assumption "Q(n) => P(n)" by ordinary induction, and then applying the premise to every Q(n) and get "∀n. P(n)". The proof goes:

• When n = 0, Q(0) is vacuously true.
• Suppose Q(n) = P(0) ∧ P(1) ∧ ... ∧ P(n-1) holds. Since Q(n) => P(n), we have P(n) as well. It follows that Q(n+1) = Q(n) ∧ P(n) also holds.

Now compare with the Agda definition of accessibility:

data Acc {A : Set} (_>_ : A -> A -> Set) (x : A) : Set where
  acc : (forall y -> x > y -> Acc _>_ y) -> Acc _>_ x

The proposition which accessibility wishes to prove is a bit weird, though (since it's recursively defined). Comparing with the proof above and roughly speaking, P and Q are both Acc _>_, i.e., Q(n) = Q(0) ∧ Q(1) ∧ ... ∧ Q(n-1). Although what acc encapsulates is a dependent function and not the more familiar form of product, but the effect of (x : A) -> B x is just using x to index one member of some set of B's and therefore encoding a (possibly infinite) product. For this reason, dependent functions are also called dependent products.

We call a relation R over A is well-founded if every element of A is accessible under R.

well-found : {A : Set} -> (A -> A -> Set) -> Set
well-found R = forall x -> Acc R x

The _≤_ proposition on natural numbers can be defined as

data _≤_ : ℕ -> ℕ -> Set where
  ≤-refl : {n : ℕ} -> n ≤ n
  ≤-step : {m n : ℕ} -> m ≤ n -> m ≤ suc n

in which suc n means the successor of n (i.e., 1+n). Define m > n = suc n ≤ m. We can prove that _>_ is well-founded:

ℕ>-wf : well-found _>_

According to the definition of well-found, we have to prove that Acc _>_ n holds for all n. Given n, the only way to prove Acc _>_ n is to prove Acc _>_ 0 ∧ Acc _>_ 1 ∧ ... ∧ Acc _>_ (n-1) (this is what the constructor acc says), which is represented by dependent functions in Agda --- given an index m, return Acc _>_ m.

conjunction : forall n -> forall m -> n > m -> Acc _>_ m

Now we imitate the proof above and do ordinary induction on n. When n = 0 the proposition is vacuously true:

conjunction zero _ ()

Suppose conjunction n = Acc _>_ 0 ∧ Acc _>_ 1 ∧ ... ∧ Acc _>_ (n-1) holds. What we wish to construct is a product Acc _>_ 0 ∧ Acc _>_ 1 ∧ ... ∧ Acc _>_ (n-1) ∧ Acc _>_ n, encoded as a dependent function. Given an index m, we have to hand out the corresponding Acc _>_ m, so we do case analysis on m. The last term Acc _>_ n is constructed from conjunction n:

conjunction (suc n) .n ≤-refl = acc (conjunction n)

For the other indices we just take the corresponding term in conjunction n:

conjunction (suc n) m (≤-step n>m) = conjunction n m n>m

Finally let's return to the well-foundedness of _>_. Since we can prove conjunction n for any n,

ℕ>-wf n = acc (conjunction n)

--
關於 accessibility 的直白解釋和使用例子，請期待〈Algebra of Programming using Dependent Types〉journal 版！（我對於「什麼時候才會公開」沒有概念 XD。）