ラムダ・キューブ

ラムダ・キューブの図。上向き軸はパラメトリック多相、奥向き軸は型オペレータ、右向き軸は依存型。

型理論において、ラムダ・キューブ (テンプレート:Lang) とは、8つの異なる型付きラムダ計算の関係を表した図である。これらの計算体系がそれぞれ型（type）と項（term）の間にどのような依存関係を認めるかを整理したもので、単純型付きラムダ計算から、テンプレート:仮リンクを導くフレームワークになっている。数学者ヘンク・バレンドレフトによって1991年に提唱された。

（右図参照）ラムダキューブの原点は、単純型付きラムダ計算に相当する。三つの座標軸は、Y軸=パラメトリック多相、Z軸=型オペレータ、X軸=依存型に対応している。X, Y, Zの三軸線を融合した終点の$\lambda \mathrm{\Pi }\omega$は、Calculus of Constructionsに相当する。

各頂点は、以下の通りである:

λ→

項に依存した項（単純型付きラムダ計算）

一階命題論理

（これを以下全てが含む。）

λ2

型に依存した項（System F）

パラメトリック多相

二階命題論理

λテンプレート:Underline

型に依存した型（System Fテンプレート:Underline）

型オペレータ

弱性高階命題論理

λω

型に依存した型、型に依存した項（System Fω）

型構築子

高階命題論理

λ2とλテンプレート:Underlineの融合

λP

項に依存した型（$\lambda \mathrm{\Pi }$）

依存型

一階述語論理

λP2

型に依存した項、項に依存した型（$\lambda \mathrm{\Pi }2$）

依存型

二階述語論理

λPとλ2の融合

λPテンプレート:Underline

項に依存した型、型に依存した型（$\lambda \mathrm{\Pi }\underset{\_}{\omega }$）

依存型

弱性高階述語論理

λPとλテンプレート:Underlineの融合

λC

型に依存した型、型に依存した項、項に依存した型（$\lambda \mathrm{\Pi }\omega$）

CoC

高階述語論理

λP2とλPテンプレート:Underlineの融合

参考文献

• テンプレート:Citation