我的最爱Lambda演算——开篇

（在这个帖子的原始版本里，我试图用一个JavaScript工具来生成MathML。但不太顺利：有几个浏览器没法正确的渲染，在RSS feed里也显示的不好。所以我只好从头开始，用简单的文本格式重新写一遍。）

计算机科学，尤其是编程语言，经常倾向于使用一种特定的演算：Lambda演算（Lambda Calculus）。这种演算也广泛地被逻辑学家用于学习计算和离散数学的结构的本质。Lambda演算伟大的的原因有很多，其中包括：

• 非常简单。
• 图灵完备。
• 容易读写。
• 语义足够强大，可以从它开始做（任意）推理。
• 它有一个很好的实体模型。
• 容易创建变种，以便我们探索各种构建计算或语义方式的属性。

Lambda演算易于读写，这一点很重要。它导致人们开发了很多极为优秀的编程语言，他们在不同程度上都基于Lambda演算：LISP，ML和Haskell语言都极度依赖于Lambda演算。

Lambda演算建立在函数的概念的基础上。纯粹的Lambda演算中，一切都是函数，连值的概念都没有。但是，我们可以用函数构建任何我们需要的东西。还记得在这个博客的初期，我谈了一些关于如何建立数学的方法么？ 我们可以从无到有地用Lambda演算建立数学的整个结构。

闲话少说，让我们深入的看一看LC（Lambda Calculus）。对于一个演算，需要定义两个东西：语法，它描述了如何在演算中写出合法的表达式；一组规则，让你符号化地操纵表达式。

Lambda演算的语法

Lambda演算只有三类表达式：

1. 函数定义：Lambda演算中的函数是一个表达式，写成：lambda x . body，表示“一个参数参数为x的函数，它的返回值为body的计算结果。” 这时我们说：Lambda表达式绑定了参数x。
2. 标识符引用（Identifier reference）：标识符引用就是一个名字，这个名字用于匹配函数表达式中的某个参数名。
3. 函数应用（Function application）：函数应用写成把函数值放到它的参数前面的形式，如(lambda x . plus x x) y。

柯里化

在Lambda演算中有一个技巧：如果你看一下上面的定义，你会发现一个函数（Lambda表达式）只接受一个参数。这似乎是一个很大的局限 —— 你怎么能在只有一个参数的情况下实现加法？

这一点问题都没有，因为函数就是值。你可以写只有一个参数的函数，而这个函数返回一个带一个参数的函数，这样就可以实现写两个参数的函数了——本质上两者是一样的。这就是所谓的柯里化（Currying），以伟大的逻辑学家Haskell Curry命名。

例如我们想写一个函数来实现x + y。我们比较习惯写成类似：lambda x y . plus x y之类的东西。而采用单个参数函数的写法是：我们写一个只有一个参数的函数，让它返回另一个只有一个参数的函数。于是x + y就变成一个单参数x的函数，它返回另一个函数，这个函数将x加到它自己的参数上：

lambda x. ( lambda y. plus x y )

现在我们知道，添加多个参数的函数并没有真正添加任何东西，只不过简化了语法，所以下面继续介绍的时候，我会在方便的时候用到多参数函数。

自由标识符 vs. 绑定标识符

有一个重要的语法问题我还没有提到：闭包（closure）或者叫完全绑定（complete binding）。在对一个Lambda演算表达式进行求值的时候，不能引用任何未绑定的标识符。如果一个标识符是一个闭合Lambda表达式的参数，我们则称这个标识符是（被）绑定的；如果一个标识符在任何封闭上下文中都没有绑定，那么它被称为自由变量。

• lambda x . plus x y：在这个表达式中，y和plus是自由的，因为他们不是任何闭合的Lambda表达式的参数；而x是绑定的，因为它是函数定义的闭合表达式plus x y的参数。
• lambda x y . y x ：在这个表达式中x和y都是被绑定的，因为它们都是函数定义中的参数。
• lambda y . (lambda x . plus x y)：在内层演算lambda x . plus x y中，y和plus是自由的，x是绑定的。在完整表达中，x和y是绑定的：x受内层绑定，而y由剩下的演算绑定。plus仍然是自由的。

我们会经常使用free(x)来表示在表达式x中自由的标识符。

一个Lambda演算表达式只有在其所有变量都是绑定的时候才完全合法。但是，当我们脱开上下文，关注于一个复杂表达式的子表达式时，自由变量是允许存在的——这时候搞清楚子表达式中的哪些变量是自由的就显得非常重要了。

Lambda演算运算法则

Lambda演算只有两条真正的法则：称为Alpha和Beta。Alpha也被称为「转换」，Beta也被称为「规约」。

Alpha转换

Alpha是一个重命名操作; 基本上就是说，变量的名称是不重要的：给定Lambda演算中的任意表达式，我们可以修改函数参数的名称，只要我们同时修改函数体内所有对它的自由引用。

所以 —— 例如，如果有这样一个表达式：

lambda x . if (= x 0) then 1 else x ^ 2 

我们可以用Alpha转换，将x变成y（写作alpha[x / y]），于是我们有：

lambda y . if (= y 0) then 1 else y ^ 2 

这样丝毫不会改变表达式的含义。但是，正如我们将在后面看到的，这一点很重要，因为它使得我们可以实现比如递归之类的事情。

Beta规约

Beta规约才是精彩的地方：这条规则使得Lambda演算能够执行任何可以由机器来完成的计算。

Beta基本上是说，如果你有一个函数应用，你可以对这个函数体中和对应函数标识符相关的部分做替换，替换方法是把标识符用参数值替换。这听起来很费解，但是它用起来却很容易。

假设我们有一个函数应用表达式：“ (lambda x . x + 1) 3 “。所谓Beta规约就是，我们可以通过替换函数体（即“x + 1”）来实现函数应用，用数值“3”取代引用的参数“x”。于是Beta规约的结果就是“3 + 1”。

一个稍微复杂的例子：(lambda y . (lambda x . x + y)) q。 这是一个挺有意思的表达式，因为应用这个Lambda表达式的结果是另一个Lambda表达式：也就是说，它是一个创建函数的函数。这时候的Beta规约，需要用标识符“q”替换所有的引用参数“y”。所以，其结果是“ lambda x . x + q “。

再给一个让你更不爽的例子：“ (lambda x y. x y) (lambda z . z * z) 3 “。这是一个有两个参数的函数，它(的功能是)把第一个参数应用到第二个参数上。当我们运算时，我们替换第一个函数体中的参数“x”为“lambda z . z * z “；然后我们用“3”替换参数“y”，得到：“ (lambda z . z * z) 3 “。 再执行Beta规约，有“3 * 3”。

Beta规则的形式化写法为：

lambda x . B e = B[x := e] if free(e) subset free(B[x := e]) 

最后的条件“if free(e) subset free(B[x := e])”说明了为什么我们需要Alpha转换：我们只有在不引起绑定标识符和自由标识符之间的任何冲突的情况下，才可以做Beta规约：如果标识符“z”在“e”中是自由的，那么我们就需要确保，Beta规约不会导致“z”变成绑定的。如果在“B”中绑定的变量和“e”中的自由变量产生命名冲突，我们就需要用Alpha转换来更改标识符名称，使之不同。

例子更能明确这一点：假设我们有一个函数表达式，“ lambda z . (lambda x . x + z) “，现在，假设我们要应用它：

(lambda z . (lambda x . x + z)) (x + 2) 

参数“(x + 2)”中，x是自由的。现在，假设我们不遵守规则直接做Beta规约。我们会得到：

lambda x . x + x + 2 

原先在“x + 2”中自由的的变量现在被绑定了。再假设我们应用该函数：

(lambda x . x + x + 2) 3 

通过Beta规约，我们会得到“3 + 3 + 2”。

如果我们按照应有的方式先采用Alpha转换，又该如何？

• 由 alpha[x/y] 有: (lambda z . (lambda y . y + z)) (x + 2)
• 由Beta规约： (lambda y . y + x + 2) 3
• 再由Beta规约： 3 + x + 2 。

“3 + x + 2”和“3 + 3 + 2”是非常不同的结果！

规则差不多就是这些。还有另外一个规则，你可以选择性地加一条被称为Eta-规约的规则，不过我们将跳过它。 我在这里描述了一个图灵完备 —— 完整有效的计算系统。 要让它变得有用，或看它如何用来做些有实际意义的事情，我们还需要定义一堆能让我们做数学计算的基本函数，条件测试，递归等，我将在下一篇文章讨论这些。

我们也还没有定义Lambda-演算的模型呢。（原作者在这里和这里讨论了模型的概念。）模型实际上是非常重要的！逻辑学家们在摆弄了LC好几年之后，才为其想出一个完整的模型，这是件非常重要的事情，因为虽然LC看起来是正确的，但在早期为它定义一个模型的尝试，却是失败的。毕竟，请记住，如果没有一个有效的模型，这意味着该系统的结果是毫无意义的！

http://cgnail.github.io/academic/lambda-1/