日々の流転

λ. 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)

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

• <URL:http://citeseer.ist.psu.edu/luo89ecc.html>
• <URL:http://jp.citeulike.org/article/612085>

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

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

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

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

関連

• 強い直和?