Lambda立方體
維基百科,自由的 encyclopedia
在數理邏輯和類型論中,λ-立方是探索 Coquand 的構造演算中細化軸的框架,以簡單類型 λ-演算(在立方圖中寫作 λ→)作為原點放在立方體的頂點,而構造演算(即高階依賴類型化 λ-演算,在圖中寫作 λPω)則是其空間對頂點。立方體的每個軸都表示一種新的抽象形式:
- 值依賴類型,或多態。系統F,即二階λ-演算(圖中寫作 λ2)就是通過只加入此性質得到的。
- 類型依賴類型,或類型構造器。帶類型構造器的簡單類型 λ-演算(圖中為
)就是通過只加入此性質得到的。它與系統F結合就產生了系統Fω(在圖中寫作不帶下劃線的λω)。
- 類型依賴值,或依賴類型。只加入此性質就得到了λΠ(在圖中寫作λP),一種與LF緊密相關的類型系統。
![Thumb image](http://upload.wikimedia.org/wikipedia/commons/1/19/Lambda_cube.png)
所有的八種演算包含了最基本的抽象形式,值依賴值即簡單類型 λ-演算中的普通函數。此立方中最豐富的演算即構造演算,它帶有所有三種抽象。所有八種演算都是強規範化的。
然而子類型並未展示在此立方中,儘管像 這樣以高階有界量化聞名的,結合了子類型和多態的系統具有實際意義,它可被進一步推廣為有界類型構造器。進一步擴展到
允許純函數對象的定義;這些系統通常在λ-立方的論文發表後才被開發出來。
[1]
此立方的思想來源於Henk Barendregt (1991)。就此立方的所有角而言,純類型系統的框架涵蓋了λ-立方,其它一些系統也可表示為此通用框架的實例。[2] 此框架的出現比λ-立方早上幾年。在 Barendregt 1991年的論文中,他也在此框架中定義了λ-立方的角。
Olivier Ridoux 在他的 Habilitation à diriger les recherches Lambda-Prolog de A à Z... ou presque 中給出了此立方的一個截邊角後的模版(p. 70) 的兩種表示,一種將此立方表示為一個八面體,其中 8 個頂點以面代替,另一種將它表示為一個十二面體,其中 12 條棱則以面代替。