Lambda立方體

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

  • 值依賴類型,或多態系統F,即二階λ-演算(圖中寫作 λ2)就是通過只加入此性質得到的。
  • 類型依賴類型,或類型構造器。帶類型構造器的簡單類型 λ-演算(圖中為)就是通過只加入此性質得到的。它與系統F結合就產生了系統Fω(在圖中寫作不帶下劃線的λω)。
  • 類型依賴值,或依賴類型。只加入此性質就得到了λΠ(在圖中寫作λP),一種與LF緊密相關的類型系統。
λ-立方。箭頭的方向展示了包含關係。

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

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

此立方的思想來源於Henk Barendregt (1991)。就此立方的所有角而言,純類型系統的框架涵蓋了λ-立方,其它一些系統也可表示為此通用框架的實例。[2] 此框架的出現比λ-立方早上幾年。在 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.
  • 同倫類型論

註記

  1. ^ Pierce, 2002, chapters 31 and 32
  2. ^ Pierce, 2002, p. 466

參考來源

擴展閱讀

外部連結