簡單類型λ演算

簡單類型 lambda 演算( $\lambda ^{\to }$ )是連接詞只有 $\to$ (函數類型)的有類型 lambda 演算。這使它成為規範的、在很多方面是最簡單的有類型 lambda 演算的例子。

簡單類型也被用來稱呼對簡單類型 lambda 演算的擴展比如積、陪積或自然數(系統 T)甚至完全的遞歸(如PCF)。相反的，介入了多態類型(如系統F)或依賴類型(如邏輯框架)的系統不被當作是簡單類型。簡單類型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入來嘗試避免無類型 lambda 演算的悖論性使用。

類型

簡單類型 lambda 演算的類型構造自基本類型(或類型變量) $\alpha ,\beta ,\gamma ,\dots$ ，給定類型 $\sigma ,\tau \,$ 我們能構造 $\sigma \to \tau$ 。邱奇只使用了兩個基本類型， $o\,$ 是命題的類型， $\iota \,$ 是個體的類型。這種演算經常只有一個基本類型，通常考慮為 $o\,$ 。

$\to$ 是右結合的: 我們讀 $\sigma \to \tau \to \rho$ 為 $\sigma \to (\tau \to \rho )$ 。對每個類型 $\sigma \,$ 我們指派一個數字 $o(\sigma )\,$ ，它是 $\sigma \,$ 的階。對於基本類型，我們設置 $o(\alpha )=0\,$ ，而對於函數類型我們遞歸的定義 $o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))$ 。

項

要定義有給定類型的 lambda 項的集合，我們介入定類型上下文 $\Gamma ,\Delta ,\dots$ ，它們是形如 $x:\sigma \,$ 的類型假定的序列，這裡的 $x\,$ 是變量。我們介入判斷 $\Gamma \vdash t:\sigma$ ，它意味着 $t\,$ 在上下文 $\Gamma \,$ 中是類型 $\sigma \,$ 的項，它們由下列定類型規則給出:

${\frac {}{x:\sigma \vdash x:\sigma }}$	${\Gamma \vdash x:\sigma \quad x\not =y} \over {\Gamma ,y:\tau \vdash x:\sigma }$
${\Gamma ,x:\sigma \vdash t:\tau } \over {\Gamma \vdash \lambda x:\sigma .t:\sigma \to \tau }$	${\Gamma \vdash t:\sigma \to \tau \quad \Gamma \vdash u:\sigma } \over {\Gamma \vdash t\,u:\tau }$

換句話說，

如果 x 有類型 $\sigma \,$ ，我們知道 x 有類型 $\sigma \,$ 。
如果在特定上下文中，可以推導出 x 有類型 $\sigma \,$ ，且有某個不是 x 的 y，則上述上下文與 y 有類型 $\tau \,$ 的事實一起，同樣允許推導出 x 有類型 $\sigma \,$ 。即向上下文增加一個新值不改變現存的值(新值不同於舊值之一)。
如果在特定上下文中，已知 x 有類型 $\sigma \,$ ，可以推導出 t 有類型 $\tau \,$ ，則在同一個上下文中，可以構造lambda 抽象 $\lambda x:\sigma .t\,$ ，它有類型 $\sigma \to \tau$ 。
如果在特定上下文中，可以推導出 t 有類型 $\sigma \to \tau$ 和 u 有類型 $\sigma \,$ ，則在同一個上下文中，可以推導出表達式 $t\,u\,$ 有類型 $\tau \,$ 。這捕獲了函數應用的概念。

閉合項的例子有:

$\lambda x:\alpha .x:\alpha \to \alpha$ (I)
$\lambda x:\alpha .\lambda y:\beta .x:\alpha \to \beta \to \alpha$ (K)
$\lambda x:\alpha \to \beta \to \gamma .\lambda y:\alpha \to \beta .\lambda z:\alpha .xz(yz):(\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma$ (S)。

它們是組合子邏輯的基本組合子的有類型 lambda 演算的表示。

簡單類型 lambda 演算通過 Curry-Howard同構密切相關於只有蘊涵( $\to$ )作為連接詞的直覺邏輯(極小邏輯): 閉合項所居留的類型正好是極小邏輯的重言式。

相同類型的項通過 $\beta \eta \,$ -等價來識別，它是通過方程 $(\lambda x:\sigma .t)\,u=_{\beta }t[x:=u]\,$ 生成的，這裡的 $t[x:=u]\,$ 代表 $t\,$ 帶有 $x\,$ 的所有自由出現都被替代為 $u\,$ ，而 $\lambda x:\sigma .t\,x=_{\eta }t\,$ ，如果 $x\,$ 在 $t\,$ 中不自由出現。簡單類型 lambda 演算(帶有 $\beta \eta \,$ -等價)是笛卡兒閉範疇(CCC)的內部語言。這是 Lambek 首先觀察到的。

重要成果

Tait 在 1967 年證明了 $\beta$ -歸約是強規範化的。作為必然推論 $\beta \eta$ -等價是可判定性的。Statman 在 1977 年證明規範化問題不是基本遞歸的。純語義規範化證明由 Berger 和 Schwichtenberg (Normalisation by evaluation) 在 1991 年給出。
$\beta \eta$ -等價的合一問題是不可判定的。Huet 在 1973 年證明 3 階合一已經是不可判定的了，而 Goldfarb 在 1981 年進而證明了 2 階合一是不可判定的。更高階匹配(只有包含存在性變量一個項的合一)是否是可判定仍無定論。
我們可以通過類型 $(o\to o)\to (o\to o)$ 的項(邱奇數)來編碼自然數。Schwichtenberg 在 1976 年證明在 $\lambda ^{\to }$ 中擴展的多項式被準確的表示為在邱奇數上的函數；這些粗略的是在條件運算下閉合的多項式。
$\lambda ^{\to }$ 的完整模型是通過解釋基本類型為集合和解釋函數類型為集合論的函數空間來給出。Friedman 在 1975 年證明這種解釋是對 $\beta \eta$ -等價是完備的，如果基本類型被解釋為無限集合。Statman 在 1983 年證明 $\beta \eta$ -等價是極大等價，它是典型歧義的，就是說，在類型替換下閉合(Statman's Typical Ambiguity Theorem)。它的必然推論是有限模型性質成立，就是說，有限集合就足夠用來區別出不能通過 $\beta \eta$ -等價識別的項。
Plotkin 在 1973 年介入邏輯關係來特徵化可以用 lambda 項定義的模型的基礎。在 1993 年 Jung 和 Tiuryn 證明了邏輯關係的一般形式(帶有可變元數的 Kripke 邏輯關係)完全特徵化了 lambda 定義能力。Plotkin 和 Statman 推測從有限模型生成給定元素是否是通過 lambda 項可定義的(Plotkin-Statman-conjecture)。這個推測被 Loader 在 1993 年證明為假。

引用

A. Church: A Formulation of the Simple Theory of Types, JSL 5, 1940
W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967
G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973
G.P. Huet: The Undecidability of Unification in Third Order Logic Information and Control 22(3): 257-267 (1973)
H. Friedman: Equality between functionals. LogicColl. 73, pages 22-37, LNM 453, 1975.
H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114.
R. Statman: The Typed lambda-Calculus Is not Elementary Recursive FOCS 1977: 90-94
W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230.
R. Statman. $\lambda$ -definable functionals and $\beta \eta$ conversion. Arch. Math. Logik, 23:21--26, 1983.
J. Lambek: Cartesian Closed Categories and Typed Lambda-calculi. Combinators and Functional Programming Languages 1985: 136-175
U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus LICS 1991: 203-211
Jung, A.,Tiuryn, J.:A New Characterization of Lambda Definability, TLCA 1993
R. Loader: The Undecidability of λ-definability, appeared in the Church Festschrift, 2001

參見

構造演算