ラムダ・キューブ

型理論において、ラムダ・キューブ (Lambda cube) とは、8つの異なる型付きラムダ計算の関係を表した図である。これらの計算体系がそれぞれ型（type）と項（term）の間にどのような依存関係を認めるかを整理したもので、単純型付きラムダ計算から、を導くフレームワークになっている。数学者ヘンク・バレンドレフトによって1991年に提唱された。 （右図参照）ラムダキューブの原点は、単純型付きラムダ計算に相当する。三つの座標軸は、Y軸=パラメトリック多相、Z軸=型オペレータ、X軸=依存型に対応している。X, Y, Zの三軸線を融合した終点のは、Calculus of Constructionsに相当する。 各頂点は、以下の通りである: λ→項に依存した項（単純型付きラムダ計算）一階命題論理（これを以下全てが含む。）λ2型に依存した項（System F）パラメトリック多相λω型に依存した型（System Fω）型オペレータ弱性λω型に依存した型、型に依存した項（System Fω）型構築子λ2とλωの融合λP項に依存した型（）依存型一階述語論理λP2型に依存した項、項に依存した型（）依存型二階述語論理λPとλ2の融合λPω項に依存した型、型に依存した型（）依存型弱性高階述語論理λPとλωの融合λC型に依存した型、型に依存した項、項に依存した型（）CoC高階述語論理λP2とλPωの融合