ラムダ・キューブ

ラムダキューブ(lambda cube)

単純型付きラムダ計算から、Calculus of Constructions(CoC)までを導く過程を立方体で表している

Henk Barendregt(ヘンク・バレンドレヒト)

$ \rightarrow : x軸: 依存型(dependent type)

$ \nearrow : z軸: 型構築子(type operator)

型演算、型オペレーター、型コンストラクタ、型構築子は同じものを指してるっぽい

λ→

λP

→: ( λ→ ) → λP

単純型付きラムダ計算 + 依存型

$ \lambda \underline{\omega}

$ \nearrow : (λ→) → $ \lambda \underline{\omega}

単純型付きラムダ計算 + 型構築子

弱高階命題計算？(Weak Higher Order Propositional Calculus)

λ2

$ \uparrow : (λ→) → λ2

単純型付きラムダ計算 + 多相型

λω

(λ2 → λω) or ($ \lambda \underline{\omega} → λω)

単純型付きラムダ計算 + 多相型 + 型構築子

λP2

(λ2 → λP2) or (λP → λP2)

単純型付きラムダ計算 + 依存型 + 多相型

$ λP\underline{\omega}

(λP → λPω) or ($ \lambda \underline{\omega} → λPω)

単純型付きラムダ計算 + 依存型 + 型構築子

弱高階述語計算？(Weakly Higher Order Predicate Calculus)

λC

λω → λC

λP2 → λC

$ λP\underline{\omega} → λC

単純型付きラムダ計算 + 依存型 + 多相型 + 型構築子

確認用

Q. ラムダキューブとは

Q. CoCとは