ラムダ・キューブのソースを表示

[[Image:Lambda_cube.png|ラムダ・キューブの図。上向き軸はパラメトリック多相、奥向き軸は型オペレータ、右向き軸は依存型。|サムネイル|250x250ピクセル]]
[[型理論]]において、'''ラムダ・キューブ''' ('''{{lang|en|Lambda cube}}''') とは、8つの異なる[[型付きラムダ計算]]の関係を表した図である。これらの計算体系がそれぞれ型（type）と項（term）の間にどのような依存関係を認めるかを整理したもので、[[単純型付きラムダ計算]]から、{{仮リンク|Calculus of Constructions (CoC)|en|calculus of constructions}}を導くフレームワークになっている。数学者ヘンク・バレンドレフトによって1991年に提唱された。

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

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

==参考文献==
* {{citation
  | first = Henk | last = Barendregt | authorlink = ヘンク・バレンドレフト
  | contribution = Lambda Calculi with Types
  | contribution-url = ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
  | title = Handbook of Logic in Computer Science
  | volume = Volume II
  | publisher = Oxford University Press
  | isbn = 0-19-853761-1
}}

{{DEFAULTSORT:らむたきゆうふ}}
[[Category:型理論]]
[[Category:ラムダ計算]]