日々の流転

λ. W-typesによる帰納的データ型の表現

まずは W-types の定義と除去規則を示す。

data W (A::Set) (B::A->Set) = sup (a::A) (x::B a->W A B)

elimW (|A::Set) (|B::A->Set)
      (!C::W A B -> Set) 
      (!d::(a::A) -> (f::B a -> W A B) ->
           (g::(b::B a) -> C (f b)) -> C (sup a f))
      (!c::W A B)
      :: C c
elimW = case c of (sup a f)-> d a f (\(b::B a)-> elimW C d (f b))

W-types という名前は Wellorderings から来ていて、順序数(っぽい何か)を整礎な木として構成したものになっている。Martin-Löf の Intuitionistic Type Theory での説明:

The concept of wellordering and the principle of transfinite induction were first introduced by Cantor. Once they had been formulated in ZF, however, they lost their original computational content. We can construct ordinals intuitionistically as wellfounded trees, which means they are no longer totally ordered.

この型それ自体も面白いのだけど、この型を使った面白い事として外延的な型理論ではこれを使って帰納的なデータ型を表現する事が出来るという事が知られている。なので、これをagdaでも表現してみたい。 だが、agdaの型理論は外延的ではないので、まずは「関数は全ての引数に対する値が等しければ等しい」ことを公準として追加する。 ついでに後で使う定義も追加。

postulate ext :: (X,Y::Set) |-> (f,g::X->Y) ->
                 ((x::X) -> Id (f x) (g x)) -> Id f g

data Empty =
data Unit = tt

uu (X::Set) :: Empty -> X
uu e = case e of { }

uu_lemma (X::Set) (!f::Empty -> X) :: Id uu f
uu_lemma = let eid (!e::Empty) :: Id (uu e) (f e)
               eid = case e of { }
           in ext uu f eid

tt_lemma (X::Set) (!f::Unit -> X) :: Id (\(t::Unit)-> f tt) f
tt_lemma = let eid (!t::Unit) :: Id (f tt) (f t)
               eid = case t of (tt)-> refId (f tt)
           in ext (\(t::Unit) -> f tt) f eid

リストの例

例えばリスト型は以下のように表現する事が出来る。

data Maybe (X::Set) = Nothing | Just (x::X)

L (A::Set) :: Maybe A -> Set
L x = case x of
        (Nothing)-> Empty
        (Just a )-> Unit

List' :: Set -> Set
List' A = W (Maybe A) L

Nil' (A::Set) :: List' A
Nil' = sup Nothing uu

Cons' (A::Set) :: A -> List' A -> List' A
Cons' x xs = sup (Just x) (\(t::Unit) -> xs)

elimList' (X::Set)
          (!C::List' X -> Set)
          (!n::C Nil')
          (!c::(x::X) -> (xs::List' X) -> C xs -> C (Cons' x xs))
          (!xs::List' X)
  :: C xs
elimList' =
    let h :: (a::Maybe X) ->
             (f::L a -> W (Maybe X) L) ->
             (g::(b::L a) -> C (f b)) ->
             C (sup a f)
        h a f g =
            case a of
              (Nothing)->
                  substId (\(f'::Empty -> W (Maybe X) L) ->
                           C (sup Nothing f'))
                          (uu_lemma f) n
              (Just x )->
                  let lem :: C (Cons' x (f tt))
                      lem = c x (f tt) (g tt)
                  in substId (\(f'::(t::Unit) -> W (Maybe X) L) ->
                              C (sup (Just x) f'))
                             (tt_lemma f) lem
    in elimW C h xs

ちなみに、substId が必要になっているのは、agdaでは Unit や Empty→X の要素が自動的に同一視される(それらの間に definitional equality が成り立つ)ことはないため。外延的な型理論の中にはこれらが自動的に同一視されるものもある。

コンテナ

コンテナ(Container)の概念を使った場合について後で書く。

参考

• “Representing inductively defined sets by wellorderings in Martin-Löf's type theory” by Peter Dybjer
• “Representing Nested Inductive Types using W-types” by Michael Abbott, Thorsten Altenkirch, and Neil Ghani