### 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 _>_ xThe 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 xThe

`_≤_`

proposition on natural numbers can be defined as
data _≤_ : ℕ -> ℕ -> Set where ≤-refl : {n : ℕ} -> n ≤ n ≤-step : {m n : ℕ} -> m ≤ n -> m ≤ suc nin 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 _>_ mNow 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>mFinally 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。）

Labels: Agda

看不懂是正常吼~

Accessibility 出現之後看不懂是正常的 XD。

<< 回到主頁