简单类型λ演算

简单类型 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

参见

构造演算