檢視 Lambda立方體的原始碼

佇數理邏輯佮類型論中，'''λ-立方'''是探索 Coquand 的構造演算中細化軸的框殼，以簡單類型 λ-演算（佇立方圖內底寫作 λ→）做為原點囥佇立方體的頂點，構造演算（即高階依賴類型化 λ-演算，伊佇圖內底寫作 λPω）是其實空間對頂點。立方體每一个軸攏表示一種新的抽象形式：

* 值依賴類型，抑是多態。系統 F，即二階 λ-演算（圖內底寫作 λ 二）就是通過干焦加入此性質得著的。
* 類型依賴類型，或者是這个構造器。帶類型構造器的簡單類型 λ-演算（圖當中為 $ \ lambda { \ underline { \ omega } } $）就是通過干焦加入此性質得著的。伊佮系統 F 結合就產生矣系統 Fω（伊佇圖內底寫作無紮下劃線的 λω）。
* 類型依賴值，抑是依賴類型。只加入此性質就得著矣 λΠ（伊佇圖內底寫作 λP）， 一種佮 LF 有密相關的類型系統。

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

毋過子類型並無展示佇這片立方內底，就算講像 $ F _ { < : } ^ { \ omega } $ 按呢以高階有界量化有名的，結合了子類型佮多態的系統有實際意義，伊會當予人進一步推廣做有界類型構造器。進一步擴展到 $ F _ { < : } ^ { \ omega } $ 允准純函數對象的定義；𪜶遮的系統通常佇 λ-立方的論文發表了後才予人開發出來。$ F _ { < : } ^ { \ omega } $

此立方的思想來源於 Henk Barendregt ( 一千九百九十一 )。自按呢立方的所有的角色，純類型系統的框殼攏包起矣 λ-立方，其他的一寡系統嘛會當表示為此通用框架仔的實例。  佇遐框架仔出來比現 λ-立方早起幾年。佇咧 Barendregt 一九九一年的論文中，伊嘛佇遮咧框殼中定義矣 λ-立方的角。

Olivier Ridoux 佇伊的  Habilitation à diriger les recherches _ Lambda-Prolog de A à Z . . . ou presque _ 著予出現此立方的一个鋩角角邊仔的模版 ( p .   七十 ) 的兩種表示，一種共此立方表示為一个八面體，其中八个頂點以下代替，另外一種共表示做一个十二面體，其中十二條行為以面代替。

==參見==

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

==註記==

==參考來源==

==擴展閱讀==

* Simon Peyton Jones and Erik Meijer , 一千九百九十七 . _ Henk : A Typed Intermediate Language _

==外部連結==

* Barendregt's Lambda Cube in the context of pure type systems by Roger Bishop Jones

[[分類: 待校正]]