Lambda立方體

λ-立方。箭頭的方向展示了包含關係。

在數理邏輯和類型論中，λ-立方是探索 Coquand 的構造演算中細化軸的框架，以簡單類型 λ-演算（在立方圖中寫作 λ→）作為原點放在立方體的頂點，而構造演算（即高階依賴類型化 λ-演算，在圖中寫作 λPω）則是其空間對頂點。立方體的每個軸都表示一種新的抽象形式：

• 值依賴類型，或多態。系統F，即二階λ-演算（圖中寫作 λ2）就是通過只加入此性質得到的。
• 類型依賴類型，或類型構造器。帶類型構造器的簡單類型 λ-演算（圖中為$\lambda {\underline {\omega }}$）就是通過只加入此性質得到的。它與系統F結合就產生了系統Fω（在圖中寫作不帶下劃線的λω）。
• 類型依賴值，或依賴類型。只加入此性質就得到了λΠ（在圖中寫作λP），一種與LF緊密相關的類型系統。

所有的八種演算包含了最基本的抽象形式，值依賴值即簡單類型 λ-演算中的普通函數。此立方中最豐富的演算即構造演算，它帶有所有三種抽象。所有八種演算都是強規範化的。

然而子類型並未展示在此立方中，儘管像$F_{<:}^{\omega }$ 這樣以高階有界量化聞名的，結合了子類型和多態的系統具有實際意義，它可被進一步推廣為有界類型構造器。進一步擴展到$F_{<:}^{\omega }$允許純函數對象的定義；這些系統通常在λ-立方的論文發表後才被開發出來。$F_{<:}^{\omega }$

此立方的思想來源於Henk Barendregt (1991)。就此立方的所有角而言，純類型系統的框架涵蓋了λ-立方，其它一些系統也可表示為此通用框架的實例。 此框架的出現比λ-立方早上幾年。在 Barendregt 1991年的論文中，他也在此框架中定義了λ-立方的角。

Olivier Ridoux 在他的 Habilitation à diriger les recherches Lambda-Prolog de A à Z... ou presque 中給出了此立方的一個截邊角後的模版(p. 70) 的兩種表示，一種將此立方表示為一個八面體，其中 8 個頂點以面代替，另一種將它表示為一個十二面體，其中 12 條棱則以面代替。

參見

• Some of the systems included in the cube were first defined in Automath.
• 同倫類型論

擴展閱讀

• Simon Peyton Jones and Erik Meijer, 1997. Henk: A Typed Intermediate Language （頁面存檔備份，存於互聯網檔案館）

外部連結

• Barendregt's Lambda Cube （頁面存檔備份，存於互聯網檔案館） in the context of pure type systems by Roger Bishop Jones