More than 5 years have passed since last update.
「リストは自分自身のfoldr関数として定義される」について
「リストは自分自身のfoldr関数として定義される」について
2014_05_11 @suharahiromichi
はじめに
TAPL（参考文献1.)には、p.47とp.275の2箇所に渡って、「リストは自分自身のfoldr関数として定義される」と書かれている。しかし、前後の説明を読んでもこの一文の意味することはよくわからなかった。
また、別なところ（同 p.277）で、「(System Fは)fixに頼ることなく純粋な言語でソート関数のようなものが書ける…」と極めて重要なことが書いてある。これは、チャーチ数やリストのチャーチ表現がそのような性質を持つのであって、System Fはそれらを扱える（型付けをすることができる）と理解するべきなのだろう。
以上のことを納得するために、数やリストについて、
- Inductiveな定義
- チャーチ表現
- fold関数
の関係を調べてみる。証明はCoq SSRefelctで行う。
この文章のソースコードは、以下にあります。
https://github.com/suharahiromichi/coq/blob/master/ssr/ssr_church_number.v
RequireImportssreflectssrboolssrnat.チャーチ数
チャーチ数(CNat)
DefinitionCNat:=forallX,(X->X)->X->X.DefinitionC0:CNat:=funX=>funs:X->X=>funz:X=>z.DefinitionC1:CNat:=funX=>funs:X->X=>funz:X=>sz.DefinitionC2:CNat:=funX=>funs:X->X=>funz:X=>s(sz).DefinitionCSucc:CNat->CNat:=funn:CNat=>funX=>funs:X->X=>funz:X=>s(nXsz).EvalcomputeinCSuccC0.InductiveなNatの定義
InductiveNat:Type:=|O|SofNat.CNatとNatの間の変換
CNatをNatに変換する関数
DefinitionCNat2Nat(c:CNat):Nat:=cNatSO.EvalcomputeinCNat2NatC2.= S (S O) : Nat
これはチャーチ数cに、Sをfoldしているとみることもできる。
Fold関数
Inductiveに定義したNatに対しては、Foldを定義しなければならない。
FixpointfoldNat(X:Type)(s:X->X)(z:X)(n:Nat):X:=matchnwith|O=>z|Sn'=>s(foldNatXszn')end.CheckfoldNat.: forall X : Type, (X -> X) -> X -> Nat -> X
NatをCNatに変換する関数
DefinitionNat2CNat(n:Nat):CNat:=funX=>funs:X->X=>funz:X=>foldNatXszn.EvalcomputeinNat2CNat(S(SO)).= fun (X : Type) (s : X -> X) (z : X) => s (s z) : CNat
Inductiveに定義された整数nに、sをFoldし、そのsをλ抽象すると、チャーチ数が得られる。
証明
C0とOが同じ、CSuccとSの結果が同じになることの証明
TheoremCNat_Nat_zero:CNat2NatC0=O.Proof.by[].Qed.TheoremCNat_Nat_succ:forallcn,CNat2Natc=n->CNat2Nat(CSuccc)=Sn.Proof.rewrite/CNat2Nat/CSucc.bymove=>cn->.Qed.CNat2NatとNat2CNatで元に戻ることの証明
TheoremCNat2Nat_Nat2CNat:foralln:Nat,CNat2Nat(Nat2CNatn)=n.Proof.rewrite/CNat2Nat/Nat2CNat.elim.by[].bymove=>/=n0->.Qed.自然数のリスト
要素の自然数は、SSReflectのnatの定義を使う。
チャーチ表現
DefinitionCListNat:=forallR,(nat->R->R)->R->R.DefinitionCNil:CListNat:=funR=>func:nat->R->R=>funn:R=>n.(* [] *)DefinitionCL1:CListNat:=funR=>func:nat->R->R=>funn:R=>c1n.(* [1] *)DefinitionCL2:CListNat:=funR=>func:nat->R->R=>funn:R=>c1(c2n).(* [1,2] *)DefinitionCL3:CListNat:=funR=>func:nat->R->R=>funn:R=>c1(c2(c3n)).(* [1,2,3] *)DefinitionCCons:nat->CListNat->CListNat:=funhd:nat=>funtl:CListNat=>funR=>func:nat->R->R=>funn:R=>chd(tlRcn).EvalcomputeinCCons1CNil.Inductiveな定義
InductiveListNat:Type:=|Nil|Consofnat&ListNat.clistとlistの間の変換
clistをlistに変換する関数
Definitionclist2list(c:CListNat):ListNat:=cListNatConsNil.Evalcomputeinclist2listCL2.= Cons 1 (Cons 2 Nil) : ListNat
clist2listは、チャーチ表現のリストcに、Consをfoldrしているとみることもできる。
Foldr関数
Inductiveに定義したlistに対しては、Foldを定義しなければならない。
Fixpointfoldr(R:Type)(c:nat->R->R)(n:R)(l:ListNat):R:=matchlwith|Nil=>n|Consxl'=>cx(foldrRcnl')end.Checkfoldr.: forall R : Type, (nat -> R -> R) -> R -> ListNat -> R
listをclistに変換する関数
Definitionlist2clist(l:ListNat):CListNat:=funR=>func:nat->R->R=>funn:R=>foldrRcnl.Evalcomputeinlist2clist(Cons1(Cons2Nil)).= fun (R : Type) (c : nat -> R -> R) (n : R) => c 1 (c 2 n) : CListNat
Inductiveに定義されたリストlに、cをFoldrし、そのcをλ抽象すると、チャーチ表現で表したリストが得られる。
証明
CNilとnilが同じ、CConsとConsの結果が同じになることの証明
Theoremclist_list_nil:clist2listCNil=Nil.Proof.by[].Qed.Theoremclist_list_cons:forallcln,clist2listc=l->clist2list(CConsnc)=Consnl.Proof.rewrite/clist2list/CCons.bymove=>cln->.Qed.clist2listとlist2clistで元に戻ることの証明
Theoremclist2list_list2clist:foralll:ListNat,clist2list(list2clistl)=l.Proof.rewrite/clist2list/list2clist.elim.by[].bymove=>/=nl->.Qed.まとめ
わかったこと。チャーチ数やリストのチャーチ表現は、それ自身にFoldの機能を持っていること。また、Inductiveに定義したnatやlistは、Fold関数によってチャーチ表現に変換できること。
参考文献2.は、無限大のチャーチ数と不動点演算子の関係をHaskellで論じたもので、FoldNatの定義などを参考にさせていただいた。
参考文献
- Pierce、住井 監訳「型システム入門 プログラミング言語と型の理論」オーム社
- 酒井 「不動点演算子はチャーチ数での無限大?」 http://msakai.jp/d/?date=20100628
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme