初涉 λ 演算 (lambda calculus)

不幸上了一门干瘪枯燥的形式化方法课程，但课讲得不太好并不影响这些知识的趣味，毕竟还可以自己学嘛。课程内容更偏向软件形式化验证，不过会补充 λ 演算的内容，并且用到的证明器 Coq 也比较像是一种函数式语言。而相比于形式化验证，我对 λ 演算和函数式编程的兴趣更多一点。借着几篇博客和一些视频资料了解 λ 演算是什么之后，我也写下了几页的草稿和笔记。这里再整理一下自己的思路，从原始的 λ 演算系统开始构造一些简单的算数和逻辑表达。

这篇文章主要是笔记，用来整理我跟着^[3]学习 λ 演算时略有混乱的思路。推导这些东西未见得有什么实际作用，但是我觉得好玩，也就记下来了。也感谢^{[1] [2]} 两篇文章分享了推导思路的细节，这些细节着实解决了我的疑问。下面的内容有些长，主要原因是我写了不少自己的思考过程，以免日后想再看时发现无从翻找。

原始的 λ 演算规则

对一个编程多于推导的人来说，λ 演算看起来更像是一种“字符串代换规则”，只有两条：

• $\lambda x.E$ 定义一个函数：$x$ 表示一个绑定变量（函数参数）、$E$ 是表示函数内容的表达式。
• $E\;x$ 表示代入：将变量 $x$ 代入到变量 $E$ 中，或者说将 $E$ 作用于 $x$ 。

一个 λ 表达式就是一段包含上面两种情况的文本。对 λ 表达式而言，任何东西都是变量，函数也不例外。λ 演算的主要工作就是写一些表达式，然后进行“归约” (reduction)：

• α 等价 (α-equivalence)：函数的绑定变量可以随意改名，$\lambda x.f\;x$ 等价于 $\lambda y.f\;y$
• β 归约：执行代入，$(\lambda x.f\;x)\;y$ 等价于 $f\;y$
• η 归约：去掉多余的绑定变量。由于将任何表达式 $y$ 代入到 $\lambda x.f\;x$ 中都会得到 $f\;y$ ，写成 $\lambda x.f\;x$ 和只写 $f$ 实际上没有区别。

这样的表达式定义和归约规则看起来简直只剩抽象了，很难和计算联系到一起。但 λ 演算是和图灵机等价的计算模型，它也能构造一个通用计算机，解决图灵机能解决的所有问题，只是所有的“计算”都需要从表达式开始自己构造。

自然数和算数运算

对于计算机来说，一切计算从整数开始。从自然数开始更简单一些，但 λ 演算连数字也没有定义，所以想加减乘除，首先需要定义自然数。任何 λ 表达式都逃不出那两条原始规则，那么 λ 演算意义下的“自然数”也得是某种 λ 表达式。皮亚诺算数体系可以帮助我们定义一个满足算数公理的自然数集合，它有两条基本规则：

1. 0 是自然数。
2. 每个自然数有其后继，这个后继也是自然数。

照着这个规定，邱奇这样定义 λ 演算中的“自然数”：

1. 给定一个函数 $f$ ，0 就是这个函数不作用于 $x$ 的结果。

   $$0\triangleq\lambda f.\lambda x.x$$

2. 自然数 $k$ 是这个函数连续 $k$ 次作用于 $x$ 的结果，或者说 $k$ 的后继比 $k$ 多作用一次。写成 λ 表达式是

   $$k+1\triangleq\lambda f.\lambda x.f\;(k\;f\;x)$$

按照第二条规则构造的“自然数”就是邱奇数 Church Numerals ，

邱奇数	λ 表达式	代数记法
0	$\lambda f.\lambda x.x$	$x$
1	$\lambda f.\lambda x.f\;x$	$f(x)$
2	$\lambda f.\lambda x.f\;(f\;x)$	$f(f(x))$
3	$\lambda f.\lambda x.f\;\big(f\;(f\;x)\big)$	$f(f(f(x)))$

这样定义出来的“自然数”确实还是 λ 表达式，并且自身还是个函数。例如当我们归约到 $\lambda f.\lambda x.f\;x$ 时，就称之为得到了 1 ，而原始的 λ 演算中并没有“值”和“计算（过程）”这样的区分，所有的表达式都可以叫做变量 (variable)。

当表达式越来越长时，就容易产生演算顺序上的歧义。为方便起见，一般直接规定：函数定义尽可能向右延伸， $\lambda x.f\;x$ 表示 $\lambda x.(f\;x)$ ；而作用 (application) 则是左结合的，$f\;g\;x$ 表示 $(f\;g)\;x$ 。

有了邱奇数之后，下一步就是加减乘除了。根据代数知识，加法和乘法都对自然数集封闭，这个性质是比较好的；而且正整数加法和乘法都是越算越大，这意味着函数 $f$ 作用的次数只会增加不会减少，这意味着不用求逆。

加法和乘法

定义邱奇数的乘法最简单，因为在 $\lambda f.\lambda x.f\;x$ 这样的表达式中，$x$ 也可以是一个函数！这样我们就可以让 $b$ 作用于 $f$ 得到 $b\;f$ ，这是 $f$ 的连续 $b$ 次复合；再让 $a$ 作用于这个复合函数，得到的就是 $f$ 的连续 $a\times b$ 次复合：

$$\times\triangleq\lambda a.\lambda b.\lambda f.\lambda x.a\;(b\;f)\;x$$

加法要得到 $f$ 的 $a+b$ 次复合，我们可以分别得到 $f$ 的连续 $a$ 次和连续 $b$ 次复合，再将 $b$ 次复合的作用结果 $b\;f\;x$ 代入到 $a$ 次复合的函数中：

$$+\triangleq\lambda a.\lambda b.\lambda f.\lambda x.(a\;f)\;(b\;f\;x)$$

由于 λ 表达式允许函数作用于函数（因为函数也是变量），有时看起来不太直观。如果换成代数记法把函数参数写在括号里，乘法是 $a\big(b(f)\big)(x)$ ，加法是 $a(f)\big(b(f)(x)\big)$ 。

这样可以更明显地看出： $a$ 和 $b$ 在上述的运算过程中是函数到函数的映射，在分析学中称为算子。在 $f\;x$ 这个代入中，λ 演算在形式上允许 $f$ 和 $x$ 是任何东西，所以我们可以把它们都当作（分析学意义上的）函数，那么邱奇数就都是算子。

如果 $a$ 或 $b$ 为 0 ，只要注意任何函数 $f$ 代入 0 之后都不起作用，根据上面的定义就可以验证 $\times x\;0$ 是 $0$ 而 $+ x\;0$ 是 $x$ 。

前驱与减法

刚才说过，加法和乘法都不用求 $f$ 的逆，减法就要麻烦一些——因为我们希望知道 $k$ 的前驱是谁，而函数 $f$ 是一个任意的 λ 表达式，我们又没有定义代入的“逆运算”是什么。为此可以用一种笨办法求 $n$ 的前驱：

1. 最初，我们有一个二元组 $<0,0>$
2. 取第二个分量的后继，并用原先的第二个分量作为下次的第一个分量：$<a,b>\rarr<b,b+1>$
3. 把第二步视为一个函数，这个函数连续 $n$ 次作用于 $<0,0>$ 后正好得到 $<n-1,n>$

有了加法和乘法的经验，第三步不难和邱奇数联系起来。但这个笨办法还是不能马上实现，因为我们还没定义什么是二元组、如何取出二元组的分量。

和编程不同的是：函数是没有赋值操作的，并不能记录某种状态。但函数有参数，复合函数求值的过程中，外层函数可以用自己的参数构造内层函数的参数。相应地，我们在 λ 表达式中不是用变量去记录状态，而是用参数去传递状态，这样就能定义出二元组和取分量的函数。

$$\begin{aligned} \mathrm{pair}&\triangleq\lambda a.\lambda b.\lambda f.f\;a\;b \\ \mathrm{fi}&\triangleq\lambda p.\lambda a.\lambda b.a \\ \mathrm{se}&\triangleq\lambda p.\lambda a.\lambda b.b \end{aligned}$$

结合二元组、邱奇数，就可以实现前驱函数：

$$\mathrm{pred}\triangleq \lambda n.\mathrm{fi}\;\Big( n\; \textcolor{royalblue}{\lambda p.\mathrm{pair}\;(\mathrm{se}\;p)\;(+\;1\;(\mathrm{se}\;p))}\; (\mathrm{pair}\;0\;0) \Big)$$

这个式子有些长，其中蓝色的部分是 $<a,b>\rarr<b,b+1>$ 这一步，而 $\mathrm{pair}\;0\;0$ 则是初值 $<0,0>$ 。$n$ 作用于蓝色函数得到它的连续 $n$ 次复合，再作用于初值，最后用 $\mathrm{fi}$ 取第一个分量。

减法就是若干次前驱：

$$-\triangleq\lambda a.\lambda b.\lambda f.\lambda x.b\;\mathrm{pred}\;a\;f\;x$$

试着归约 $-\;1\;2$ 这样的表达式，会发现结果是 $0$ ——这意味着我们定义的减法结果不会是“负数”，$a<b$ 时最多得到 $0$ 。

遗留问题：除法

眼看快要完成，只剩除法没有定义了！减法依赖前驱，那除法依赖什么呢？学过计算机组成原理的同学可以回忆 ALU 中的除法器，最简单的思路是循环试减：用被除数不断循环减去除数，直至不能再减。循环的次数就是商、剩下的是余数。

问题来了：λ 演算还没有循环，这是个大麻烦。

• 直接实现循环需要记录状态，而 λ 演算做不到，我们得转换成函数复合的形式，但现在又没有办法将任意的循环转换成复合。
• 循环还需要判断何时退出，但现在也没有办法作条件判断。

接下来，我们去实现分支结构和“循环”结构。

Dijkstra 提出结构化程序设计时，他证明一种编程语言只需要顺序、分支、循环三种结构就是图灵完备的。

逻辑判断与分支

进行逻辑判断首先要有 true 和 false，在 λ 演算中可以人为规定一下：

$$\begin{aligned} \mathrm{true}&\triangleq\lambda a.\lambda b.a \\ \mathrm{false}&\triangleq\lambda a.\lambda b.b \end{aligned}$$

这里把 true 和 false 的定义交换一下其实也没什么影响，有意义的是它们的结构。将 true 视为含有两个绑定变量的函数，依次代入两个变量的结果是前一个，即 $\mathrm{true}\;x\;y$ 等价于 $x$ ，反之 $\mathrm{false}\;x\;y$ 等价于 $y$ ，这就对应“真”和“假”的两种结果，自然形成了条件分支。

在上述的定义下，假如一个 λ 表达式 $E$ 可以被归约为 true 或 false ，那 $E\;x\;y$ 中的 $x$ 可以视作条件成立的分支 (if case)、$y$ 可以视作条件不成立的分支 (else case) 。用分支的观点看待 true 和 false 有助于构造与、或、非这些逻辑运算，例如两个条件 $a$ 和 $b$ 作与运算时先考察 $a$ ，若 $a$ 为真则结果为 $b$ 、$a$ 为假时结果为 $a$ 。

$$\begin{aligned} \land&\triangleq\lambda a.\lambda b.a\;b\;a \\ \lor&\triangleq\lambda a.\lambda b.a\;a\;b \\ \lnot&\triangleq\lambda a.a\;\mathrm{false}\;\mathrm{true} \end{aligned}$$

先试试判零：无论代入什么到 $\lambda x.\mathrm{false}$ 这个函数中，得到的都是 false 。将 $\lambda x.\mathrm{false}$ 再代入到 $n$ 中，

• 如果 $n$ 不是零，那得到的函数还是 $\lambda x.\mathrm{false}$ ，最后作用于什么都会是 false
• 只有 $n$ 为零时这个函数不起作用，最后代入 true 就可以得到 true

$$\mathrm{zero}\triangleq\lambda n.n\;(\lambda x.\mathrm{false})\;\mathrm{true}$$

借助“减法不会得到负数”这一特点，还能构造出判断大小的函数：

$$\begin{aligned} \leq&\triangleq\lambda a.\lambda b.\mathrm{zero}\;(-\;a\;b) \\ \geq&\triangleq\lambda a.\lambda b.\mathrm{zero}\;(-\;b\;a) \\ =&\triangleq\lambda a.\lambda b.\land\;(\leq\;a\;b)\;(\geq\;a\;b)\\ \neq&\triangleq\lambda a.\lambda b.\lnot\;(=\;a\;b)\\ <&\triangleq\lambda a.\lambda b.\land\;(\leq\;a\;b)\;(\neq\;a\;b) \\ >&\triangleq\lambda a.\lambda b.\land\;(\geq\;a\;b)\;(\neq\;a\;b) \end{aligned}$$

有了运算、比较和分支，接下来就可以准备“循环”了。

“循环”？递归！

无论哪种编程语言，想要实现循环都需要用一个变量控制，而这对 λ 演算而言是不现实的。所以 λ 演算里不用循环，而是用递归。例如求 $1$ 到 $n$ 的和，可以表示为一个递归函数：

$$\mathrm{sum}(n)=\begin{cases} 0 &\text{if }n=0 \\ n+\mathrm{sum}(n-1) &\text{else} \end{cases}$$

这样的定义似乎很容易转写成 λ 表达式：

$$\mathrm{sum}\triangleq\lambda n.(\mathrm{zero}\;n)\;0\;\big(+\;n\;(\mathrm{sum}\;(\mathrm{pred}\;n))\big)$$

然而，λ 表达式中只存在两种东西：纯函数 (pure function) 和函数作用 (application)，而纯函数的定义中不能包含自身，这意味着上面这种递归定义不是一个正确的 λ 表达式。

换个角度理解，所有的 λ 表达式（函数）都是匿名函数，在定义中引用自己的名字实际上意味着在定义中引用自己的定义。过程式编程中的函数只是某段代码的别称，并不需要一个数学上的严格定义，也就不担心自引用会带来什么问题。然而 λ 演算的函数是严格定义的，并不能这样递归。

用纯函数实现递归

纯函数的定义不能引用自身，那就意味着我们需要想办法在不直接引用自身的情况下实现递归。假如有一个递归函数 $f_r$ ，它的定义中引用了自身，那么如果把 $f_r$ 作为一个绑定变量（参数）代入某个函数 $g$ ，让 $g$ 的代入结果是一个功能与 $f_r$ 一样的函数，不就能避开“直接引用”了吗？

例如用求和函数 $\mathrm{sum}$ 作为 $f_r$ ，下面这个 λ 表达式显然也表达了求和的含义，并且它是合法的：

$$g\triangleq\lambda f.\lambda n.(\mathrm{zero}\;n)\;0\;\big(+\;n\;(f\;(\mathrm{pred}\;n))\big)$$

$g$ 这个表达式中缺了一个参数 $f$ ，需要代入些什么才能继续归约。由于 $f_r$ 不是合法的 λ 表达式，我们不能直接把它代入 $g$ 中。但只要将某个功能与 $f_r$ 一样的函数代入 $g$ 中，就能得到一个定义合法的求和函数。姑且将这个函数称为 $f$ ，它

1. 首先功能与 $f_r$ 一样，所以是一个求和函数
2. 代入 $g$ 之后应该得到一个功能与 $f_r$ 一样的函数——这不是它自己吗？

第二个条件正是所谓不动点方程：

$$f=g(f)$$

函数 $f$ 就称为 $g$ 的不动点。如果而我们能求出这个不动点（函数），将其代入 $g$ ，问题立刻解决。把不动点方程的左边反复代入右边：

$$f=g(f)=g(g(f))=g\big(g(g\cdots)\big)$$

得到的 $g\big(g(g\cdots)\big)$ 是一个无限长的表达式，那它的“开方结果”应该也是个无限长的表达式：

$$f=g\big(g(g\cdots)\big)= \textcolor{royalblue}{G(G)=g\big(G(G)\big)}$$

蓝色的部分当然是个方程，但也可以理解为一个函数的定义：$G$ 是一个将任意函数 $G$ 映射为 $g\big(G(G)\big)$ 的函数，这里第一个 $G$ 是定义的函数名称，第二个 $G$ 则是任意的参数。

$$\begin{aligned} &G\triangleq\lambda G.g\;(G\;G) \\ \text{$\alpha$-equivlence}\implies &G\triangleq\lambda x.g\;(x\;x) \end{aligned}$$

把这个“开方”结果代回去，得到 $f$ 实际上是 $G$ 自己代入自己的结果：

$$f=G\;G=\big(\lambda x.g\;(x\;x)\big)\big(\lambda x.g\;(x\;x)\big)$$

试试归约 $f$ ：将 $\lambda x.g\;(x\;x)$ （第二个表达式）作为一个整体代入 $x$ （第一个表达式的绑定变量）中，得到的是 $g\;(G\;G)$ ——多套了一层 $g$ ，里面的结构还没变！这意味着 $f$ 能自己“复制”自己，生成任意长的表达式，正符合递归的要求。

设不动点方程的一般解是 $f=Y\;g$ ，这个解也可以理解为对 $Y$ 的定义：

$$\begin{aligned} &Y\triangleq\lambda g.\big(\lambda x.g\;(x\;x)\big)\big(\lambda x.g\;(x\;x)\big) \\ \text{inversed $\beta$-reduction}\implies&Y\triangleq\lambda f.(\lambda x.x\;x)\;\big(\lambda x.f\;(x\;x)\big) \end{aligned}$$

这个东西称为 Y 组合子 (Y combinator) ，只要将我们写好的纯函数 $g$ 代入 Y 组合子就能得到一个递归函数。回头再看 $g$ 的定义

$$g\triangleq\lambda f.\lambda n.(\mathrm{zero}\;n)\;0\;\big(+\;n\;(f\;(\mathrm{pred}\;n))\big)$$

其实就是计算求和结果的过程中与递归无关的部分（返回零、进行加法），而与递归有关的部分则属于 $f$ 。一个表示递归求和的合法 λ 表达式可以用 Y 组合子定义：

$$\mathrm{sum}\triangleq Y\;\bigg(\lambda f.\lambda n.(\mathrm{zero}\;n)\;0\;\big(+\;n\;(f\;(\mathrm{pred}\;n))\big)\bigg)$$

构造 Y 组合子为什么要“开方”呢？其实不需要特殊理由，纯粹是一种构造技巧，选“开立方”、“开任意次方”甚至“夹心饼干”都行 ——来自知乎网友 canonical 的推导 ^[1]，推荐去看一下

最后一环：除法

用递归实现循环试减，就能定义除法和模运算：

$$\begin{aligned} /&\triangleq Y\bigg( \lambda d.\lambda a.\lambda b.(<\;a\;b)\;0\; \textcolor{royalblue}{\big(+\;1\;(d\;(-\;a\;b)\;b)\big)} \bigg) \\ \mod&\triangleq Y\bigg( \lambda m.\lambda a.\lambda b.(<\;a\;b)\;a\; \textcolor{royalblue}{\big(m\;(-\;a\;b)\;b\big)} \bigg) \end{aligned}$$

蓝色部分表示当被除数剩余部分仍大于除数时，商加一、被除数继续减去除数，最终累加结果是商、剩下的是余数。至此，自然数、加减乘除、条件分支和递归都已经初步构造好了，λ 演算终于有了一些“计算”的样子。

参考资料

1. Y组合子的一个启发式推导 ↩
2. Y组合子（Y Combinator）| The Little Schemer 第九章 ↩
3. lambda演算科普 ↩