日々の流転

λ. Wellfounded induction in Agda2

Coqの整礎帰納法(Wellfounded induction)はどうやって実現されているのか見てみたら、accessibility predicate を定義して、それに対する通常の帰納法になっているようだった。 なるほど、整礎帰納法は accessibility predicate に関する通常の帰納法になってしまうのね。面白い。 Coqはまだ良くわからないので、とりあえずAgda2で似たようなもの(?)を書いてみる。

Rel : Set -> Set1
Rel X = X -> X -> Set

-- The accessibility predicate
data Acc {X : Set} (_<_ : Rel X) (x : X) : Set where 
  AccIntro : ((y : X) -> y < x -> Acc _<_ y) -> Acc _<_ x

-- A relation is wellfounded if every element is accessible
Wellfounded : {X : Set} -> (R : Rel X) -> Set
Wellfounded {X} R = (x : X) -> Acc R x

-- Wellfounded induction
wInd : {X : Set} -> {_<_ : Rel X} -> (wf : Wellfounded _<_) ->
       {P : X -> Set} ->
       ((x : X) -> ((y : X) -> y < x -> P y) -> P x) ->
       (x : X) -> P x
wInd {X} {_<_} wf {P} F x = f x (wf x)
  where
    f : (x : X) -> (Acc _<_ x) -> P x
    f x (AccIntro ch) = F x (\y r -> f y (ch y r))

これを length (filter p xs) ≦ length xs の証明 と組み合わせると、ようやく停止性の証明されたクイックソートが書けそうw

あと、一階述語論理と違ってCoqやAgdaで整礎性を表現できるのは、単なる不動点ではなく最小不動点を定義できるからか。一階述語論理の「Acc(x) ⇔ ∀y. y < x → Acc(y)」だと最小不動点であることを表現できないのが問題になる。

関連

• 整礎性は一階述語論理では表現できないのね - ヒビルテ(2007-12-05)