有類型 lambda 演算是使用 lambda 符號指示匿名函式抽象的一種有類型的形式化。有類型 lambda 演算是基礎程式語言並且是有類型的函式式程式語言如 ML 和 Haskell 和更間接的指令式程式語言的基礎。它們通過 Curry-Howard同構密切關聯於直覺邏輯並可以被認為是範疇的類的內部語言，比如簡單類型 lambda 演算是笛卡爾閉範疇（CCC）的語言。
基本介紹
- 中文名：有類型λ演算
- 外文名：Typed lambda calculus
簡介,種類,套用,參見,
簡介
有類型lambda演算是使用lambda符號指示匿名函式抽象的一種有類型的形式化。有類型lambda演算是基礎程式語言並且是有類型的函式式程式語言如ML和Haskell和更間接的指令式程式語言的基礎。它們通過Curry-Howard同構密切關聯於直覺邏輯並可以被認為是範疇的類的內部語言，比如簡單類型lambda演算是笛卡爾閉範疇（CCC）的語言。
傳統上，有類型lambda演算被看作無類型lambda演算的精細化。更現代的觀點把有類型lambda演算看做更基礎的理論，而把無類型lambda演算看作它的只有一個類型的特殊情況。
種類
已經研究了各種有類型lambda演算。簡單類型lambda演算的類型只是基本類型（或類型變數）和函式類型。系統T向簡單類型lambda演算擴展了自然數類型和更高階的原始遞歸函式；在這個系統中在可證明在皮亞諾算術中是遞歸函式的所有函式都是可定義的。系統F通過在所有類型上的全稱量化允許多態性；從邏輯的觀點看它可以描述可證明在二階邏輯中是全函式的所有函式。有依賴類型的lambda演算是直覺類型論，構造演算和邏輯框架（LF）的基礎，它是帶有依賴類型的純lambda演算。基於Berardi的工作，Barendregt提議了Lambda立方體來系統化純有類型lambda演算（包括簡單類型lambda演算，系統F，LF和構造演算）之間的關係。
某些有類型lambda演算介入“子類型”的概念，就是說如果A是B的子類型，則類型A的所有項也有類型B。帶有子類型的有類型lambda演算是帶有合取類型的簡單類型lambda演算。
迄今提到的所有西，除了無類型lambda演算是例外，都是“強規範化”的：所有計算都會終止。結論是他們作為邏輯都是自恰的，就是說這裡有無居留（uninhabited）類型。但是存在著不是強規範化的有類型lambda演算。比如帶有所有類型的一個類型（Type:Type）的依賴類型lambda演算由於Girard悖論而不是強規範化的。這個系統也是最簡單的純類型系統，它是推廣Lambda立方體的一種形式化。有明確的遞歸組合子的系統，比如GordonPlotkin的PCF，不是規範化的，但是它們不意圖被解釋為邏輯。實際上，PCF（可計算函式的程式語言）是元典型（prototypical）的有類型的函式式程式語言，這裡的類型被用來確保程式是有良好行為的而不必須是終止的。
套用
有類型lambda演算在為程式語言設計新類型系統的時候扮演了關鍵性角色；這裡類型能力通常捕獲了程式想要的性質，比如程式不會導致記憶體訪問違規。
