ラムダ・キューブ

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

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

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

λ→

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

一階命題論理

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

λ2

型に依存した項（System F）

パラメトリック多相

二階命題論理

λω

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

型オペレータ

弱性高階命題論理

λω

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

型構築子

高階命題論理

λ2とλωの融合

λP

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

依存型

一階述語論理

λP2

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

依存型

二階述語論理

λPとλ2の融合

λPω

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

依存型

弱性高階述語論理

λPとλωの融合

λC

型に依存した型、型に依存した項、項に依存した型（${\displaystyle \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