拉姆达演算

也称λ演算，数理逻辑中描述和研究函数及其组合的最一般性质的一个分支。在λ演算中，函数是作为规则来研究的，是一种老式的函数概念，注重从主目得出值的过程，强调它们的计算方面。这里函数概念是完全一般性的概念。例如，函数可以用日常语言定义，应用于用日常语言表达的主目。在这种情形下，研究的对象同时是函数又是主目。特别是一个函数可以应用于它自身，即以自己作主目。对于数学中的通常的函数概念，这是不可能的。λ演算由美国逻辑学家A．丘奇在20世纪30年代初创立，他的目的是建立函数的一般理论，然后引入逻辑概念扩展理论为逻辑和数学提供一个基础。在20世纪30年代关于可计算性理论研究中，λ演算占有突出位置，第一个不可计算性结果是丘奇证明的关于λ演算的项的问题的。S．C．克利尼从λ演算的不动点定理获得灵感而导致他的递归定理。递归函数与图灵可计算函数的等价性是以λ可定义函数为中介而证明的。克利尼和J．B．罗塞尔对λ演算研究和发展有重要贡献。D．斯科特在1969年构造了λ演算的第一个模型，开创了对λ演算的模型的研究。λ演算在计算机科学中有重要应用。

λ演算的初始符号包括：①变元：x，y，z，x，y，…；②=(相等)和→(归约)；③λ；④括号。(如果初始符号中还包括常元，称为应用的，不包括常元的系统称为纯λ演算。)

λ演算的项称为λ项，简称项。项归纳地定义如下：①所有的变元是项。②如M，N是项，则(MN)是项。③如果M是项，x是变元，则λx．M是项。④只有由①～③规则生成的是项。

M，N是元语言符号。用大写字母M，N，P，Q等表示任意的项。(MN)称为应用(application)，把M应用于N。应用是一个不用专门符号表示的初始运算。λx．M称为抽象，λ是抽象算子，其中的M称为λx的辖域。一个变元x的某个出现如果是位于某个λx辖域之中，称此出现为约束的，否则称为自由的。不含自由变元的项称为闭项。一项M中的自由变元的集合记作：FV(M)。三类项(变元、应用、抽象)没有共同的分子。在纯λ演算中，项是未解释的。直观地说，如果把M解释为一函数，(MN)就解释为把M应用于主目N的结果。项λx．M表示那个函数：它在主目N的值通过用N对M中的x作代入来计算。用元语言符号≡表示项的同一性，用M≡N表示M，N是同一个项。按照左结合省略括号。

对于任何项M，N和变元x，［N／x］M表示将x在M中的每一处自由出现都代入以N的结果。这种代入必须保证N中的自由变元在作代入之后仍保持自由。否则须先将M中的约束变元改名再作代入。例如，［y／x］(λy·xy)，代入的结果不应是λy·yy，而须先将λy·xy中约束变元y改名，取一个不在其中出现的变元z，将λy·xy改名为λz·xz，再作代入，其结果为λz·yz。

α规则(约束变元改名) λx·M≡λy·［y／x］M，yFV(M)

令项P包含λx·M的一次出现，yFV(M)。将λx·M换作λy·［y／x］M，称为P中的一次约束变元改名。我们说Pa－转换为Q，记作：P≡Q，当且仅当，Q是从P经有穷步(可以为0)约束变元改名而得。关系≡。是自反的、对称的和传递的。

具有形式(λx·M)N的项表示把函数λx·M应用于主目N。λx·M在N的值通过用N代入M中的x而计算。因此可以把(λx·M)N“简化为”［N／x］M。

β－归约 任何形式为(λx·M)N的项称为一β－redex，相应的项［N／x］M称为它的β－收缩。如果项P含有(λx·M)N的一个出现，并用［N／x］M代替该出现，结果为P′，就说Pβ－收缩为P′，记作：P→P。称Pβ－归约为Q，记作：P→Q，当且仅当Q从P经由β－收缩和约束变元改名的有穷(可以空)序列而得。

一不含有β-redex的项P称为一β－范式(简称范式)。如果项Pβ－归约为Q，而Q是范式，就称为Q为P的范式。(一个项可以有范式，也可以没有范式。例如，(a)zv是(λx·(λy·yx)z)v的范式。(b)L≡(λx·xxy)(λx·xxy)，L→Ly→Lyy→…，L没有范式。)直观上说，一个具范式的项不能再进一步计算。

归约是传递的但非对称的，但它产生下面的等价关系。

Pβ－等于Q或Pβ－可转换为Q，记作P=Q，当且仅当Q是从P经由β－收缩和逆β－收缩以及约束变元改名的有穷(可以空)序列而得。这也就是说，P=Q，当且仅当存在P，P，…，P(n≥0)使得P0≡P，Pn≡Q，并且对所有i≤n－1，或者P→P或P→P或P≡P。

λ演算的公式 如果M，N是项，则M=N，M→N是公式。

λ演算的公理和规则(为元语言符号，读作：如果…，则)：

1．λx·M=λy·［y／x］M，yFV(M) (α规则)

2．(λx·M)N=［N／x］M。 (β－转换)

3．M=M。

4．M=NN=M。

5．M=N，N=PM=P。

6．M=M′NM=NM′。

7．M=M′MN=M′N。

8．M=M′λx·M=λx·M′。

9．(λx·M)N→［N／x］M， (β－归约)

10．M→M。

11．M→N，N→PM→P。

12．M→NPM→PN。

13．M→NMP→NP。

14．M→Nλx·M→λx·N。

一个公式A在λ演算中可证明，记作λ┝A。(λ演算是一个不包含逻辑常项，不包含逻辑公理和规则的系统。在λ演算中的证明，只使用上列的公理和规则。λ演算实质上是以应用和抽象作初始运算和以β转换作公理的系统。)

关于β－可转换和β－归约有：如果P=Q，则λ┝P=Q；如果P→Q，则λ┝P→Q。一个项P有一范式，当且仅当存在一N，N是范式，λ┝P→N。

λ演算的一个重要结果是下面的定理：

丘奇－罗塞尔定理 (a)如果λ┝P→M，λ┝P→N，则存在某个Q，λ┝M→Q，并且λ┝N→Q。(b)如果λ┝M=N，则存在某个P，λ┝M→P并且λ┝N→P。

从丘奇－罗塞尔定理可得以下的推论：①如果M有一范式，则M有唯一的范式；②如果λ┝M=N并且N是范式，则M→N。③如果M，N是不同的范式，则根据①和②，λM=N。由此可以得出：λ演算是协调的，即不是所有的等式都是在系统中可证的。

令M是一项。如果M不是一范式，令M′是通过归约M中最左的redex而得，否则M′无定义。定义M=M，M=(Mn)′。序列M→M→…(有穷或无穷)称为M的最左或规范的归约链。

下面的定理是λ演算的另一重要结果：

标准化定理(寇里) M有一范式，当且仅当M的最左的归约链是有穷的。

对每一项F，都存在一项M，使得λ┝F(M)=M(不动点定理)。M称为F的不动点，即将F应用于M时，其值仍为M。(证明：定义W=λx·F(xx)和M=WW。则λ┝M=WW=(λx·F(xx))W=F(WW)=FM。)不仅如此，不动点还能用统一的方法找到，即存在不动点组合算子Y，对每一F，λ┝YF=F(YF)。不动点组合算子不是唯一的，下面是两个这样的Y。①Y=λf·(λx·f(xx))(λx·f(xx))，②Y=(λzx·x(zzx))(λzx·x(zzx))。寇里称Y为悖论的组合算子。因为在应用的λ演算系统中，如果不留心，由Y就可导致矛盾。Y可用于在λ演算中定义递归函数。

在λ演算中可以定义一些项表示自然数，并可在系统中定义数论函数。在λ演算中可定义的函数称为λ可定义函数(参见λ可定义函数)。克利尼证明，一函数f是λ可定义的当且仅当f是部分递归的。在把语法对象加以编码后就可以研究项的集合或等式集合的可判定性问题。丘奇证明：有(没有)范式的项的集合不是递归的。这是数理逻辑中第一个不可判定性结果。由这个结果，丘奇证明了一阶逻辑是不可判定的。斯科特在1963年证明了一个一般的定理。令∧°是闭λ项的集合。一集合A∧°是在相等性下封闭的，当且仅当M∈A并且λ┝M=NN∈A。A∧°是非不足道的当且仅当A≠Φ并且A≠∧°。斯科特证明：令A是在相等性下封闭的非不足道的集合。则A不是递归的。由斯科特定理可推出上面说的丘奇的不可判定性结果和关于λ理论的其它的不可判定结果。

λ演算可用下面的外延性规则加以扩张：

Mx=M′xM=M′，

若xFV(M)，FV(M′)。

这个规则可用增加下述规则公理化：

λx·Mx→M，xFV(M)，(η－归约)

增加η－归约规则的λ演算称为λη－演算。在λη演算中，具有形式(λx·Px)(xFV(P))的项也称为redex项。范式也不含这样的项，称为βη范式。下面的结果表明λη演算相对于有范式的项的完全性：如果M，N是不同的βη范式，则加上M=N作公理的λ演算是不协调的。

在λ演算和组合逻辑(与λ演算等价的一种逻辑系统)建立40年之后，斯科特在1969年构造了λ演算(也是组合逻辑)的第一个模型。为什么在经过这么长的时间之后才第一次建立λ演算的模型，原因之一是由于模型的复杂性。在λ演算中，对象既作为主目又作为应用于这些主目的函数。因此，人们看来希望对于λ演算的模型由一域D组成，使得它的函数空间D与D同构。根据(集合论中的)康托尔定理这是不可能的。斯科特通过把D限制为相对于D上的某个合宜的拓扑的连续函数集，解决了这个问题。现在人们考虑两类模型，λ代数和λ模型。

λ演算的语言是一种典范的程序语言。高级程序语言都有λ演算的特点：一个程序应用于该程序自身、以程序作为输出。λ演算语言是高级语言的关键部分。因此，λ演算在计算机科学中获得了应用。在计算机科学中应用方面的研究，是λ演算研究中的一个很活跃的方面。