ラムダ・キューブ

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

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

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

λ→: 項に依存した項（単純型付きラムダ計算）; 一階命題論理; （これを以下全てが含む。）
λ2: 型に依存した項（System F）; パラメトリック多相; 二階命題論理
λω: 型に依存した型（System Fω）; 型オペレータ; 弱性高階命題論理
λω: 型に依存した型、型に依存した項（System Fω）; 型構築子; 高階命題論理; λ2とλωの融合
λP: 項に依存した型（ $\lambda \Pi$ ）; 依存型; 一階述語論理
λP2: 型に依存した項、項に依存した型（ $\lambda \Pi 2$ ）; 依存型; 二階述語論理; λPとλ2の融合
λPω: 項に依存した型、型に依存した型（ $\lambda \Pi {\underline {\omega }}$ ）; 依存型; 弱性高階述語論理; λPとλωの融合
λC: 型に依存した型、型に依存した項、項に依存した型（ $\lambda \Pi \omega$ ）; CoC; 高階述語論理; λP2とλPωの融合

参考文献

Barendregt, Henk, “Lambda Calculi with Types”, Handbook of Logic in Computer Science, Volume II, Oxford University Press, ISBN 0-19-853761-1, ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps