トップ «前の日記(2006-05-01) 最新 次の日記(2006-05-04)» 月表示 編集

日々の流転


2006-05-03 [長年日記]

λ. CCの後継色々

CC(Calculus of Constructions)を発展させた型理論には色々あるが、それぞれどういう関係にあるんだろう。どっかに系統図とかないかな…

  • GCC (Generalized Calculus of Constructions)
  • ECC (Extended Calculus of Constructions)
  • UTT (A Unifying Theory of Dependent Types)
  • CIC (Calculus of Inductive Constructions)
Tags: 型理論

λ. “ECC, an Extended Calculus of Constructions” by Zhaohui Luo

とりあえず、ECCの定義だけ確認した。ECCはCCに強い依存直和(strong dependent sum)と型の階層(cumulative type hierarchy)とを導入したもの。CCに強い依存直和を追加したものではジラールの逆理が成り立ってしまうことが知られているので、どうするんだろうと思っていたんだが、型の階層を導入し強い依存直和の規則をpredicativeなものにすることで回避している。

また、型の階層は Prop⊆Type0⊆Type1⊆Type2,…のような階層になっていて、一番下のPropの依存直積だけはimpredicativityを許している。例えば ∏(A:Prop).(A→A)→A→A はPropに属するので、Recursive types for free!の方法で再帰的データ型を表現可能(c.f. AgdaのようなMartin-Löf流のpredicativeな型システムだとこれは不可能)。

欠点としてはη簡約とsurjective-pairingを含まないことがある。それらを追加するとチャーチ・ロッサー性が成り立たなくなる。

ところで、Zhaohui Luo って漢字だと「罗朝晖」と書くのでしょうか?

関連