2.3 λ演算

如果进行计算的是人类这样的智慧生命，也许不用深究递归的原理。我们只需要进行计算，发现递归时就在自己的思维中螺旋进入下一个层次。当递归终止时，就退回上一层。当人们思考如何用机器帮助我们进行计算时，这一问题才变得重要起来。20世纪30年代，当人们研究可计算问题时，分别独立提出了一些计算模型。最著名的包括图灵（见图2.13）提出的图灵机模型（1935年），丘奇（1932到1941年）和克莱尼（Stephen Kleene，1935年）提出的 λ 演算（希腊字母 λ 读作lambda），埃尔布朗（Jacques Herbrand）和哥德尔（Kurt Gödel）提出的递归函数（1934年）等。

图灵是英国数学家、逻辑学家，深刻地影响了计算机科学的理论发展，他提出的使用图灵机来形式化算法和计算的概念，是现代通用计算机的模型。图灵因此被称为计算机科学之父和人工智能之父 ^{[ 15 ]} 。第二次世界大战期间，图灵加入了盟军位于布莱切利公园的密码破译中心。他设计了很多方法用以快速破解纳粹德国的密码。图灵研制了一台绰号为“炸弹”（Bombe）的电子机器，使用战前波兰发现的方法，可以在1小时内找到德军恩尼格玛（Enigma）密码机的密钥。密码的成功破译是盟国获胜的一个关键因素，许多历史学家认为至少缩短了2年的战争，并且挽救了成千上万的生命。战争结束后，图灵开始从事“自动计算机”（ACE）的逻辑设计和具体研制工作。在图灵的设计思想指导下，1950年制出了ACE样机，1958年制成大型ACE机。人们认为，通用计算机的概念就是图灵提出来的。1950年，图灵开始考虑机器思维的问题并在论文《计算机与智能》中提出了著名的“图灵测试”。这一划时代的作品，使图灵赢得了“人工智能之父”的桂冠。1951年，由于在可计算数学方面所取得的成就，图灵成为英国皇家学会会员，时年39岁。为了纪念他对计算机科学的巨大贡献，美国计算机协会（ACM）于1966年设立一年一度的图灵奖，以表彰在计算机科学中做出突出贡献的人，图灵奖被喻为“计算机界的诺贝尔奖”。

对计算本身进行形式化，被称为“元数学”。这一试图重新为计算树立数学地位的尝试产生了一个杰作 ——λ 演算。 λ 演算名字的由来还有一则有趣的故事。在研究计算本身时，人们意识到应该区分函数和函数的值，例如我们说“如果 x 是奇数，那么 x × x 也是奇数”，这时我们指的是函数的值；而如果我们说“ x × x 是递增的”，那说的就是这个函数本身。为了区别这两个概念，我们会把函数写成 而不单是 x × x 。

“ ”符号是在1930年前后，由尼古拉·布尔巴基（Nicolas Bourbaki） 引入的。20世纪初，罗素和怀特海在《数学原理》中使用了 的表示法，1930年丘奇想使用类似的表示法，但是他的出版商不知道如何在 x 上面印出这个“帽子”符号，于是就改成在 x 的前面加上一个与之相似的大写希腊字母Λ，它后来又变成了小写字母 λ 。于是最终表达式就成了今天我们看到的 λx . x × x ^{[ 16 ]} 。虽然 的表示法已经广为接受，人们还是会在逻辑学和计算机科学中使用丘奇的表示法，而这种语言的名字“ λ 演算”也正源于此。

2.3.1 表达式化简

我们先从一些简单的例子开始了解如何用 λ 演算形式化算法与计算过程。首先是加减乘除四则运算，我们把它们也看成某种函数。比如加法1+2，可以看作用一个名为“+”的函数，作用到1和2两个变量上。按照把函数名写在前面的习惯，这一表达式可以写成（+1 2）。针对表达式的求值，就可以看作一系列的化简过程，例如：

(+(×2 3)(×4 5))

→(+6 (×4 5))

→(+6 20)

→26

这里箭头符号→读作“化简为”。注意到函数 f 应用到变量 x 上，并没有写成 f ( x )而是写成了 f x 的形式。对于多元函数，如 f ( x , y )，我们不把它写成（ f ( x , y )），而是用更加简单一致的方法写成（( f x ) y ）。这样为了表达“三加四”这样的加法，需要写成（（+3）4）。表达式（+3）实际上表示了一个函数，它把任何传入的变量都加3。这样在整体上这个表达式的含义就是：把加法“+”函数先应用到变量3上，这样的结果是一个函数，然后再把这个函数应用到变量4上。这样本质上，我们认为所有的函数都只接受一个参数。这一方法最初是由肖芬格尔（Schönfinkel,1889—1942）在1924年提出，后来经哈斯克尔·柯里在1958年后才被广泛使用的。因此，它被称为函数的“柯里化”（Currying） ^{[ 17 ]} 。

严格按照柯里化的方式写出的表达式含有很多括弧，为了简化描述，我们在不引起歧义的情况下会省略一些括弧，例如将（( f ((+3)4））( g x )）简写为( f (+3 4)( g x )）。

在进行表达式化简时，需要能够理解一些基本含义并做出计算。对于四则运算，我们已经在第1章中利用皮亚诺公理定义了加法和乘法。我们也可以用类似的方式定义其逆运算减法和除法。对于参与运算以及表示结果的常数，我们也有基于零和后继的定义。在这些理论基础上，实现时通常将基本运算和数字内置实现（built-in）以提高性能。通常加以内置实现的还有与/或/非等逻辑运算、布尔常量真（true）和假（false）。条件表达式可以按照第1章描述的麦卡锡形式 实现，也可以定义为下面的if形式。

其中 e _t 和 e _f 都是表达式。第1章中通过cons定义的复合数据结构，也可以通过函数来抽取其中的各个部分：

2.3.2 λ抽象

我们前面简单介绍了 λ 符号的由来，所谓 λ 抽象，实际上是一种构建函数的方法。我们通过一个例子来了解 λ 抽象的各个组成部分。

( λx .+ x 1)

一个 λ 抽象包含四个组成部分，首先是 λ 符号，表示“接下来要定义一个函数”。紧随其后的是变量，在本例中就是 x ，被称为形参（formal parameter）。形参之后是一个点，剩余部分是函数体，它向右延伸到最长，在本例中是+ x 1。有时为了避免对函数体的右边界产生歧义，可以增加括号，对于本例，可以写成：（+ x 1）。为了记忆方便，我们可以将 λ 抽象的四个部分按照如下方法对应到自然语言上：

为了方便，在后继的推导中我们也会等价地使用 形式的记法。这里有一点需要澄清， λ 抽象并不等同于 λ 表达式。 λ 抽象只是 λ 表达式四种情况之一，其他三种情况为

2.3.3 λ变换规则

考虑下面的 λ 表达式，如果对它化简，我们需要知道“全局”变量 y 的值。与之相对，我们不需要事先知道变量 x 的值，因为它以形参出现在函数中。

( λx .+ x y ) 2

比较 x 和 y 的不同之处，我们称 x 是被 λx “绑定”的。当将这一 λ 抽象应用到参数2时，我们会用2替换掉所有的 x 。相反， y 没有被 λ 绑定，我们称变量 y 是自由的。总之，表达式的值是由未被绑定的自由变量的值决定的。一个变量要么是被绑定的，要么是自由的。下面是一个稍复杂点的例子：

λx .+(( λy .+ y z ) 3) x

我们可以把它写成箭头记法，这样可以看得更清楚：

这样就可以看出， x 与 y 是被绑定的，而 z 是自由变量。在更加复杂的表达式中，同一变量的名字，有时是被绑定的，有时又以自由变量的形式出现，例如：

+ x (( λx .+ x 1) 2)

写成箭头形式为

我们看到，第一次出现的 x 是个自由变量，而后面出现的 x 是被绑定的。在复杂的表达式中，这种同一名字代表不同的变量的情况会给表达式化简带来麻烦。为了解决名称冲突的问题，我们引入第一条 λ 变换规则 ——α -变换。其中 α 是希腊字母阿尔法。这一规则说，我们可以将 λ 表达式中的一个变量，重新命名为另一个变量。例如：

写成箭头形式为

我们说 λ 抽象是一种构建函数的方法，如何将构建好的函数应用到参数值上呢？这就需要引入第二条 λ 变换规则 —— β -变换。正向使用这条规则时，把 λ 抽象函数体中的所有形参的自由出现替换成形参的值。例如：

根据变换规则，把 λ 抽象 应用到自变量2上得2+1。即2+1是将函数体 x +1中出现的形参 x 替换为2的结果。用箭头将这一变换表示为

我们称这一特定箭头方向的变换为 β -归约( β -reduction) ^[7] 。而反向使用这条规则称为 β -抽象。下面再通过更多的例子了解一下 β -归约。首先是形参多次出现的例子：

然后是形参出现零次的情况：

这是一个典型的“常量映射”的例子。接下来是一个多重归约的例子：

可以看到，从外向内逐层归约是一个不断柯里化的过程。有时我们把多重归约简写如下：

( λx .( λy . E ))⇒( λx . λy . E )

其中 E 表示函数体。写成箭头形式为

使用 β -归约进行函数应用时，参数也可以是另一个函数，例如：

最后一个我们要介绍的变换是 η -变换。它的定义如下：

写成箭头形式为

其中 F 是函数，且 x 不是 F 中的自由变量。我们来看一个例子：

在这个例子中， η -变换两边的行为表现得完全一样。如果应用到一个参数上，效果都是把这个参数增加1。 η -变换之所以要求 x 不能是 F 的自由变量是为了避免错误地将( λx .+ x x )变换为（+ x ）。我们可以看到， x 是（+ x ）中的自由变量。同样，限定 F 必须为函数是为了避免错误地将1变换为( λx .1 x )。在上面的定义中，称从左向右的变换为 η -归约。

至此，我们介绍了 λ 表达式变换的三大规则，我们小结一下：

● α -变换用于改变形参的名字；

● β -归约用于实现函数应用；

● η -归约用于去除多余的 λ 抽象。

此外，我们称内置函数的化简，如加减乘除四则运算、逻辑上的与或非等为 δ -变换。在某些文献上，还会看到另外一种 λ 表达式变换的简记形式，我们这里简单介绍一下。对表达式( λx . E ) M ，进行 β -归约时，我们用 M 替换 E 中的 x ，将此结果记为 E [ M / x ]。这样三大变换就可以简写成如表2.4所示的形式。

由于这些转换规则都是双向的，在对一个 λ 表达式进行变换时，既可以从左向右进行归约，也可以反过来从右向左进行抽象。这样自然会产生两个问题。第一个问题是：化简过程最终会停止么？第二个问题是：不同的化简方式得到的结果是一致的吗？对于第一个问题，答案是不确定的，化简过程不能保证一定会终止 。下面就是一个“死循环”的例子：( D D )，其中 D 定义为 λx . x x ，写成箭头形式为 。如果我们试图化简，就会得到这样的结果：

更耐人寻味的是这个例子：( λx . 1)( D D )，如果先化简( λx . 1)，那么化简过程会终止，答案为1。反之如果先化简( D D )，则根据上面的结论，这一过程就会陷入“死循环”而无法终止。丘奇和他的学生罗瑟 ^[8] 在1936年证明了一对定理，完整地回答了第二个问题。

定理2.1 （丘奇-罗瑟定理一）：若 E ₁ ↔ E ₂ ，则存在 E ，使得 E ₁ → E 且 E ₂ → E 。

也就是说，如果化简过程是可终止的，则化简结果是一致的。不同的化简方法会化简到同一结果，如图2.14所示。在此基础上，丘奇和罗瑟又证明了第二定理。为此我们先要给出“范式”（normal form）的概念。所谓范式，又称 β 范式，是指不能再进行 β -归约的形式。简单来讲，就是表达式中能够应用的函数都已经应用了。更严格的范式是 β-η 范式，在这样的范式中，既不能进行 β -归约，也不能进行 η -归约。例如 x +1） y 不是范式，因为它可以进行 β -归约变成 y +1。下面是范式的递归定义：

定理2.2 （丘奇-罗瑟定理二）：若 E ₁ → E ₂ ，且 E ₂ 为范式，则存在从 E ₁ 化简到 E ₂ 的正规顺序。

注意，这一定理要求化简过程也必须是可终止的。所谓正规顺序（normal order）就是从左向右，从外向内的化简顺序。 X6oOwpRlHdjixgAQo6fgGS9eZ2Jn78ncgNvX3QKRrGHpRVKbS7hJU6RBO2Mmp+ZR