查看“︁简单类型λ演算”︁的源代码

{{noteTA|G1=IT}}
{{No footnotes|time=2015-12-16T20:57:29+00:00}}
'''简单类型 lambda 演算'''(<math>\lambda^\to</math>)是连接词只有 <math>\to</math> (函数类型)的[[有类型 lambda 演算]]。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。

简单类型也被用来称呼对简单类型 lambda 演算的扩展比如[[笛卡尔积|积]]、[[陪积]]或[[自然数]](系统 T)甚至完全的[[递归]](如[[PCF]])。相反的，介入了多态类型(如[[系统F]])或依赖类型(如[[逻辑框架]])的系统不被当作是简单类型。简单类型 lambda 演算最初由[[阿隆佐·邱奇]]在 1940 年介入来尝试避免[[无类型 lambda 演算]]的悖论性使用。

== 类型 ==

简单类型 lambda 演算的类型构造自基本类型(或类型变量) <math>\alpha,\beta,\gamma,\dots </math>，给定类型 <math>\sigma,\tau \,</math> 我们能构造 <math>\sigma \to\tau</math>。邱奇只使用了两个基本类型，<math>o \,</math> 是命题的类型，<math>\iota \,</math> 是个体的类型。这种演算经常只有一个基本类型，通常考虑为 <math>o \,</math>。

<math>\to</math> 是右结合的: 我们读 <math>\sigma\to\tau\to\rho</math> 为 <math>\sigma\to(\tau\to\rho)</math>。对每个类型 <math>\sigma \,</math> 我们指派一个数字 <math>o(\sigma) \,</math>，它是 <math>\sigma \,</math> 的阶。对于基本类型，我们设置 <math>o(\alpha)=0 \,</math>，而对于函数类型我们递归的定义 <math>o(\sigma\to\tau)=\mbox{max}(o(\sigma)+1,o(\tau))</math>。

== 项 ==

要定义有给定类型的 lambda 项的集合，我们介入定类型上下文 <math>\Gamma,\Delta,\dots</math>，它们是形如 <math>x:\sigma \,</math> 的类型假定的序列，这里的 <math>x \,</math> 是变量。我们介入判断 <math>\Gamma\vdash t : \sigma</math>，它意味着 <math>t \,</math> 在上下文 <math>\Gamma \,</math> 中是类型 <math>\sigma \,</math> 的项，它们由下列定类型规则给出:

:{| cellpadding="9"
| align="center" | <math>\frac{}{x:\sigma \vdash x : \sigma}</math>
| align="center" | <math>{\Gamma\vdash x:\sigma\quad x\not=y}\over{\Gamma,y:\tau \vdash x : \sigma}</math>
|-
| align="center" | <math>{\Gamma,x:\sigma\vdash t:\tau}\over{\Gamma\vdash \lambda x : \sigma.t : \sigma \to \tau}</math>
| align="center" | <math>{\Gamma\vdash t:\sigma\to\tau\quad\Gamma\vdash u:\sigma}\over{\Gamma\vdash t\,u : \tau}</math>
|}

换句话说，
# 如果 x 有类型 <math>\sigma \,</math>，我们知道 x 有类型 <math>\sigma \,</math>。
# 如果在特定上下文中，可以推导出 x 有类型 <math>\sigma \,</math> ，且有某个不是 x 的 y，则上述上下文与 y 有类型 <math>\tau \,</math> 的事实一起，同样允许推导出 x 有类型 <math>\sigma \,</math>。即向上下文增加一个新值不改变现存的值(新值不同于旧值之一)。
# 如果在特定上下文中，已知 x 有类型 <math>\sigma \,</math>，可以推导出 t 有类型 <math>\tau \,</math>，则在同一个上下文中，可以构造[[lambda 演算|lambda 抽象]] <math>\lambda x : \sigma.t \,</math>，它有类型 <math>\sigma \to \tau</math>。
# 如果在特定上下文中，可以推导出 t 有类型 <math>\sigma \to \tau</math> 和 u 有类型 <math>\sigma \,</math>，则在同一个上下文中，可以推导出表达式 <math>t\,u \,</math>有类型 <math>\tau \,</math>。这捕获了函数应用的概念。

闭合项的例子有:
*<math>\lambda x:\alpha.x : \alpha\to\alpha</math> ('''I''')
*<math>\lambda x:\alpha.\lambda y:\beta.x:\alpha \to \beta \to \alpha</math> ('''K''')
*<math>\lambda x:\alpha\to\beta\to\gamma.\lambda y:\alpha\to\beta.\lambda z:\alpha.x z (y z) : (\alpha\to\beta\to\gamma)\to(\alpha\to\beta)\to\alpha\to\gamma</math> ('''S''')。

它们是[[组合子逻辑]]的基本组合子的有类型 lambda 演算的表示。

简单类型 lambda 演算通过 [[Curry-Howard同构]]密切相关于只有蕴涵(<math>\to</math>)作为连接词的直觉逻辑(极小逻辑): 闭合项所居留的类型正好是极小逻辑的重言式。

相同类型的项通过 <math>\beta\eta \,</math>-等价来识别，它是通过方程 <math>(\lambda x:\sigma.t)\,u =_{\beta} t[x:=u] \,</math> 生成的，这里的 <math>t[x:=u] \,</math> 代表 <math>t \,</math> 带有 <math>x \,</math> 的所有自由出现都被替代为 <math>u \,</math>，而 <math>\lambda x:\sigma.t\,x =_\eta t  \,</math>，如果 <math>x \,</math> 在 <math>t \,</math> 中不自由出现。简单类型 lambda 演算(带有  <math>\beta\eta \,</math>-等价)是'''[[笛卡儿闭范畴]]'''(CCC)的内部语言。这是 [[Joachim Lambek|Lambek]] 首先观察到的。

== 重要成果 ==

* Tait 在 1967 年证明了 <math>\beta</math>-归约是[[lambda 演算|强规范化]]的。作为必然推论 <math>\beta\eta</math>-等价是[[可判定性]]的。Statman 在 1977 年证明规范化问题不是基本递归的。纯语义规范化证明由 Berger 和 Schwichtenberg (Normalisation by evaluation) 在 1991 年给出。
* <math>\beta\eta</math>-等价的[[合一]]问题是不可判定的。Huet 在 1973 年证明 3 阶合一已经是不可判定的了，而 Goldfarb 在 1981 年进而证明了 2 阶合一是不可判定的。更高阶匹配(只有包含存在性变量一个项的合一)是否是可判定仍无定论。
* 我们可以通过类型 <math>(o\to o)\to(o \to o)</math> 的项([[邱奇数]])来编码[[自然数]]。Schwichtenberg 在 1976 年证明在 <math>\lambda^\to</math> 中扩展的[[多项式]]被准确的表示为在邱奇数上的函数；这些粗略的是在条件运算下闭合的多项式。
* <math>\lambda^\to</math> 的完整模型是通过解释基本类型为[[集合 (数学)|集合]]和解释函数类型为集合论的[[函数空间]]来给出。Friedman 在 1975 年证明这种解释是对 <math>\beta\eta</math>-等价是[[完备性|完备的]]，如果基本类型被解释为无限集合。Statman 在 1983 年证明 <math>\beta\eta</math>-等价是极大等价，它是典型歧义的，就是说，在类型替换下闭合(Statman's Typical Ambiguity Theorem)。它的必然推论是有限模型性质成立，就是说，有限集合就足够用来区别出不能通过 <math>\beta\eta</math>-等价识别的项。
* 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. <math>\lambda</math>-definable functionals and <math>\beta\eta</math> 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: [https://web.archive.org/web/20060527202447/http://homepages.ihug.co.nz/~suckfish/papers/Church.pdf The Undecidability of &#955;-definability], appeared in the Church Festschrift, 2001

==参见==
* [[构造演算]]

[[Category:Lambda演算]]
[[Category:类型论]]