Lambda演算介绍

前言

本片文章旨在帮助有兴趣了解Lambda演算，但是没有相关数学基础的读者快速理解Lambda演算的基本思想。为了能够更好的满足这种需求，本篇文章将是非严谨的、启发式的。请那些希望学习严谨Lambda演算的读者阅读相关论文与书籍。

这是什么？

Lambda演算（Lambda Calculus）是数学家阿隆佐·邱奇（Alonzo Church）在20世纪30年代提出的一种形式系统，该系统是数学家阿隆佐·邱奇进行数学基础研究时提出的数学工具。该系统在后来被证明是一种具有与图灵机相同的计算能力的计算模型——即作为一种计算模型，Lambda演算是图灵完备的。Lambda演算通过简洁的几条规则，清晰的表述了函数的定义、函数的应用、变量等基本思想，对计算机科学领域的发展产生了重要影响。现在人们所熟知的各种函数式编程语言（例如Haskell、ML等）都是以Lambda演算作为理论基础的，并且许多非函数式编程语言也积极汲取了Lambda演算的思想，各类语言中的匿名函数便是典型的代表。

符号替换游戏？

要理解Lambda演算究竟在做什么，不妨设想这样一个符号替换游戏。

小菜一碟

声明：下面的符号序列中@是可替换的

!@#$%

替换：使用&进行替换，得到：

!&#$%

这也可以套娃？

声明：下面的符号序列中@是可替换的

声明：下面的符号序列中%是可替换的

!@#$%

第一次替换：使用&进行替换，得到：

声明：下面的符号序列中%是可替换的

!&#$%

第二次替换：使用?进行替换，得到：

!&#$?

简化

试着简化一下上面的繁琐描述：

声明：下面的符号序列中c是可替换的

abcdf

被简化为

λc.abcdf

---

声明与替换两个步骤合在一起如何简化?

声明：下面的符号序列中c是可替换的

abcdf

替换：使用K进行替换，得到：

abKdf

被简化为

(λc.abcdf)K = abKdf

---

相信你已经能够理解下面的表达代表了什么：

(λc.(λf.abcdf))KL = (λf.abKdf)L = abKdL

重要概念

基础概念

上文用了很大的篇幅介绍了一个符号替换游戏，目的在于帮助读者理解Lambda演算中几个重要概念：

概念	举例	解释
变量	a	字符是一个变量，该变量通常并不代表什么，仅仅是一个名字或占位符罢了
抽象化（函数定义）	λc.abcdf	这意味着abcdf中的c是可以被替换的，c被成为绑定变量
函数应用	(λc.abcdf)K	这意味着使用字符K替换前面函数定义中的字符c，可以得到结果abKdf
函数应用	ab	这表明a可以代表一个函数，若提前规定a是λc.ccc，那么可以得到ab=(λc.ccc)b=bbb

通常情况下，Lambda演算中任何变量都没有特定的含义，这些变量仅仅是一个名字，或者是某一个占位符，并在函数应用时被替换。

例如(λa.aab)，“λ”后面的a代表一个名字，标明a是可以被替换的，而“.”后面的a和b都代表占位符，并可能在函数应用的时候被替换。这里的a由于在“λ”后面，被成为绑定变量，而b被成为自由变量。

若进行函数应用，例如(λa.(aa)b)(λa.a)，可以得到((λa.a)(λa.a))b（将(λa.a)作为一个整体替换前面的aa）。

可以发现结果((λa.a)(λa.a))b依然存在函数应用，比如(λa.a)(λa.a)部分，计算这部分可以得到结果(λa.a)，综合起来结果就是(λa.a)b。

最后计算(λa.a)b得到结果b。

为了简化书写，我们通常规定函数应用是左结合的，例如abcdf的含义实际上为(((ab)c)d)f。因此，上面的例子(λa.(aa)b)(λa.a)可以书写为(λa.aab)(λa.a)。

柯里化

柯里化是一个非常重要的概念，还记得上面所提到的“套娃”吗？以λa.(λb.aab)举例，由于柯里化思想，我们可以将上面的表达式简写为λab.aab。简单来说就是将多层单参数函数的嵌套简写为一层多参数函数。

使用JavaScript中的匿名函数举例可能会更容易理解：

/**
 * 简写之前
 */
function (a) {
    return function (b) {
        return b(a(a)) // aab = (aa)b
    }
}
/**
 * 简写之后
 */
function (a, b) {
    return b(a(a))
}

可以看出柯里化是右结合的，需要注意的是柯里化仅仅是为了书写上的便利，并没有改变原表达式的语义。例如(λab.aab)KL=(λa.(λb.aab)KL)=(λb.KKb)L=KKL。

转换与规约

α转换

需要强调的是在Lambda演算中绑定变量的名称其实并不重要，我们应该着重关注结构本身，而不是一个绑定变量叫a还是叫b。例如下面两个表达式并没有本质上的不同：

λa.a

λb.b

这种仅仅改变绑定变量名称，而不改变表达式实际结构的变换被成为α转换。请注意，这种变换仅对绑定变量有效，无法对自由变量进行这样的操作，例如下面的两个表达式：

λa.ab

λa.ac

这两个表达式是不同的！因为变量b和变量c是自由变量，我们无法确定他们是否相同。

再看一个例子：

λb.(λa.ab)b

λc.(λa.ac)c

上面的两个表达式是相同的，因为他们的结构本质上是相同的，可以通过α变换将第一个表达式改写为第二个表达式。

可以发现，上一个例子中的表达式是本例中的一部分（子表达式）。这说明了两个表达式是否相同，在于我们研究这两个表达式时所关注的范围。如果仅仅关注本例中的两个子表达式λa.ab与λa.ac，那么他们是不同的。但是从整体来看，完整的表达式又是相同的。

β规约

回顾上文中介绍的“函数应用”，就像下面这样：

(λc.abcdf)K = abKdf

这种变换被成为β规约

考虑下面的表达式：

(λa.(λb.ab))b

它的结果应该是什么呢？从直觉来看，也许结果为λb.bb。

如果仅观察表达式的内部，即(λb.ab)，它的意思为ab中的第二个字母b是可以被替换的，但是并没有说第一个字母a是可以被替换的。

若我们认为上面的表达式结果是λb.bb，那么它意味着第一个与第二个字母都是可以被替换的。显然，内部表达式的含义被改变了。

实际上，造成这种异常的原因在于表达式内层的b与表达式外层的b是不一样的。直接进行替换会造成命名冲突！

那么应该怎么办呢？可以使用上文中介绍的α转换，改变内部子表达式中绑定变量b的名字即可：

(λa.(λb.ab))b
---α变换---> (λa.(λc.ac))b
---β规约---> λc.bc

计算的魅力

（未完待续）