以函数为中心：lambda 演算和组合子逻辑

用 python 和 javascript 实现 lambda 演算器

2024-07-28 日 23:10 2024-08-01 四 16:37

修改历史

[2024-09-11 三 11:53] 修改了拓展话题里直觉逻辑等价、不可判定性的描述，稍微清晰一点

1. 一些历史背景

历史上， lambda 演算的发明是为了对计算进行形式化，那么这里自然会出现关于 “计算” 和 "形式化" 的一些大问题：

人类在几千年前就已经能够计算了，比如买东西找零钱的加减法，土地面积计算，算盘里的运算规则，欧几里得算法等等，都是一种计算，为什么要形式化？

简要回答是，因为弗雷格、罗素等人引领的逻辑主义哲学（或分析哲学）思潮，希望用逻辑来解释一切，而为了实现这个目的，其中最重要的任务是先用逻辑正确地描述出数学里基础概念，比如集合论、自然数。于是罗素、怀特海写了一本《数学原理》，构建了数理逻辑的基础，而希尔伯特看到这本书后，借用其中的形式化符号去做元数学（比如找出最精简的能够表达数论的完备且无矛盾的公理集合），至于数学之外的对象的逻辑解释，有维特根斯坦等人在探索。

因此 lambda 演算是希望在弗雷格、罗素等人的基础上，用一套符号语言去重新描述“计算”，它能够覆盖如何计算找零钱（减法），算盘计算规则（四则运算），欧几里得算法（除法和迭代）等等，也就是说，这套规则足够通用，能够表示历史上人类发明的一切计算方法。

但这引出了另外的问题：

弗雷格、罗素、怀特海、希尔伯特等人已经给数学建立了一阶逻辑，几乎能够描述大部分的数学了，而数学不就包括“计算”吗？为什么丘奇还要去思考对计算的形式化方法呢？

这是因为，数理逻辑是一种描述性语言，它主要用来描述数学对象的性质和结构或者事实和状态，比如命题 \( x^2=y \), 这里虽然表达了 y 可以通过 x 进行平方操作来，但没有说明给定 y 如何计算出 x 。一般编程里求根号需要引入牛顿法，数理逻辑很难描述出这种计算步骤，尤其涉及到循环迭代等计算方式（数学归纳法是对性质的递归性归纳，而不是对操作的递归性描述）。再比如，数理逻辑可以描述有无限多个素数这样的事实，或者 2 是一个素数这种性质，但它不方便描述如何计算某个范围内的所有素数的方法。为了能方便地表达“计算过程”而不是事实和状态，许多数学家开始设计另一套符号系统，比如 Alonzo Church 借用数理逻辑里的函数、自由变量、变量替换等概念，构造出 lambda 演算。而就像数学里把多项式函数、指数函数、对数函数作为基础函数，用组合方式构造出更复杂的函数一样， Moses Schönfinkel 和 Haskell Curry 等人则预定义一些操作符号的基础函数，比如 I,S,K 等，再用函数组合的方式以此构造出其他所有计算所需要组合子逻辑系统（Combinatory logic）”。

那么他们为什么要发明一种描述计算的符号系统？最直接目的是什么？

lambda 演算和组合子逻辑是作为一种更便于描述“操作”而非“陈述”的形式系统而被发明的语言，这是一种从以静态结构为中心到以动态过程为中心的转变。发明的直接目的是试图解决数学基础里的判定性问题，这是希尔伯特提出的一个问题，在罗素等人证明几乎所有的数学定理都可以用逻辑语言描述出来后，数学命题已经变成了纯粹的逻辑符号串了，而希尔伯特认为，存在一种算法，给定任何数学命题字符串，这个算法能够返回一个结果，判断这个命题是否能从公理推导出来。但问题就在于，逻辑语言本身虽然能表达数学对象（比如数学命题），但却不方面表达数学的证明过程和“计算”过程，所以他们才继续发明另外一套语言，来表达这种极为通用的算法，这种算法要能判断所有数学命题，因此描述算法的语言就要极为“抽象”，这也是为什么 lambda 演算和组合子逻辑的基本要素如此精简，因为需要还原地足够彻底才能获得足够的通用性。

尽管这种通用的自动判断任何数学问题的算法被证明是不存在的（Church 用 lambda 演算率先证明了这一点，然后图灵用图灵机也证明了，本文最后会有证明思路的描述），但这个探索过程中留下的工具和思想的影响是深远的，比如函数式编程、类型论、范畴论、直觉主义数学、哲学里本体论和认识论关系等等。

因此，无论是 lambda 演算还是组合子逻辑，都是想要创造一种能够记录“如何操作符号”的符号系统。

lambda 演算中的 lambda 实际是把计算过程封装的记号（可以视为一种封印符号），比如 lambda x,y:x*y 把计算两个数的乘法的过程封装了起来，只对外提供接口，当需要执行这个计算的时候，可以通过“应用”规则（解除封印）去真正实施计算 – 也就是符号的匹配和替换。

本文更多以一种 python/js 编程的角度来梳理 lambda 演算和组合子逻辑的基本概念

2. 彻底的还原：只允许单变量函数

一个 lambda 表达式可以看作是一个计算过程的结晶体，就像是琥珀对昆虫捕食动作的静态化封装一样，以下把 x*y 封装了起来：

lambda x,y: x*y

但为了遵循逻辑主义的彻底性（也为了书写时符号的简洁和统一性），加减乘除这些操作还会被继续还原到无意义符号移动或替换层面，直到仅仅包括 x,y,z 等作为占位符的变量，以及单变量抽象和应用两个操作。

具体来说，“单变量抽象”指的就是，给定一个过程，比如用 x 指代，只可以把它封装（抽象）成以下形式：

lambda x: x

或者

lambda y: x

这里 y 可以替换成任何其他占位符变量，当前想要突出的特点在于，当 x 被装到 lambda _: x 形式的盒子里后， x 所代表的函数或者编程语句不会被执行。

以下被认为是不合法的，因为第一个函数有两个参数，第二个没有参数。

lambda x,y: x
lambda : x

这种约定是出于形式统一性，追求理论上的简约。其他领域也有大量类似的尝试，比如逻辑运算中，用 NAND 实现 and/or/not 等所有逻辑联结词；欧几里得精挑细选 5 条公理可以推导所有平面几何定律等等。

为了表示两个参数的函数，可以用嵌套形式：

select_first = lambda x: lambda y: x

“应用”就是编程语言中函数的执行：

select_first(1)(2)

这等价于：

def select_first2(x, y):
    return x
select_first2(1, 2)

但相比于 select_first2，select_first 还可以进入 parital apply 状态，返回一个函数

select_first(1)

<function __main__.<lambda>.<locals>.<lambda>(y)>

这是 lambda 演算采用单变量函数后引出的一个非常灵活的性质，以至于 python 中提供了预定义的 partial 函数来使得多元函数进入半求值状态：

from functools import partial
ps = partial(select_first2, 1)
print(ps)
ps(2)

functools.partial(<function select_first2 at 0x7ab4b014cb80>, 1)
1

现代编程语言中，除了有函数这种抽象手段，还有命名，数据结构，对象等等。在 lambda 演算里，要用函数抽象去模拟所有其他的抽象手段，以构建更复杂程序。

要注意的是，实际 lambda 演算中也有命名，比如 lambda x:x*2 里 x 就是变量名，当应用这个函数时，会自动把 x 形参和传入的实参对应起来，但这种命名与抽象强绑定了，这是导致实现匿名递归需要一些技巧的原因之一，这部分会在后文详细说明。

除了以上提到的抽象方法外，现代编程语言中还有 linguistic abstraction, 即构造新的特定作用的编程语言 (DSL), 把某些计算中需要的操作抽象到新的语法规则里去，而不是在现有语法规则下进行抽象，本文后半部分会实现解析特定语法和应用规则的 lambda 演算，就是一种语言学抽象，这种抽象可以允许自己引入新的语法、记号等。实际上 Church 就是不满于罗素和希尔伯特设计的一阶逻辑语言对“计算”的描述能力，从而引入 lambda 记号以及演算规则，构造了一门新的 DSL 。

为了方便展示，本文里允许给 lambda 函数命名，比如组合子逻辑中，I 组合子是一个输入任何对象返回对象本身的函数，它等于 lambda 演算中的 lambda x:x, 即：

I = lambda x:x

不过除了涉及递归的部分，任何 I 参与运算的代码，都可以把 I 替换成 lambda x:x, 从而去除掉这些额外的命名。

2.1. 组合子逻辑

组合子逻辑的思路是，不用去把函数的结构展现出来，而是人为选择出一些具有简单功能的“符号操作”作为基础函数，然后用这些函数的组合去表达更复杂的对象。这种思路和逻辑里选择一组公理作为起点，然后按有限规则进行推理是类似的。

比如上文刚提到的 lambda x:x 的功能描述是：输入任意对象，返回该对象本身。

给它取一个名字 “I 组合子”（Identity 的首字母）就够了，不需要像 lambda 演算那样，把它的形参和内容都暴露出来。因此组合子逻辑里的组合子可以认为是基于 lambda 演算的更高一层的实现（当然它也可以不是用 lambda 演算实现的，比如可以是 python 函数实现），就像某个函数库，只告诉你某些函数的用法，而不关心其实现。

除了 I 组合子外，还有一些基本“操作公理”：

K = lambda a: lambda b: a

K 组合子和上节定义的 select_first 函数是一样的，只不过历史上它被称为 K, 它可以看作是一个二元选择函数，从行为上看，只要 K 右侧有连续两个符号，比如 Kxy, 那么就会如消消乐一般得到第一个符号 x 。

选择是一种非常基础的操作，比如组合电路中，要设计复杂的逻辑电路，都需要一种能根据某个输入去选择不同其他输入的门电路，称为 Multiplexer （简称 MUX）, 再比如编程语言中，if else 是一种选择。

K(I)(x) == I

True

K 可以选择两个并列符号中的第一个符号，那么接下来可以考虑设计一个选择第二个符号的函数，但事实上，通过 K 和 I 的组合就能够得到这样的函数：

K(I)("first")("second")

second

可以看到 K(I) 得到的就是返回第二个元素的函数，即 lambda a:lambda b:b，这就是组合子的能力 – 对已有的“操作”进行组合从而得到新的“操作”：

KI = K(I)
KI

<function __main__.<lambda>.<locals>.<lambda>(b)>

继续从行为上去理解 KIxy 是如何运作的，前文说到 Kxy 会返回 K 左侧两个连续对象中第一个对象 x, 那么 KIxy 应该先执行 KIx 返回 I （这里默认约定了从左到右的 apply 顺序）, 然后执行 Iy 得到 y ，y 是因为应用 KIx 时抛弃了 x 但留下 I 之后才有机会继续和 I 结合从而最终“出头的”。

接着再定义一个和递归密切相关的基础组合子：

M = lambda f: f(f)

这个函数的意义并不像 K 或 KI 那样直观。M 接受一个函数，然后调用它，而调用的参数就是函数自身，比如输入 I 的话，会执行 I(I) 得到 I

M(I) == I

True

而如果执行 M(M) 会导致无限递归，这个问题我们在后文用这些组合子（或 lambda 演算）实现递归时再进行具体说明。

I 可以认为是单变量函数代表，K, M 和 KI 是双变量函数的代表（以嵌套 lambda 的形式），接着定义一个三变量函数：

C = lambda f:lambda a: lambda b: f(b)(a)

如果 C 右侧有三个符号，如 Cfab, 那么结果是 fba, 注意 a 和 b 的应用顺序被调换了。

由于 Kab 是选择第一个元素，那么 CKab 就是 K(b)(a) 也就是返回 b, 这么看 CK 的功能等价于 KI, 但它们实现很不一样：

CK = C(K)
print(CK("first")("second"))
print(KI("first")("second"))
print(CK == KI)

second
second
False

如果 C 只是用来构造 KI 的话，那么 C 看上去就是冗余的了，这和命题逻辑里有了 and, not 之后，其他逻辑连接词都是冗余是一样的（甚至只需要 NAND(与非门(NAND gate)) 就可以足够表示其他逻辑运算），不过 C 的额外能力是，它不单可以从 K 构造出 KI, 还可以把 KI 逆向得到 K 。

print(C(KI)("first")("second"))

first

C 是一种翻转二元运算的算子。

目前我们得到了 I, K, M, C 四条“操作公理”，这些名字是一种速记的符号，也是一种对 lambda 表达式的抽象（本节实际是用 python 函数实现了一个包含 I,K,M,C 四个函数的库）。

可以写更多的 lambda 演算并且给他们取名字，但后文会说明，只需要少量几个算子就可以构造任何其他功能的算子。

3. 函数作为编码

3.1. 编码逻辑对象

由于目前有的手段只是函数，那么如何用函数实现逻辑对象，比如逻辑常量 True 和 False ？

注意从逻辑系统角度来看，True 和 False 有两种意义。一种是语法（或符号层面），另一种是语义。语法层面，真和假一般会有对应的常量，比如 "T" 或者 "F", 而 T 和 F 的真假意义并不是在符号之中。对于命题 P->Q 的真假，是由外部（比如人）对符号的赋值（称为解释）所决定的，比如在 {P:True, Q:False} 赋值下，P->Q 是一个假命题，而在 {P:False, Q:True} 这套赋值下，P->Q 就是真命题，语义层面的真和假可以看成是对句子的一个第三方的标签，或者一种区分猫和狗二分类法。

组合子逻辑或者 lambda 演算需要把外部的真和假写入到符号语法本身中去，这个时候，真假不是额外的标签，而是一种操作规则（操作语义）。这时候要从行为的角度去看待 True 和 False, 比如在 python 中：

if True:
    first
else:
    second

True 则执行 first, False 则执行 second, True 和 False 是一种开关，一种对后续 first, second 参数进行选择的机制。

在 C 或者 js 中有 ?: 三元运算符号，就是用来进行二选一，选择依据就是 True 或者 False:

true?1:0

false?1:0

因此为了在 lambda 演算中表达真和假，我们需要让这个函数能够从两个输入里选择其一，约定 TRUE 表示选择第一个，FALSE 表示选择第二个：

TRUE = lambda x: lambda y: x
FALSE = lambda x: lambda y: y

print(TRUE(1)(2), FALSE(1)(2))

1 2

我们用以下方式来展现 TRUE 和 FALSE 的“意义”：

print(TRUE("true")("false"), FALSE("true")("false"))

true false

这里 TRUE 实际是 K 组合子的另一个名称， FALSE 是 KI 组合子。

接着考虑 not ，它要接受一个布尔值，同时又返回布尔值，而返回的布尔值是双参数形式，所以 not 应该要有三个参数：

NOT = lambda bool: lambda x: lambda y ....

定义好了接口，然后思考其内容：

当传入 TRUE: 返回 FALSE
当传入 FALSE: 返回 TRUE

而由于 TRUE 对应 K 组合子， FALSE 对应 KI 组合子，前文里 C 组合子就能够对 K 和 KI 进行转换，因此 C 组合子就可以充当 NOT

C = lambda f:lambda a: lambda b: f(b)(a)
NOT = C
print(NOT(TRUE)("true")("false"))
print(NOT(FALSE)("true")("false"))

0
1

接着实现 AND 和 OR, 还是得从 AND 和 OR 的行为上来分析：

a AND b 中：
- 如果 a 是 TRUE，那么返回 b: 但 TRUE(a)(b) 返回的是 a 而不是 b, 所以我们可以考虑用 TRUE(b)(a), 也就是 a(b)(a) 的方式来契合 a 为 True 的场景。
- 如果 a 是 FALSE 则返回 FALSE ：但 FALSE(a)(b) 返回 b, 因此还是用 FALSE(b)(a), 也就是 a(b)(a) 方式来选择，和上一条是一致的。
```
AND = lambda a:lambda b: a(b)(a)
print(AND(TRUE)(FALSE)("true")("false"))
print(AND(TRUE)(TRUE)("true")("false"))
print(AND(FALSE)(TRUE)("true")("false"))
print(AND(FALSE)(FALSE)("true")("false"))
```
```
false
true
false
false
```
a OR b 中：
- 如果 a 是 TRUE 则返回 a ： TRUE(a)(b) 返回的是 a, 也就是 a(a)(b) 的方式进行选择。
- 如果 a 是 FALSE 则返回 b ： FALSE(a)(b) 返回 b, 也就是 a(a)(b) 方式来选择，和上一条是一致的。
```
OR = lambda a:lambda b: a(a)(b)
print(OR(TRUE)(FALSE)("true")("false"))
print(OR(TRUE)(TRUE)("true")("false"))
print(OR(FALSE)(TRUE)("true")("false"))
print(OR(FALSE)(FALSE)("true")("false"))
```
```
true
true
true
false
```

可以根据 NOT,AND,OR 组合出更多逻辑运算，比如蕴含， a->b 中：

如果 a 是 True 则返回 b
如果 a 是 False 则返回 True

但 a->b 等价于 ((NOT a) or b)

所以：

IMPLY = lambda a:lambda b: OR(NOT(a))(b)
print(IMPLY(TRUE)(FALSE)("true")("false"))
print(IMPLY(TRUE)(TRUE)("true")("false"))
print(IMPLY(FALSE)(TRUE)("true")("false"))
print(IMPLY(FALSE)(FALSE)("true")("false"))

false
true
true
true

当然在大部分编程语言中是没有 IMPLY 这个逻辑运算的，并不常用。

不过异或这个操作在 python 是有的：

True ^ False
True ^ True

False

可以用组合子实现，A^B 等于 (NOT(A) and B) OR (A and NOT(B))

XOR = lambda a:lambda b: OR(AND(NOT(a))(b))(AND(a)(NOT(b)))
print(XOR(TRUE)(FALSE)("true")("false"))
print(XOR(TRUE)(TRUE)("true")("false"))
print(XOR(FALSE)(TRUE)("true")("false"))
print(XOR(FALSE)(FALSE)("true")("false"))

true
false
true
false

3.2. 编码序列

上节已经用函数实现了对真和假两种状态的编码，因此目前可以操作 1 个 bit 了，如果要操作一个 byte ，也就是 8 bit 呢？

这时候我们需要引入数据结构，1960 年代，John McCarthy 为了研究 AI, 发明了 Lisp 语言，原论文里只有 5 篇引文，其中之一是 lambda calculus 的论文，但实际上 McCarthy 仅仅是借用了 Church 发明的 lambda 符号，从而可以在他的 Lisp 编程语言里用以下形式定义函数：

(lambda (x) x*2)

Lisp 语言里把数据结构都规约到了 Pair 对象上，通过嵌套 Pair 可以构造出 list, tree 等其他所有数据结构。比如 python 中列表 [1,2,3,4], 在 lisp 里是一个嵌套二元组： [1,[2,[3,[4, null]]]]

我们可以借用这种思路来实现 lambda 演算里的数据结构。

要把 bit 变成 byte, 需要一个长度为 8 的 list, 在这之前先实现 pair 。

只有函数，如何表达 (a,b) 这种数对？我们要做的仍然是把注意力从 pair “是什么” 这个问题转移，关心与 pair 有关的核心的操作是什么即可。这是从描述性逻辑到构建主义逻辑的核心思想转变，是从逻辑到计算的转变，也是从本体论到认识论的一种转变（如果非得上升到哲学的话）。

对于 a,b 两个对象或符号，它应该有一种组成对的方法，在 Lisp 中称为 CONS, 然后要有获取第一个元素以及剩余的元素的操作， Lisp 中称为 CAR 和 CDR 。

为了方面阅读，我们给 CONS, CAR, CDR 另外的名字： MAKE_PAIR, FIRST 和 REMAIN

实际上 K 或者 KI 组合子（在逻辑上下文中是 TRUE 和 FALSE）已经对应了选择第一个元素和选择第二个元素，但它们没有存储能力，传入两个松散的数据，然后立即返回对应位置的数据：

print(K(1)(2), KI(1)(2))

1 2

前面说过，lambda 就是一种封印方法，或者一种凝固昆虫动作的琥珀，所以 lambda 本身就是很好的存储容器，传入 a,b 数据之后不要直接去操作 a 或 b, 而是返回一个封装了可以操作 a,b 的 lambda 对象，然后这个对象可以继续参与后续的 apply:

CONS = lambda a: lambda b: lambda s:s(a)(b)
MAKE_PAIR = lambda a: lambda b: lambda selector:selector(a)(b)

pair = CONS(2)(3)

执行完以上命令后， pair 实际是一个 lambda selector:selector(a)(b) 函数，这时候再用 K 和 KI 去选择：

CAR = lambda p:p(K)
CDR = lambda p:p(KI)
FIRST = lambda p:p(TRUE)
REMAIN = lambda p:p(FALSE)

print(CAR(pair), CDR(pair))
print(FIRST(pair), REMAIN(pair))

2 3
2 3

通过嵌套方式可以构成列表：

NULL = lambda x:x
int_list = CONS(0)(CONS(1)(CONS(2)(CONS(3)(NULL))))
print(FIRST(int_list), FIRST(REMAIN(int_list)), FIRST(REMAIN(REMAIN(int_list))))

0 1 2

3.3. 编码定长二进制整数

现在我们编码一个 4 bit 的 half byte （8 bit 会导致嵌套太多）：

HALF4 = CONS(FALSE)(CONS(TRUE)(CONS(FALSE)(CONS(FALSE)(NULL))))

如果 FALSE 用 0 表示， True 用 1 表示的话，可以编写一个解码函数来解析，该函数并不属于 lambda 演算，只是用来展示编码有效性：

def decode_byte(half):
    result = []
    for i in range(4):
        result.append(FIRST(half)("1")("0"))
        half = REMAIN(half)
    return "".join(result)
decode_byte(HALF4)

HALF5 = CONS(FALSE)(CONS(TRUE)(CONS(FALSE)(CONS(TRUE)(NULL))))
decode_byte(HALF5)

理论上可以实现 half byte 的加法，为此，先实现半加器：给定一个 bit 的 a 和 b, 输入半加器之后，应该返回一个 pair, 第一个元素是 a b 求和后的进位（AND 实现），第二个元素是 a 求和后的最低为数（XOR 实现）

HALF_ADD = lambda a:lambda b: CONS(AND(a)(b))(XOR(a)(b))

sc_01 = HALF_ADD(TRUE)(FALSE)
print(CAR(sc_01)(1)(0), CDR(sc_01)(1)(0))

0 1

但实际中可以直接用 XOR 和 AND 去求各个位的加法所需要的结果或进位，比如全加器结果和进位分别是：

FULL_ADD_s = lambda a:lambda b:lambda c: XOR(XOR(a)(b))(c)
FULL_ADD_c = lambda a:lambda b:lambda c: OR(OR(AND(a)(b))(AND(a)(c)))(AND(b)(c))

用半加器实现 4 bit 加法器，思路是：

最低位（第 4 位）： a,b 第四位做半加法的结果，这里实现一些封装辅助函数：

get4 = lambda x: CAR(CDR(CDR(CDR(x))))
s4 = lambda a:lambda b: XOR(get4(a))(get4(b))
c4 = lambda a:lambda b: AND(get4(a))(get4(b))
print(s4(HALF4)(HALF5)(1)(0), c4(HALF4)(HALF5)(1)(0))

1 0

第 3 位： a,b 第四位做半加法的进位再加上 a,b 第三位加法的结果

get3 = lambda x: CAR(CDR(CDR(x)))
s3 = lambda a:lambda b: FULL_ADD_s(get3(a))(get3(b))(c4(a)(b))
c3 = lambda a:lambda b: FULL_ADD_c(get3(a))(get3(b))(c4(a)(b))
print(s3(HALF4)(HALF5)(1)(0), c3(HALF4)(HALF5)(1)(0))

0 0

第 2 位： a,b 第四位做半加法的进位再加上 a,b 第三位加法的结果的进位再加上 a,b 第二位加法的结果

get2 = lambda x: CAR(CDR(x))
s2 = lambda a:lambda b: FULL_ADD_s(get2(a))(get2(b))(c3(a)(b))
c2 = lambda a:lambda b: FULL_ADD_c(get2(a))(get2(b))(c3(a)(b))
print(s2(HALF4)(HALF5)(1)(0), c2(HALF4)(HALF5)(1)(0))

0 1

第 1 位： a,b 第四位做半加法的进位再加上 a,b 第三位加法的结果再加上 a,b 第二位加法的进位加上第一位做加法的结果

get1 = lambda x: CAR(x)
s1 = lambda a:lambda b: FULL_ADD_s(get1(a))(get1(b))(c2(a)(b))
c1 = lambda a:lambda b: FULL_ADD_c(get1(a))(get1(b))(c2(a)(b))
print(s1(HALF4)(HALF5)(1)(0), c1(HALF4)(HALF5)(1)(0))

1 0

实现加法器：

FULL_ADD4 = lambda a: lambda b: CONS(s1(a)(b))(CONS(s2(a)(b))(CONS(s3(a)(b))(CONS(s4(a)(b))(NULL))))

decode_byte(FULL_ADD4(HALF4)(HALF5))

可以把以上所有函数名都展开成 lambda 形式，从而得到一个只有 lambda 的加法器，但这变得非常难以阅读。

3.4. 编码不定长自然数

上节实现的固定长度的自然数二进制编码（如果解释上是补码的话，就是整数表示）以及在其上的加法，本节则实现不定长度的自然数，理论上可以支持无限大小。

这种编码思路和之前的完全不同，它将函数中第一个参数作用在第二个参数上的次数来表示数字：

TWO = lambda f:lambda x:f(f(x))
THREE = lambda f:lambda x:f(f(f(x)))
FOUR = lambda f:lambda x:f(f(f(f(x))))
FIVE = lambda f:lambda x:f(f(f(f(f(x)))))

它们表达的是一种重复，比如重复加 1:

def inc(x):
    return x+1

print(TWO(inc)(0))
print(THREE(inc)(0))

2
3

我们将用 inc 函数来作为解码，把 lambda 表示的数解码成 python 中的 int, 便于检验程序正确性。

自然地，0 和 1 是分别应用 0 次和 1 次

ZERO = lambda f:lambda x:x
ONE = lambda f:lambda x:f(x)

ZERO 实际等于 KI 组合子，而这种自然数编码最初是 Church 设计，因此称为 Church 编码或 Church 自然数。

3.4.1. 指数

尝试将 THREE(TWO) 组合起来：

print(THREE(TWO)(inc)(0))

马上就得到了两个数之间的指数运算，因此这种组合子实际可以看作是一种 for 循环，比如循环计算 fibnacci 序列的值：

def fib(x):
    return x[1], x[0]+x[1]

print(TWO(THREE(fib))((0,1)))

(8, 13)

3.4.2. 加 1

接着定义“加一”操作，思路是：

该函数接受一个数（双 lambda 函数），返回一个数，因此这应该有三个参数的函数，其中第一层参数是 n, 表示 number, 先确定接口：
```
SUCC = lambda n:lambda g:lambda y: ...
```
任何一个数 n, 执行 n(g) 后相当于褪去一层 lambda, 并把需要应用多次的函数 g 代入到函数体内，比如 lambda f:lambda x:f(x) 执行 g 后是 lambda x:g(x), 再应用一次，即执行 n(g)(y) 才暴露出真正的函数体 g(y) ，这时候再给它加上一层 g, 即 g(n(g)(y)) 就是加上一层应用了，于是得到：
```
SUCC = lambda n:lambda g:lambda y:g(n(g)(y))
```

统一字符的话，得到：

SUCC = lambda n:lambda f:lambda x:f(n(f)(x))

print(SUCC(THREE)(inc)(0))

3.4.3. 加法

a+b 可以看作是一种递归：

def add(x,y):
    if x == 0:
        return y
    return add(x - 1,y+1)

add(10, 20)

每一步 a 减去 1, b 则加上 1, 但这需要有判断某个数是否是 0 的函数，同时还需要减 1 操作，更重要的是，我们还不知道如何实现递归。因此还是只能根据 add 的现象去反推出一种机制：

首先它应该接受 n1 n2 两个数，再返回一个数，因此它要有四个参数：
```
lambda n1: lambda n2: lambda f: lambda x: ...
```
通过执行 n1(f) 就会得到 lambda x:f(f(f(…))) 形式的结果，这里 f 有 n1 个。
同样 n2(f) 也会得到这种形式，这是时候只要把 n1(f)(x) 应用到 n2(f) 就可以了

于是得到：

ADD = lambda n1: lambda n2: lambda f: lambda x: n2(f)(n1(f)(x))

print(ADD(THREE)(TWO)(inc)(0))

print(ADD(THREE(THREE))(TWO(TWO))(inc)(0))

但还有另一种更精简的实现，其思路是：

我们不单可以执行 SUCC(THREE), 还可以执行 THREE(SUCC)
正如执行 THREE(inc) 后得到的是一个迭代加 1 函数，应用到 0 上会得到 3, 应用到 4 上得到 7, 这实际就是加法，只不过作用在 python 整数对象 0,1,2,3.. 上
那么执行 THREE(SUCC) 后，应用到其他 lambda 数字上，会得到什么呢？实际就是在这种数字编码上的加法

ADD = lambda n1: lambda n2: n1(SUCC)(n2)
print(ADD(THREE)(TWO)(inc)(0))

这是一种组合子的思路，把数字 n 和 SUCC 组合后就得到了“加 n” 操作。

由于对称性质，也可以是：

ADD = lambda n1: lambda n2: n2(SUCC)(n1)
print(ADD(THREE(TWO))(THREE)(inc)(0))

3.4.4. 乘法

类似加法的思路，乘法的一种思路是：

它应该接受 n1 n2 两个数，再返回一个数，因此它要有四个参数：
```
lambda n1: lambda n2: lambda f: lambda x: ...
```
通过执行 n2(f) 就会得到 lambda x:f(f(f(…))) 形式的结果，这里 f 有 n2 个。
我们希望把这里的 f 替换成 n1 个 f, 这样最后代入 x 就相当于有 n1*n2 个 f 了
n1(f) 可以得到 n1 个 f, 那么把 n1(f) 应用到 n2 上已更改就可以了：

MUL = lambda n1: lambda n2: lambda f: lambda x: n2(n1(f))(x)
print(MUL(THREE)(TWO)(inc)(0))
print(MUL(THREE(TWO))(TWO)(inc)(0))

6
16

注意这种写法和指数的区别，如果是直接应用 n1(n2), 得到的是 lambda x:n2(n2(n2(…)), 有 n1 重 n2 那么这时候再代入 x ，最内层的 n2(x) 会得到 f(f(f(…))) 有 n2 个 f, 然后应用 n2, 相当于对 f(f(f(…))) 再执行 n2 次，就是 n2 的平方次。

不过这实际等于：

MUL = lambda n1:lambda n2:lambda f: n2(n1(f))
print(MUL(THREE)(TWO)(inc)(0))
print(MUL(THREE(TWO))(TWO)(inc)(0))

6
16

这里只需要三层 lambda 。

由于对称性，以下也是可以的：

MUL = lambda n1:lambda n2:lambda f: n1(n2(f))
print(MUL(THREE(TWO))(TWO)(inc)(0))

不过根据组合的思路，还有另一种实现：

MUL = lambda n1:lambda n2: n2(n1(SUCC))(ZERO)
print(MUL(THREE(TWO))(TWO)(inc)(0))

这里 n1(SUCC) 表示 "+n1" 操作，那么 n2(n1(SUCC)) 就是重复 "+n1" 操作 n2 次，最后应用在 0 上就是 n1 乘以 n2 了

或者：

MUL = lambda n1:lambda n2: n2(ADD(n1))(ZERO)
print(MUL(THREE(TWO))(TWO)(inc)(0))

3.4.5. 指数

前文已经用 n2(n1) 的方式构建出指数了：

EXP = lambda n1:lambda n2: n2(n1)
EXP(TWO)(SUCC(THREE))(inc)(0)

但我们可以循着前文各个操作组合的思路继续构造另一种指数实现，即对 *n1 重复 n2 次，得到的就是 \( n_1^{n_2} \)

EXP = lambda n1:lambda n2: n2(MUL(n1))(ONE)
EXP(TWO)(SUCC(THREE))(inc)(0)

3.4.6. 幂塔：指数的重复

循着这种思路，很快就可以写出对指数重复 n 次的操作，比如 \( 3^{3^{3^{3}}} \) 是对 3 求 4 次指数迭代的结果，这个操作称为幂塔（tetration）

TER = lambda n1:lambda n2: n2(EXP(n1))(ONE)
TER(TWO)(THREE)(inc)(0)

基本只能计算到 \( 2^{2^{2}} \) ，再往上就会 stackoverflow 了

3.4.7. 自然数对和减 1

在数学中，定义完自然数后，如果继续定义减法，那么实际会出现未定义对象，比如 1-3 在自然数里是未定义的，为了解决这个问题，需要扩充数域引入整数对象，而整数对象实际和自然数对是等价的，比如 1-3 可以对应 (1, 3) 或者 (2, 4),(4,6) 等等。为了在 Chruch 编码中实现减 1，也需要引入数对。

而由于前文已经介绍了 CONS, 因此我们直接引入

T = lambda pair: CONS(CDR(pair))(SUCC(CDR(pair)))

以上组合子在做的事情请示等价于：

def move_and_add(pair):
    return [pair[1], pair[1] + 1]

用 Church 数去重复多次，重复的结果是，第一个元素就是第二个元素减去 1

print(THREE(THREE)(move_and_add)([0,0]))

[26, 27]

那么可以定义减 1 操作就是：

PRED = lambda n: CAR(n(T)(CONS(ZERO)(ZERO)))
PRED(THREE)(inc)(0)

如果对 ZERO 减去 1 仍然得到 0:

PRED = lambda n: CAR(n(T)(CONS(ZERO)(ZERO)))
PRED(ZERO)(inc)(0)

因为 ZERO(T) 返回 T, 对初始的 [0,0] 操作的结果结果是 [0, 1], 因此返回 0.

3.4.8. 减法

有了减 1 操作，那么重复 n 次就是减去 n 了

SUB = lambda n1: lambda n2: n2(PRED)(n1)
SUB(FIVE(TWO))(TWO)(inc)(0)

如果 n1 比 n2 大呢？

SUB = lambda n1: lambda n2: n2(PRED)(n1)
SUB(TWO)(FIVE)(inc)(0)

原因和 0 减去 1 为 0 是类似的。

4. 递归

上文提到过， Church 数本身就是一种 for 循环机制，比如重复在 3 上进行 4 次加 1:

FOUR(inc)(3)

但这种机制的问题在于，它完全是固定次数，没法在中间加入条件判断以便根据动态的环境跳出循环。因此需要引入递归，而递归的核心是 basecase 和朝着 basecase 变化的操作，比如前文提到过的以下 add 算法：

def add(x,y):
    if x == 0:
        return y
    return add(x - 1,y+1)

add(10, 20)

x==0 是 basecase, 而 add(x-1, y+1) 中，每次递归 add 的第一个参数 x 都朝着 0 方向变化。

减 1 加 1 前文而都实现过，这里关键是等于的实现

4.1. 判断整数是否为 0

在只有符号操作函数的世界里，要实现类似 x==0 的功能，实际我们是在处理 x,0 和 T, F 四个符号之间的选择关系。由于 0 的实现就是接受两个参数并返回第二个参数（KI 组合子）

ZERO = lambda f:lambda x: x

那么只要第二个参数赋予 TRUE, ZERO 就会选择 TRUE

ZERO("something")(TRUE) == TRUE

True

如果是其他自然数，那么第二个参数至少会应用到第一个参数 f 上一次。因此只要传入的 f 是一个能够把任何输入都变成 FALSE 的函数即可，因此判断是否为 0 的函数可以写成：

IS0 = lambda n:n(lambda x:FALSE)(TRUE)
print(IS0(ONE)("true")("false"))
print(IS0(PRED(ONE))("true")("false"))
print(IS0(SUB(FIVE)(FOUR))("true")("false"))
print(IS0(SUB(FIVE)(FIVE))("true")("false"))

false
true
false
true

4.2. 非匿名函数的递归

注意，本节的实现并非纯 lambda 演算，因为借用了 python 的变量定义，后文会介绍如何在无法进行变量定义的情况下实现递归

有了对 0 的判断，实际可以实现许多递归函数，比如重新实现 ADD:

ADD_rec = lambda n1: lambda n2: IS0(n1)(n2)(ADD_rec(PRED(n1))(SUCC(n2)))
ADD_rec(ONE)(TWO)(inc)(0)


RecursionErrorTraceback (most recent call last)
<ipython-input-367-d799676f5c3e> in <module>
      1 ADD_rec = lambda n1: lambda n2: IS0(n1)(n2)(ADD_rec(PRED(n1))(SUCC(n2)))
----> 2 ADD_rec(ONE)(TWO)(inc)(0)

<ipython-input-367-d799676f5c3e> in <lambda>(n2)
----> 1 ADD_rec = lambda n1: lambda n2: IS0(n1)(n2)(ADD_rec(PRED(n1))(SUCC(n2)))
      2 ADD_rec(ONE)(TWO)(inc)(0)

... last 1 frames repeated, from the frame below ...

<ipython-input-367-d799676f5c3e> in <lambda>(n2)
----> 1 ADD_rec = lambda n1: lambda n2: IS0(n1)(n2)(ADD_rec(PRED(n1))(SUCC(n2)))
      2 ADD_rec(ONE)(TWO)(inc)(0)

RecursionError: maximum recursion depth exceeded

但这里我们陷入了无限递归，这里的问题在于，我们实现的 IS0 在接受两个参数的时候，会同时执行两个分支，即便 IS0(b1)(b2) 中 b1 已经是 0, b2 仍然会执行。这就像我们用函数实现了 if 一样

def my_if(cond, branch1, branch2):
    if cond:
        return branch1
    else:
        return branch2

my_if(True, 1+1, 1/0)


ZeroDivisionErrorTraceback (most recent call last)
<ipython-input-368-e1d3676a32cc> in <module>
      5         return branch2
      6 
----> 7 my_if(True, 1+1, 1/0)

ZeroDivisionError: division by zero

这种情况下，所有函数参数都会运行。一种临时解决的方法是，把传入的参数全部用 lambda 封装凝固起来，然后在具体的分支里执行：

def my_if(cond, branch1, branch2):
    if cond:
        return branch1()
    else:
        return branch2()

my_if(True, lambda: 1+1, lambda: 1/0)

这是一种 call by need 的延迟执行的思想。

对于 lambda 演算中，我们需要修改 TRUE 和 FALSE 实现，改成一种 lazy evaluate 形式，也就是传入的结果需要手动执行一下才行：

LAZY_TRUE = lambda a:lambda b:a()
LAZY_FALSE = lambda a:lambda b:b()
IS0 = lambda n:n(lambda x:LAZY_FALSE)(LAZY_TRUE)
print(IS0(ONE)(lambda :"true")(lambda :"false"))
print(IS0(PRED(ONE))(lambda :"true")(lambda :"false"))
print(IS0(SUB(FIVE)(FOUR))(lambda :"true")(lambda :"false"))
print(IS0(SUB(FIVE)(FIVE))(lambda :"true")(lambda :"false"))

false
true
false
true

ADD_rec = lambda n1: lambda n2: IS0(n1)(lambda : n2)(lambda :ADD_rec(PRED(n1))(SUCC(n2)))
ADD_rec(ONE)(TWO)(inc)(0)

减法也可用类似方式实现：

SUB_rec = lambda n1: lambda n2: IS0(n2)(lambda : n1)(lambda :SUB_rec(PRED(n1))(PRED(n2)))
SUB_rec(FIVE)(ONE)(inc)(0)

同理，乘法，指数也可以用类似的方式实现，此处不再列出，而是实现前文没有实现过的整数除法以及求余

为此，我们要实现两个数比较大小，比如大于等于：

GEQ = lambda n1: lambda n2: IS0(SUB(n2)(n1))

以及小于：

LT = lambda n1: lambda n2: NOT(GEQ(n1)(n2))
print(LT(FIVE)(FOUR)(lambda :"T")(lambda :"F"))
print(LT(ZERO)(FOUR)(lambda :"T")(lambda :"F"))

F
T

余数定义为：

def mod(n1, n2):
    if n1 < n2:
        return n1
    return mod(n1-n2, n2)

mod(9,4)

MOD_rec = lambda n1: lambda n2: LT(n1)(n2)(lambda :n1)(lambda : MOD_rec(SUB(n1)(n2))(n2))
print(MOD_rec(ONE)(FOUR)(inc)(0))
print(MOD_rec(FOUR)(FOUR)(inc)(0))
print(MOD_rec(FIVE)(FOUR)(inc)(0))
print(MOD_rec(ADD(FIVE)(FIVE))(FOUR)(inc)(0))

除法定义为：

def div(n1, n2):
    if n1 < n2:
        return 0
    return 1+div(n1-n2, n2)

print(div(9,4), div(3,4), div(10, 2))

2 0 5

DIV_rec = lambda n1: lambda n2: LT(n1)(n2)(lambda : ZERO)(lambda :SUCC(DIV_rec(SUB(n1)(n2))(n2)))

print(DIV_rec(ONE)(FOUR)(inc)(0))
print(DIV_rec(FOUR)(FOUR)(inc)(0))
print(DIV_rec(FIVE)(FOUR)(inc)(0))
print(DIV_rec(ADD(FIVE)(FIVE))(FOUR)(inc)(0))

4.3. 匿名函数的递归

在另一篇文章从 x(x) 到 Y : 用 python 构建和理解 Y 算子（Y combinator）中，介绍了如何用 python 实现匿名递归函数，比如以下是 fibnacci

(lambda x:x(x))(lambda x: lambda n: n if n <= 2 else x(x)(n-1) + x(x)(n-2))(10)

同时也介绍了 Y 算子（组合子），但那并没有引入 lambda 演算，而只是一种试错的方式逐渐实现出匿名函数递归的。本节则是在组合子和 lambda 演算的框架下来梳理。

首先对于 fibnacci ，如果带函数命名，可以用如下实现

fib = lambda n: n if n <= 2 else fib(n-1) + fib(n-2)
fib(10)

追求精简的原始 lambda 演算中，不允许在函数定义中引用对自身的函数名。一种修改做法是，把函数用参数传进去

lambda f: lambda n: n if n <= 2 else f(n-1) + f(n-2)

这个时候实现中完全没有了 fib, 但问题是目前该函数是双参数的，第一个参数 f 要执行 f(n-1) 并返回整数，因此是单参数的，那么这时候传入的 f 是什么呢？

一种修改如下，然后把 fib 本身传进去：

fib = lambda f: lambda n: n if n <= 2 else f(f)(n-1) + f(f)(n-2)
fib(fib)(10)

这里 f(f) 中传入 f 是为了在递归中把 f 继续传递下去，因为 lambda f:lambda n 中第一个参数就是接受上一层环境传递给它的函数。

但我们还是在借用 fib 这个名称，不过由于定义中完全没有 fib, 于是只需要把以上代码里所有 fib 替换成 lambda 函数即可：

(lambda f: lambda n: n if n <= 2 else f(f)(n-1) + f(f)(n-2))(lambda f: lambda n: n if n <= 2 else f(f)(n-1) + f(f)(n-2))(10)

这实际等价于本节提到的第一个函数：

(lambda x:x(x))(lambda x: lambda n: n if n <= 2 else x(x)(n-1) + x(x)(n-2))(10)

只不过这里用 lambda x:x(x) 间接地复制了 fib 两次，它实际是前文提到过的 M 组合子：

M(lambda x: lambda n: n if n <= 2 else x(x)(n-1) + x(x)(n-2))(10)

从组合子的角度，还可以把这种匿名函数递归现象上升到函数的不动点理论，某个函数的不动点指的是，输入参数和函数结果返回一样的那个值，比如 sin(x) 中 0 就是不动点，因为 sin(0)=0

在组合子理论中，我们希望能有一个组合子，记为 Y, 它应用在以下形式的递归函数（第一个参数接受一个递归形式的函数）后，能够得到一个真正的可以执行的递归函数

lambda f: lambda n: n if n <= 2 else f(n-1) + f(n-2)

什么是“可以执行的递归函数”，实际就是第一个参数 f 那样的函数，因为 f 在以上函数体中要执行 f(n-1) 和 f(n-2) 它必然返回一个数字。假设记以上函数为 R 的话, 那么我们希望 Y(R)(10) 应该等于 f(10), 这里 f 是 R 函数第一个形参所期望的函数。也就是说形参 f 期望得到的是 Y(R), 如果把 Y(R) 作为参数传入 R, 结果是 R(Y(R)), 也就是：

lambda n: n if n <= 2 else Y(R)(n-1) + Y(R)(n-2)

从功能角度看， Y(R) 应该等于 R(Y(R)), 因为 Y(R)(n) 和 R(Y(R))(n) 结果应该对任何 n 都相等。

这意味着 Y(R) 是 R 的一个不动点，因此 Y 实际上是一个求解机器，比如要计算 sin(x)=x, 可以转换成解 sin(x)-x=0 方程，那么 Y 就类似这样一个程序，给定 sin(x)-x=0, 返回 x 的值。但对于程序来说，R(x)=x 没法转成求 R(x)-x=0 形式去求数值解。

对于 Y 的设计，也没法根据求根的思路，而是依赖自指，Curry 发现的 Y 算子如下：

\[ \lambda f.(\lambda x.f(x x)) (\lambda x. (f (x x))) \]

可以验证其满足 Y(R)=R(Y(R)) ：

Y(R)
(λf.(λx.f(xx))(λx.f(xx)))(R)
(λx.R(xx))(λx.R(xx)) ;; Y(R)
R((λx.R(xx)(λx.R(xx)))) ;; R(YR)
R(R(λx.R(xx)(λx.R(xx)))) ;; R(R(YR))
R(R(R(λx.R(xx)(λx.R(xx))))) ;; R(R(R(YR)))
...

核心在于其中 x(x) 操作，不过要注意的是这种 Y 实现会遇到前一节中递归里遇到的相同的问题 – stackoverflow，它只能在 lazy mode 下运行，而 python 并不是这种求值模式，而是 eager 求值模式，对于 python 版本还是参见：从 x(x) 到 Y : 用 python 构建和理解 Y 算子（Y combinator）

然后可以写出出 lambda 演算的递归：

Y = lambda f: (lambda x:f(lambda z:x(x)(z)))(lambda x:f(lambda z:x(x)(z)))

fact = Y(lambda f:lambda n:IS0(n)(lambda :ONE)(lambda: MUL(n)(f(PRED(n)))))

print(fact(ZERO)(inc)(0), fact(FIVE)(inc)(0))

1 120

fib = Y(lambda f:lambda n:IS0(n)(lambda :ONE)(lambda: ADD(f(PRED(PRED(n))))(f(PRED(n)))))

print(fib(ZERO)(inc)(0), fib(MUL(FIVE)(TWO))(inc)(0))

1 144

5. lambda 演算解释器

前文介绍递归相关的函数时，出现了许多 stackoverflow 的情况，那时把原因归为 lazy 和 eager 求值模式的区别，在 SICP 里，这被称为 noraml-order evaluation 和 appliative-order evaluation, 前者是先把函数参数代入函数体，然后求值，后者是先求出函数参数，再代入，用一个具体例子来说明：

(lambda x: x*x)(1+1)

对于 lazy 模式，计算过程是

(lambda x: x*x)(1+1)
(1+1)*(1+1)
2*2
4

对于 eager 模式是：

(lambda x: x*x)(1+1)
(lambda x: x*x)(2)
2*2
4

数学家们更多是在需要的时候去化简公式，而不是上来就直接化简，比如对于以下公式：

(lambda x: x+2321-1923)(1923-2321)

如果一上来就计算 1923-2321, 那计算出结果之后代入函数还要计算一遍 x+2321-1923, 但如果先观察式子，发现可以代入之后从表达式上进行化简，那么就不需要先对 1923-2321 求值，而是直接代进去，最后得到 0 。

lambda 演算只有 apply 一个操作，但也会面临类似的问题，比如以下表达式

(lambda x: x)((lambda y: y)(lambda z: z))

可以先执行 (lambda y: y)(lambda z: z) 得到：

(lambda x: x)((lambda z: z))

然后得到：

(lambda z: z)

也可先把 (lambda y: y)(lambda z: z) 整个替换 (lambda x: x) 中的 x 得到：

(lambda y: y)(lambda z: z)

执行后得到：

(lambda z: z)

大部分情况下，不同求值（或替换）顺序的结果是一样的，但如何涉及到无限递归，就会出现差别，比如：

(lambda x: x)((lambda y: y(y)(lambda z: z(z))

如果用 eager 方式直接对 ((lambda y: y(y)(lambda z: z(z)) 执行应用，会导致无限递归，根本执行不到 (lambda x: x)

但如果先代入，那么至少能够先执行到 (lambda x: x) 然后陷入递归。而如果把 (lambda x: x) 改成 (lambda x: 1), 完整表达式如下：

(lambda x: 1)((lambda y: y(y)(lambda z: z(z))

那么 eager 模式会陷入死循环，而 lazy 模式则直接返回 1, 根本不会执行到递归部分。

本节实现一个 lazy 模式的 lambda 演算解释器，其具体执行顺序如下：

如果这是一个 MN 形式的表达式， M 是一个 lambda 表达式，那么先用 N 去替换 M 的参数，然后再对替换完的结果递归进行求值（替换）
如果这是一个 lambda x: M 形式的表达式，那么执行后结果是 lambda x: N, 这里 N 是对 M 求值的结果。

此外，本解释器支持用 latex 形式的语法来写 lambda 表达式，比如 λxyz.zxy 对应的是

lambda x:lambda y:lambda z:(z(x))(y)

注意 zxy 的执行是先组合 z(x) 然后再组合 y, 而不是 z(x(y))

而如果要表示 z(x(y)), 则使用 λxyz.z(xy), 为了方便书写，也可用 L 替代 λ，比如 Lxy.xy

我们只允许单字符小写字母作为变量名，由于 lambda 演算中，只有 lambda(抽象) 和 apply （执行）两种操作，对应到语法上，就是两个核心对象：

class Apply:
    def __init__(self, first, second=None):
        self.first = first
        self.second = second  # None 表示这是个变量

    def py(self):
        first, second = self.first, self.second
        res = f"{first.py()}" if type(first) is not str else f"{first}"
        while second is not None:
            first = second.first
            if type(first) is str:
                res = (
                    f"({res})({first})" if len(res) > 1 else f"{res}({first})"
                )
            else:
                res = (
                    f"({res})({first.py()})"
                    if len(res) > 1
                    else f"{res}({first.py()})"
                )

            second = second.second
        return res

    def __str__(self) -> str:
        first, second = self.first, self.second
        res = f"({first})" if isinstance(first, Lambda) and second else f"{first}"
        while second is not None:
            first = second.first if hasattr(second, "first") else second
            res = f"{res}{first}" if type(first) is str else f"{res}({first})"
            second = second.second if hasattr(second, "second") else None
        return res


class Lambda:
    def __init__(self, arg, body):
        self.arg = arg
        self.body = body

    def py(self):
        return f"lambda {self.arg}: {self.body.py()}"

    def __str__(self):
        exp = self
        res = "λ"
        while isinstance(exp.body, Lambda):
            res += exp.arg
            exp = exp.body
        res += f"{exp.arg}.{exp.body}"
        return res

其中 py 和 str 函数都是用来打印的。

5.1. 语法解析器

根据文法规则编写一个 LL 风格的 Lambda parser

class LLLparser:
    def __init__(self, s):
        self.s = "".join(s.split())  # delete spacees
        self.i = 0

    def parse_apply(self):
        if self.i == len(self.s) or self.s[self.i] == ")":
            return None
        if self.s[self.i] == "(":
            self.i += 1
            first = self.parse()
            assert self.s[self.i] == ")", "parentheses not match"
            self.i += 1
        else:
            first = self.s[self.i]
            self.i += 1
        return Apply(first, self.parse_apply())

    def parse_lambda(self):
        if self.s[self.i] == ".":
            self.i += 1
            return self.parse()
        var = self.s[self.i]
        self.i += 1
        return Lambda(var, self.parse_lambda())

    def parse(self):
        if self.s[self.i] == "(" and self.s[self.i + 1] in "Lλ":
            self.i += 2
            lmb = self.parse_lambda()
            assert self.s[self.i] == ")", "parentheses not match"
            self.i += 1
            return Apply(lmb, self.parse_apply())

        if self.s[self.i] in "Lλ":
            self.i += 1
            return self.parse_lambda()
        return self.parse_apply()

这样我们可以直接把类似 latex 的公式转成 python 类型：

for exp in [
        "λx.f(x)",
        "λx.f(f(x))",
        "λf.λx.f(f(x))",
        "(λf.f(xx))(λf.f(xx))",
        "λxyz.xyz",
]:
    print(LLLparser(exp).parse().py())

lambda x: f(x)
lambda x: f(f(x))
lambda f: lambda x: f(f(x))
(lambda f: f(x(x)))(lambda f: f(x(x)))
lambda x: lambda y: lambda z: (x(y))(z)

注意观察最后一个式子的结合顺序，xyz 是从左到右结合，而不是从右到左。

可以用 python 的 eval 去运行这些返回的字符串，比如以此实现 Church 数的解码函数：

def num(lam: Lambda):
    def inc(x):
        return x + 1
    return eval(lam.py())(inc)(0)

print(num(LLLparser("λf.λx.f(f(f(f(f(x)))))").parse()))
print(num(LLLparser("λfx.f(f(f(f(x))))").parse()))

5
4

注意 Church 数里 f 和 x 是右结合的。

可以连同 TRUE 和 FALSE 一起解码，前者对应 1 后者对应 0:

def decode(lam: Lambda):
    def inc(x):
        return x + 1

    exp = eval(lam.py())
    try:
        return exp(1)(0)
    except:
        return exp(inc)(0)

print(decode(LLLparser("λfx.f(f(f(f(x))))").parse()))
print(decode(LLLparser("λfx.f").parse())) #TRUE /K
print(decode(LLLparser("λfx.x").parse())) #FALSE /KI

4
1
0

不过 eval 运行机制仍然是 eager 的，和前文代码结果是一样的，因此除了用来解码特定 lambda 函数，我们不用它去执行 apply ，而是实现对解析结果的 lazy 求值器。

5.2. beta 求值器

lambda 演算实际是一种字符串的替换系统（rewrite system），它的求值就是字符串地不断替换。

以下是一个单步的 beta_reduce 算法（每次遍历整个表达式解析树，找到可以应用的操作，执行一次递归应用）

def beta_reduce(exp, env={}):
    if isinstance(exp, Lambda):
        # REMOVE conflict
        env = {key: value for key, value in env.items() if exp.arg != key}
        return Lambda(exp.arg, beta_reduce(exp.body, env))
    if isinstance(exp, Apply):
        if isinstance(exp.first, Lambda):
            param = exp.first.arg
            if exp.second is None:
                return beta_reduce(exp.first, env)
            value, remain = exp.second, None
            if hasattr(exp.second, "second"):
                value, remain = exp.second.first, exp.second.second
            new_env = {**env, param: value}
            return Apply(
                beta_reduce(exp.first.body, new_env),
                beta_reduce(remain, new_env),
            )
        if type(exp.first) is str:
            return Apply(
                env.get(exp.first, exp.first), beta_reduce(exp.second, env)
            )
        return Apply(beta_reduce(exp.first, env), beta_reduce(exp.second, env))
    return exp

比如它可以：

print(beta_reduce(LLLparser("(λx.x)y").parse(), {}))

还可以：

print(beta_reduce(LLLparser("(λxyz.x(yz))(mn)").parse(), {}))

λyz.mn(yz)

如果执行多步骤，则可以逐步 reduce

exp = LLLparser("(λfab.fba)(λab.b)").parse()
for i in range(3):
    exp = beta_reduce(exp, {})
    print(exp)

λab.(λab.b)ba
λab.(λb.b)b
λab.b

还可以进行 Church 数的加一：

exp = LLLparser("(λngy.g(ngy))(λfx.f(f(f(f(f(x))))))").parse()
for i in range(3):
    exp = beta_reduce(exp, {})
    print(exp)
print(decode(exp))

λgy.g((λfx.f(f(f(f(f(x))))))gy)
λgy.g((λx.g(g(g(g(g(x))))))y)
λgy.g(g(g(g(g(g(y))))))
6

指数运算：

exp = LLLparser("(λfx.f(fx))(λgy.g(gy))").parse()
print(decode(exp))
for i in range(7):
    exp = beta_reduce(exp, {})
    print(exp)
print(exp.py())
print(decode(exp))

4
λx.(λgy.g(gy))((λgy.g(gy))x)
λx.λy.(λgy.g(gy))x((λgy.g(gy))xy)
λxy.λy.x(xy)(λy.x(xy)y)
λxy.(λy.x(xy))((λy.x(xy))y)
λxy.x(x((λy.x(xy))y))
λxy.x(x(x(xy)))
λxy.x(x(x(xy)))
lambda x: lambda y: x(x(x(x(y))))
4

exp = LLLparser("(λfx.f(f(fx)))(λgy.g(gy))").parse()
print(decode(exp))
for i in range(10):
    exp = beta_reduce(exp, {})
    print(f"--{i}", exp)
print(decode(exp))

8
--0 λx.(λgy.g(gy))((λgy.g(gy))((λgy.g(gy))x))
--1 λx.λy.(λgy.g(gy))((λgy.g(gy))x)((λgy.g(gy))((λgy.g(gy))x)y)
--2 λxy.λy.(λgy.g(gy))x((λgy.g(gy))xy)(λy.(λgy.g(gy))x((λgy.g(gy))xy)y)
--3 λxy.(λy.λy.x(xy)(λy.x(xy)y))((λy.λy.x(xy)(λy.x(xy)y))y)
--4 λxy.(λy.x(xy))((λy.x(xy))((λy.λy.x(xy)(λy.x(xy)y))y))
--5 λxy.x(x((λy.x(xy))((λy.λy.x(xy)(λy.x(xy)y))y)))
--6 λxy.x(x(x(x((λy.λy.x(xy)(λy.x(xy)y))y))))
--7 λxy.x(x(x(x((λy.x(xy))((λy.x(xy))y)))))
--8 λxy.x(x(x(x(x(x((λy.x(xy))y))))))
--9 λxy.x(x(x(x(x(x(x(xy)))))))
8

exp = LLLparser("(λfx.f(f(f(fx))))(λgy.g(g(gy)))").parse()
print(decode(exp))
for i in range(8):
    exp = beta_reduce(exp, {})
print(decode(exp))

81
81

一切看似没有问题，直到遇到以下例子：

exp = LLLparser("(λfx.fx)(λfx.f(fx))").parse()
print(decode(exp))
for i in range(2):
    exp = beta_reduce(exp, {})
    print(exp)
print(decode(exp))

2
λx.(λfx.f(fx))x
λx.λx.x(xx)


TypeErrorTraceback (most recent call last)
<ipython-input-669-f56e94a014a6> in decode(lam)
      6     try:
----> 7         return exp(1)(0)
      8     except:

<string> in <lambda>(x)

TypeError: 'int' object is not callable

During handling of the above exception, another exception occurred:

TypeErrorTraceback (most recent call last)
<ipython-input-692-ed12961e310d> in <module>
      4     exp = beta_reduce(exp, {})
      5     print(exp)
----> 6 print(decode(exp))

<ipython-input-669-f56e94a014a6> in decode(lam)
      7         return exp(1)(0)
      8     except:
----> 9         return exp(inc)(0)
     10 
     11 print(decode(LLLparser("λfx.f(f(f(f(x))))").parse()))

<string> in <lambda>(x)

TypeError: 'int' object is not callable

这里是 lambda 参数名作用域冲突导致的，真正执行时应该要用以下方式：

1. λx.(λfx.f(fx))x
2. λx'.(λx.x'(x'x)) ;; 替换 x 为 x', 
3. λy.(λx.y(yx))
3. λyx.y(yx)

因此还需要一个更精细的命名冲突处理的机制，要能够在 beta reduce 中自动执行 lambda 演算的 alpha-conversion 规则。这个问题在逻辑、编程语言（比如 lisp 论文里提到了 lambda 演算符号替换的命名冲突问题）中都反复出现。

5.3. alpha 替换

所谓 alpha 替换，就是说 lambda x:x 和 lambda y: y 是等价的，在 beta 求值过程中，比如上个例子中的 (λfx.f(fx))x, 最右侧的 x 去替换 f, 当它经过 λfx. 时遇到了另一个 x, 这个时候它知道，被替换的 lambda 表达式中有相同的 x 冲突，这时候，需要把 λx.f(fx)) 替换成 λy.f(fy)),

为了能够知道哪些变量要替换，替换成哪个新变量名，需要引入两个辅助函数（类）：

class VariableGenerator:
    def __init__(self, vars=set()):
        self.vars = vars
        from itertools import product, chain

        base = string.ascii_lowercase
        self.hub = chain(base, product(base, range(100)))

    def __call__(self):
        for ele in self.hub:
            if type(ele) is tuple:
                ele = ele[0] + str(ele[1])
            if ele not in self.vars:
                self.vars.add(ele)
                return ele
        raise ValueError("no more variable")


def get_variables(exp):
    if isinstance(exp, Apply):
        return get_variables(exp.first) | get_variables(exp.second)
    if isinstance(exp, Lambda):
        return {exp.arg} | get_variables(exp.body)
    if type(exp) is str:
        return {exp}
    return set()

VariableGenerator 没调用一次会产生一个不在 self.vars 中的新变量名，都是小写英文字母，当不够的时候则加上所数字，最多可以到 z99, 有 2600+26 个字母。之所以提供这么多字母，主要是 Y 算子的递归有产生大量新变量，除此之外，前文提到的大部分运算只需要 26 个小写字母就可以了。

get_variables 是返回表达式里所有变量名

接着实现 alpha 替换，递归地把给定字符 var 替换成 generator 里产生的的字符。

def alpha_conv(exp, var, generator):
    """
    replace all var in exp with a new variable generated by generator
    """
    if not isinstance(exp, Lambda) or var != exp.arg:
        return exp

    new_var = generator()

    def _alpha(exp):
        if isinstance(exp, Apply):
            return Apply(_alpha(exp.first), _alpha(exp.second))
        if isinstance(exp, Lambda):
            if exp.arg == var:
                return exp
            return Lambda(exp.arg, _alpha(exp.body))
        if exp == var:
            return new_var
        return exp

    return Lambda(new_var, _alpha(exp.body))

然后把 alpha 替换代码加入到 beta 规约中，主要是在表达式为 Lambda 时，除此之外修复了之前版本的一些问题：

def beta_reduce(exp, env={}, generator=None):
    if type(exp) is str:
        return env.get(exp, exp)

    if isinstance(exp, Lambda):
        if env:
            key = list(env.keys())[0]
            all_variables = get_variables(env[key])
            if exp.arg in all_variables and key in get_variables(exp.body):
                exp = alpha_conv(exp, exp.arg, generator)

            env = {} if key == exp.arg else env
        return Lambda(exp.arg, beta_reduce(exp.body, env, generator))

    if isinstance(exp, Apply):
        if env != {}:
            return Apply(
                beta_reduce(exp.first, env, generator),
                beta_reduce(exp.second, env, generator),
            )

        if isinstance(exp.first, Lambda):
            if exp.second is None:
                return exp.first
            lam = exp.first
            value, remain = exp.second, None
            if isinstance(exp.second, Apply):
                value, remain = exp.second.first, exp.second.second

            env = {lam.arg: value}  # only one
            return Apply(beta_reduce(lam.body, env, generator), remain)
        return reduce_list(exp, env, generator)
    return exp


def reduce_list(exp, env, generator):
    return (
        Apply(
            beta_reduce(exp.first, env, generator),
            reduce_list(exp.second, env, generator),
        )
        if hasattr(exp, "second")
        else beta_reduce(exp, env, generator)
    )

这样，之前的出错的例子就可以正确求值了：

exp = LLLparser("(λfx.fx)(λfx.f(fx))").parse()
generator = VariableGenerator(get_variables(exp))
for i in range(5):
    exp = beta_reduce(exp, {}, generator)
    print(f"--{i}", exp)
print(decode(exp))

--0 λa.(λfx.f(fx))a
--1 λa.(λfx.f(fx))a
--2 λa.λx.a(ax)
--3 λax.a(ax)
--4 λax.a(ax)
2

5.4. 预处理宏和 SK 组合子系统

在 C 语言中我们可以用预处理宏对源代码进行文本替换和处理。预处理宏通常以 # 开头，例如 #define、#include 等

比如以下用 #define 定义常量和代码片段

#define PI 3.14159
#define SQUARE(x) ((x) * (x))

#include <stdio.h>

int main() {
    printf("Square of %d: %d\n", PI, SQUARE(PI));
    return 0;
}

在 lambda 解释器中，我们也可以用这种方式来进行简单的命名，用 python 赋值形式 K=λ… 表示宏定义，之后直接用字符串替换的方式去预处理。

import re
def preprocess(exp, subst_map):

    subst_lst = list(subst_map.items())
    subst_lst.sort(key=lambda x: (len(x[0]), x[0]), reverse=True)
    for key, value in subst_lst:
        if not value.startswith("("):
            value = f"({value})"
        exp = re.sub(key, value, exp)
    return exp

succ_one = preprocess("SUCC(ONE)", {"SUCC": "λnfx.f(nfx)", "ONE": "λfx.fx"})
print(succ_one)

(λnfx.f(nfx))((λfx.fx))

封装求值执行过程，并通过检查 beta reduce 前后树是否相等来决定是否 reduce:

def tree_equal(ast1, ast2):
    if isinstance(ast1, Apply) and isinstance(ast2, Apply):
        return tree_equal(ast1.first, ast2.first) and tree_equal(
            ast1.second, ast2.second
        )
    if isinstance(ast1, Lambda) and isinstance(ast2, Lambda):
        return tree_equal(ast1.body, ast2.body)
    return ast1 == ast2

def evaluate(ast, max_step=2000):
    for _ in range(max_step):
        generator = VariableGenerator(get_variables(ast))
        ast_after = beta_reduce(ast, {}, generator)
        if tree_equal(ast, ast_after):
            return ast
        ast = ast_after

    return ast

print(evaluate(LLLparser(succ_one).parse()))

λab.a(ab)

将解析赋值语句、注释、表达式和求值、打印都封装在以下函数中：

def read_and_rewrite(string):
    expressions_str = string.split("\n")
    subst_map = {}
    for exp in expressions_str:
        if exp.strip() == "" or exp.startswith(";") or exp.startswith("#"):
            continue
        if "=" in exp:
            key, value = exp.split("=")

            parser = LLLparser(preprocess(value.strip(), subst_map))
            ast = parser.parse()

            subst_map[key.strip()] = str(
                evaluate(ast) if isinstance(ast, Apply) else ast
            )

            continue
        print(exp, end="-> ")
        exp_ = preprocess(exp.strip(), subst_map)
        ast = LLLparser(exp_).parse()
        step = 300

        if numerical(exp):
            if "Y(" in exp:
                step = 1000

            res = evaluate(ast, step)
            print(f"{decode(res)}: {res} ")
        else:
            res = evaluate(ast)
            print(res)

def numerical(exp):
    return any(
        x in exp
        for x in ["FACT", "PRED", "ADD", "MUL", "ACC", "EXP", "ISZERO"]
    )

最后的 numerical 函数用来检查当前语句执行后结果是否会是一个 Church 数以便打印数字（对于赋值语句不进行打印）：

codes = """
ONE = λfx.fx
TWO = λfx.f(fx)
THREE = λfx.f(f(fx))
FOUR = λfx.f(f(f(fx)))
FIVE = λfx.f(f(f(f(fx))))
SUCC = λnfx.f(nfx)
ADD = λmn.m(SUCC)(n)
ADD(ONE)(TWO)
ADD(TWO)(THREE)
ADD(FIVE)(FOUR)
"""

read_and_rewrite(codes)

ADD(ONE)(TWO)-> 3: λab.a(a(ab)) 
ADD(TWO)(THREE)-> 5: λab.a(a(a(a(ab)))) 
ADD(FIVE)(FOUR)-> 9: λab.a(a(a(a(a(a(a(a(ab))))))))

有了这些函数后，我们可以重新来看组合子，实际只需要 K 和 S 两个组合子就可以构造出所有通用计算需要的要素（逻辑判断, 数字，加减乘除，递归）。

注意以下 AND, NOT 都是后缀表达式（NOT 直接用 (FALSE)(TRUE) 表示没有赋值），而 OR 是中缀表达式（如果是前缀，会更复杂），这里给出一些容易实现的组合子的例子，更多参考 SKI combinator calculus - Wikipedia

codes = """
K = λxy.x
S = λxyz.xz(yz)
I = SKK
TRUE = K
FALSE = SK
OR = K
AND = FALSE
TRUE
FALSE
# FALSE(NOT):
FALSE(FALSE)(TRUE)
(TRUE)OR(FALSE)
(FALSE)OR(FALSE)
(TRUE)(TRUE)AND
(FALSE)(TRUE)AND
I
KI
SKIK
KS(I(SKSI))
SKI(KIS)
"""

read_and_rewrite(codes)

TRUE-> λxy.x
FALSE-> λaz.z
FALSE(FALSE)(TRUE)-> λxy.x
(TRUE)OR(FALSE)-> λxy.x
(FALSE)OR(FALSE)-> λaz.z
(TRUE)(TRUE)AND-> λxy.x
(FALSE)(TRUE)AND-> λaz.z
I-> λz.z
KI-> λyz.z
SKIK-> λxy.x
KS(I(SKSI))-> λxyz.xz(yz)
SKI(KIS)-> λz.z

有许多以鸟类命名的组合子（组合子逻辑发明人之一 Haskell Curry 和类型论创始人 Per Martin Lof 似乎都是资深鸟类观察爱好者），可以参考： Combinator Birds

5.5. 从 x 到 Y

最后我们把前文用 python 实现的几乎所有运算都用纯 lambda 演算执行：

ALL = """
x
λfx.f(fx)
(λfx.f(fx))(λfx.f(fx))
I = λx.x
K = λxy.x
KI = KI
C = λfxy.fyx
S = λxyz.xz(yz)
NOT = C
TRUE = K
FALSE = KI
AND = λab.aba
OR = λab.aab
CONS = λabs.sab
CAR = λp.pK
CDR = λp.pKI
XOR = λab.OR(AND(NOT(a))(b))(AND(a)(NOT(b)))
CK
CKI
SKK
NOT(TRUE)
NOT(FALSE)
AND(TRUE)(TRUE)
AND(TRUE)(FALSE)
AND(FALSE)(TRUE)
AND(FALSE)(FALSE)
OR(TRUE)(TRUE)
OR(TRUE)(FALSE)
OR(FALSE)(TRUE)
OR(FALSE)(FALSE)
CONS(TRUE)(FALSE)
CAR(CONS(TRUE)(FALSE))
CDR(CONS(TRUE)(FALSE))
XOR(TRUE)(TRUE)
XOR(TRUE)(FALSE)
XOR(FALSE)(TRUE)
XOR(FALSE)(FALSE)

ZERO = λfx.x
ONE = λfx.fx
TWO = λfx.f(fx)
THREE = λfx.f(f(fx))
FOUR = λfx.f(f(f(fx)))
FIVE = λfx.f(f(f(f(fx))))
SUCC = λnfx.f(nfx)
ADD = λmn.m(SUCC)(n)
ADD(ONE)(TWO)
ADD(TWO)(THREE)
ADD(FIVE)(FOUR)
MUL = λmn.m(ADD(n))(ZERO)
MUL(ZERO)(THREE)
MUL(TWO)(THREE)
MUL(THREE)(FOUR)
EXP = λmn.n(m)
EXP(TWO)(THREE)
EXP(THREE)(TWO)

ISZERO = λn.n(K(FALSE))(TRUE)
ISZERO(ZERO)
ISZERO(ONE)
ISZERO(TWO)
LEQ = λmn.ISZERO(SUB(n)(m))

T = λp.CONS(CDR(p))(SUCC(CDR(p)))
PRED = λn.CAR(n(T)(CONS(ZERO)(ZERO)))
PRED(ONE)
PRED(TWO)
PRED(THREE)
PRED(FOUR)
PRED(FIVE)
Y = λf.(λx.f(xx))(λx.f(xx))
ACC = λfn.ISZERO(n)(ZERO)(ADD(n)(f(PRED(n))))
ISZERO(ZERO)(ONE)(TWO)
ISZERO(ONE)(ONE)(TWO)
Y(ACC)(ZERO)
Y(ACC)(ONE)
Y(ACC)(TWO)
Y(ACC)(THREE)
Y(ACC)(FOUR)
FACT=λfn.ISZERO(n)(ONE)(MUL(n)(f(PRED(n))))
Y(FACT)(ZERO)
Y(FACT)(ONE)
Y(FACT)(TWO)
Y(FACT)(THREE)
"""

read_and_rewrite(ALL)

x-> x
λfx.f(fx)-> λfx.f(fx)
(λfx.f(fx))(λfx.f(fx))-> λab.a(a(a(ab)))
CK-> λab.b
CKI-> λab.a
SKK-> λz.z
NOT(TRUE)-> λab.b
NOT(FALSE)-> λab.a
AND(TRUE)(TRUE)-> λxy.x
AND(TRUE)(FALSE)-> λyx.x
AND(FALSE)(TRUE)-> λyx.x
AND(FALSE)(FALSE)-> λyx.x
OR(TRUE)(TRUE)-> λxy.x
OR(TRUE)(FALSE)-> λxy.x
OR(FALSE)(TRUE)-> λxy.x
OR(FALSE)(FALSE)-> λyx.x
CONS(TRUE)(FALSE)-> λs.s(λxy.x)(λyx.x)
CAR(CONS(TRUE)(FALSE))-> λxy.x
CDR(CONS(TRUE)(FALSE))-> λyx.x
XOR(TRUE)(TRUE)-> λjk.k
XOR(TRUE)(FALSE)-> λjk.j
XOR(FALSE)(TRUE)-> λxy.x
XOR(FALSE)(FALSE)-> λyx.x
ADD(ONE)(TWO)-> 3: λab.a(a(ab)) 
ADD(TWO)(THREE)-> 5: λab.a(a(a(a(ab)))) 
ADD(FIVE)(FOUR)-> 9: λab.a(a(a(a(a(a(a(a(ab)))))))) 
MUL(ZERO)(THREE)-> 0: λfx.x 
MUL(TWO)(THREE)-> 6: λbc.b(b(b(b(b(b(c)))))) 
MUL(THREE)(FOUR)-> 12: λcd.c(c(c(c(c(c(c(c(c(c(c(c(d)))))))))))) 
EXP(TWO)(THREE)-> 8: λab.a(a(a(a(a(a(a(ab))))))) 
EXP(THREE)(TWO)-> 9: λab.a(a(a(a(a(a(a(a(ab)))))))) 
ISZERO(ZERO)-> 1: λxy.x 
ISZERO(ONE)-> 0: λyx.x 
ISZERO(TWO)-> 0: λyx.x 
PRED(ONE)-> 0: λfx.x 
PRED(TWO)-> 1: λac.a(c) 
PRED(THREE)-> 2: λac.a(a(c)) 
PRED(FOUR)-> 3: λac.a(a(a(c))) 
PRED(FIVE)-> 4: λac.a(a(a(a(c)))) 
ISZERO(ZERO)(ONE)(TWO)-> 1: λfx.fx 
ISZERO(ONE)(ONE)(TWO)-> 2: λfx.f(fx) 
Y(ACC)(ZERO)-> 0: λfx.x 
Y(ACC)(ONE)-> 1: λic.i(c) 
Y(ACC)(TWO)-> 3: λce.c(c(c(e))) 
Y(ACC)(THREE)-> 6: λce.c(c(c(c(c(c(e)))))) 
Y(ACC)(FOUR)-> 10: λce.c(c(c(c(c(c(c(c(c(c(e)))))))))) 
Y(FACT)(ZERO)-> 1: λex.ex 
Y(FACT)(ONE)-> 1: λla.l(a) 
Y(FACT)(TWO)-> 2: λac.a(a(c)) 
Y(FACT)(THREE)-> 6: λah.a(a(a(a(a(a(h))))))

注意执行 Y 的时候需要 Y(ACC)(FOUR) 写在一起，如果是：

acc=Y(ACC)
acc(FOUR)

除非 Y(ACC) 不做任何求值替换，只是预处理宏替换，否则先替换 Y(ACC) 然后再把 FOUR 代入会执行错误

另外，由于以上求值器没有优化，执行到 Y(FACT)(THREE) 就比较耗时了，因此只测试到它为止。

完整代码的 github 链接： numbers/lambda/rewriter.py

6. 拓展话题

6.1. 模拟图灵机

有非常多种用 lambda 演算模拟图灵机的方式，这里给出想到的三种：

6.1.1. 软件模拟器层面

图灵机一般由于以下部分组成：

一个无限长的纸带（tape），分成一格一格的方块，每个方块可以存放一个符号。
一个读写头（head），可以读取和写入纸带上的符号，并且可以左右移动。
一个有限状态控制器（state machine），根据当前状态和读取的符号决定下一步操作。

纸带可以用 CONS 来构建 list 模拟, CAR, CDR 可以用于在纸带上左右移动，并用 Y 算子递归地修改 list, 因此可以直接在软件层面模拟图灵机。

6.1.2. 电路层面

前文给出过用 lambda 演算实现 4 bit 整数的加法器，按类似思路甚至可以实现 64 位的完整的 CPU, 有了 CPU 自然可以模拟图灵机，比如图灵机上的编程语言、解释器和应用里提到的 python 实现。

6.1.3. 数学模拟层面： Counter 寄存器机器为桥梁

这也是软件模拟的一种，但它用纯数学编码的形式，并且是基于计算历史，比较有趣。

如果图灵机的纸带上只能写 0 和 1 的话（0/1 可以编码一切），那么图灵机的基本操作可以限制成：

左移一格
写下 0/1
右移一格

那么任何纸带可以分成三个部分：

left, point, right = [0,1, 0, 1], [1], [1,1,0]

第二个部分只有一个元素，就是读写头所在的位置对应的格子里的数据，整个纸带是这三个部分的拼接：

print(left + point + right)

[0, 1, 0, 1, 1, 1, 1, 0]

而 Counter 机器包含 a,b,c 三个寄存器，它们可以存储无限大整数倍并且三个寄存器之间可以互相运算，比如 a=a+b, a=b+c 等等，那么 a 负责编码读写头左侧纸带 left，b 编码 point， c 编码 right 。

编码规则如下：

a = int("".join(map(str, left)), 2)
print(a)
b = point[0]
print(b)
c = int("".join(map(str, right[::-1])), 2)
print(c)

5
1
3

注意 c 是对 right 逆转之后再取二进制编码对应的整数。

那么图灵机层面原子操作和 Counter 寄存器机器操作对应如下：

读写头左移

right = point + right
point = [left[-1]]
left = left[:-1]
print(left, point, right)

[0, 1, 0] [1] [1, 1, 1, 0]

而 Counter 寄存器机器层面等价的操作是

c = c*2 + b
b = a%2
a = a//2
print(a,b,c)

2 1 7

读写头写下 0/1 以 0 为例

point = [0]

print(left, point, right)

[0, 1, 0] [0] [1, 1, 1, 0]

对应 Counter 寄存器机器层面等价的操作是

b = 0
print(a,b,c)

2 0 7

读写头右移

left = left + point
point = [right[0]]
right = right[1:]
print(left, point, right)

[0, 1, 0, 0] [1] [1, 1, 0]

Counter 寄存器机器层面等价的操作是

a = a*2 + b
b = c%2
c = c//2
print(a,b,c)

4 1 3

可以看到，三个能够相互之间进行加法、除法和求余的寄存器完全可以模仿图灵机的任何一个局部状态转移。这意味着，给定任何一个图灵机的程序，只要能够看到它的所有执行过程（甚至可以是无限运行的程序，只要每一步纸带和读写头状态能从一个无限的流中产生出来），那么就可以用一个这样的寄存器机器“影子式模仿”出每一步。

而前文介绍的 CONS 和 CAR, CDR 操作可以保存三个寄存器的值，每个值都是一个可以无限大的 Church 自然数，并且用前文实现的 ADD,DIV,MOD 实现不同寄存器之间运算，因此 lambda 演算理论上可以实现这个 Counter 寄存器机器，从而在图灵机的计算历史上完全实现“影子模仿”。

注意这里突出“计算历史上的模仿”而不是整个机器的模拟，是因为我们没有描述如何在这个寄存器机器上实现逻辑判断（goto），循环，递归等指令，因此没法从程序编写上完全和图灵机的程序（状态转移表）进行等价，实际可以在这个机器上添加这些指令，但那样就和前文里完全模拟图灵机类似了。

本节的“影子模拟”方法有描述上的简洁性（比如把通用的计算过程归类到纯粹小学数学上，类似 Godel 编码），同时也体现了不同计算模型能力上的等价性。

Counter Machine 参考： Turing Machine Alternative (Counter Machines) - Computerphile - YouTube

6.2. 和直觉逻辑的等价

SK 组合子直接来自于命题逻辑里两个公理：

1. A->(B->A) 对应  K = λxy.x

2. (A->(B->C))->((A->B)->(A->C)) 对应 S = λxyz.xz(yz)

这两条公理都是真的，比如对于第一条：

当 A 是真的时候，无论 B 是真还是假， B->A 都是真，因此 A->(B->A) 就是真->真，仍为真
当 A 是假的时候，A->X 直接为真，因此最终还是真

第二条的验证也是类似的。

命题逻辑中唯一的推理规则是 Modus Ponens （MP）: 给定 A->B 以及 A, 那么可以得到 B 。

除了推理之外，还有一个变量替换规则，即如果知道 A->(B->A), 那么也可以得到 x->(y->x), 也就是说，以上公理只是一种模板，只要保持各个符号关系的一致性，可以生成无数的结构相同但变量名不同公理：

我们可以根据以上两个公理结合 MP 证明出 a->a:

1. 根据替换规则和公理 1 得到： a->((b->a)->a)
2. 根据替换规则和公理 2 得到： (a->((b->a)->a))->((a->(b->a))->(a->a))
3. 根据 MP 以及 1 和 2 得到： ((a->(b->a))->(a->a))
4. 根据替换规则和公理 1 得到： a->(b->a)
5. MP 以及 3 和 4 得到： a->a

这个过程对应了 I=SKK, 同时注意到这种根据公理来进行证明（演绎）的方法其实很需要技巧，因此我们更多时候会偏向于用“自然演绎”，方法如下：

1. a->a 其实说的是，如果 a 成立，那么 a 也成立。那么直接假设 a 成立
2. 根据替换规则和公理 1 得到： a->(a->a)
3. 根据 MP 以及 1 和 2 得到： a->a
4. 根据 MP 以及 1 和 3 得到： a

我们在假设 a 成立的情况下得到了 a, 于是我们可以知道 a->a, 要证明基于公理的演绎系统和以上自然演绎是等价的需要用到 Deduction theorem - Wikipedia 。

总之，自然推理这种证明方式更直观，更接近“计算”方式。

现在来比较 KS 和以上两条公理的具体细节：

对于公理 A->(B->A), 当给定 A 时就可以得到 (B->A), 再给定 B 就可以得到 A, 也就是给定连续的 A,B 返回 A 。

对于 K 算子正是如此：

print(show_history("(λxy.x)AB", 2))

--1 (λy.A)B
--2 A
A

组合子逻辑或 lambda 演算中的 beta 规约对应的是 MP 规则，而 alpha 规约对应的是替换规则。

对于公理 (A->(B->C))->((A->B)->(A->C)) ，它可以看作一种如何用级联的方式证明 C 成立的方法，先给定命题 (A->(B->C), 根据 Modus Ponens 可以得到 ((A->B)->(A->C)), 然后给定 (A->B) 得到 A->C, 再给定 A 可以得到 C.

把 A->(B->C) 记为 x, 对应 lambda 表达式 λAB.C, 把 A->B 记为 y 对应 λA.B , 把 A 看作 z ，那么公理 2 就是给定函数 x, y 和 z 情况下能够得到 C 。

这里的证明步骤是：

由于 y 对应了 A->B, z 对应了 A, 那么 y(z) 就得到了 B,
由于 x 是以 A 为前提的命题 A->(B->C), 所以 x(z) 就得到了 B->C
1 中已经得到了 B, 再把 B 代入到 B->C 就得到了 C
联合起来就是 x(z)(y(z)), 对应 (λxyz.x(z)(yz))

S 算子正是如此：

print(show_history("(λxyz.xz(yz))(λAB.C)(λA.B)A", 5))

--1 (λyz.(λAB.C)z(yz))(λA.B)A
--2 (λz.(λAB.C)z((λA.B)z))A
--3 (λAB.C)A((λA.B)A)
--4 (λB.C)((λA.B)A)
--5 C
C

beta reduction 对应的证明顺序是：

- 给定 A->B 和 A, 可以得到 B
- 给定 A->(B->C) 和 A, 可以得到 B->C
- 给定 B 和 B->C, 可以得到 C

以上两条公理只是命题逻辑中希尔伯特公理集合（P2 ）的子集，比如它缺少一条关于否定命题的公理，一般是逆否命题的支撑： (~P->~Q)->(Q->P) 整个系统中实际就缺少 ~ 这个符号，因此组合子逻辑或者 lambda 演算等价的是命题逻辑里少了这条逆否公理且不包括否定形式命题的子集（称为直觉逻辑中的蕴含子集）。

Haskell Curry 等人系统论证了逻辑系统中某个子集和 lambda 演算有同构关系，参考 Curry–Howard correspondence - Wikipedia

6.3. 不可判定性

上节论证了 lambda 演算可以模拟图灵机，那么自然停机问题的不可判定性也就“转嫁”到了 lambda 演算上。

实际上，历史上第一个不可判定性问题是 Church 用 lambda 演算所表达的（比 Turing 早 1 年），被称为 Beta Normal Form 的判断问题，用以下例子来说明。

def show_history(exp, step=5):
    ast = LLLparser(exp).parse()
    generator = VariableGenerator(get_variables(ast))
    for i in range(1,step+1):
        ast = beta_reduce(ast, {}, generator)
        print(f"--{i}", ast)
    return ast

decode(show_history("(λfx.f(fx))(λfx.f(fx))", 10))

--1 λa.(λfx.f(fx))((λfx.f(fx))a)
--2 λa.(λfx.f(fx))((λfx.f(fx))a)
--3 λa.λb.(λfx.f(fx))a((λfx.f(fx))ab)
--4 λab.(λfx.f(fx))a((λfx.f(fx))ab)
--5 λab.λx.a(ax)(λx.a(ax)b)
--6 λab.(λx.a(ax))((λx.a(ax))b)
--7 λab.a(a((λx.a(ax))b))
--8 λab.a(a(a(ab)))
--9 λab.a(a(a(ab)))
--10 λab.a(a(a(ab)))
4

以上是计算 2 的 2 次方，它在进行到第 8 步之后就变成了 λab.a(a(a(ab))), 无法再进行 beta_reduce ，因为第一个 lambda 没有 apply 的参数了，而 lambda 表达式的内部也没有嵌套的可以继续 apply 的 lambda 表达式，都是纯变量名了。所以之后执行 beta_reduce 返回的是前一个表达式本身，这种形式就是 Beta Normal Form, 也就是该表达式已经没有可以再执行 apply 的“潜力”了，前文所有的例子最终都会执行到这种形式（类似停机了）

但给定以下例子（称为 W 算子，也是 MM 算子组合形式）：

print(show_history("(λf.ff)(λf.ff)"))

--1 (λf.ff)(λf.ff)
--2 (λf.ff)(λf.ff)
--3 (λf.ff)(λf.ff)
--4 (λf.ff)(λf.ff)
--5 (λf.ff)(λf.ff)
(λf.ff)(λf.ff)

它无论进行多少次 beta 规约，都会得到自身，而自身还是一个可以继续规约的形式。这个例子中每一行的相等和上一个例子中第 8 到第 10 行的相等并不一样，本例子中虽然每行都相等，但实际每次都执行了一次 beta 规约，而上一个例子是无法进行规约。

用 python 语言来说的话，无法规约的情况下，前后两行的内容是引用上相同的，记前后两行为 a 和 b 的话，a is b 和 a == b 都返回 True 。

但 W 算子规约过程中打印出的前后两行，虽然 a == b 为 True, 但 a is b 为假。

另外一种特别的规约模式是 Y 组合子，越进行 beta reduce 反而越增长（反 reduce）：

print(show_history("(λf.(λx.f(xx))(λx.f(xx)))R", 8))

--1 (λx.R(xx))(λx.R(xx))
--2 R((λx.R(xx))(λx.R(xx)))
--3 R(R((λx.R(xx))(λx.R(xx))))
--4 R(R(R((λx.R(xx))(λx.R(xx)))))
--5 R(R(R(R((λx.R(xx))(λx.R(xx))))))
--6 R(R(R(R(R((λx.R(xx))(λx.R(xx)))))))
--7 R(R(R(R(R(R((λx.R(xx))(λx.R(xx))))))))
--8 R(R(R(R(R(R(R((λx.R(xx))(λx.R(xx)))))))))
R(R(R(R(R(R(R((λx.R(xx))(λx.R(xx)))))))))

因此，判断某个 lambda 公式是否已经“收敛”是容易的，即用 == 去检查 beta 规约前后两次的结果在外表上是否相同，这只是字符串/数据结构语法层面的对比（前文的 evaluate 函数就用 tree_equal 这种形式相等判断函数来决定是否继续 beta reduce），但判断这个公式是否能够继续规约到无法规约的状态（判断前后两个公式是不是 is 级别的相同，操作语义上是否相同），被证明为是一个不可判定问题。

Church 用的是类似 Godel 证明不完备定理的方式进行证明的，以下用一个更容易描述的停机问题版本来说明：

由于 lambda 表达式只是普通的英文字符串，所以它可以编码成一个整数，比如直接把每个字母映射成一个数字， λ 对应 1, f 对应 2, 句号 . 对应 3, λf.ff 就可以编码成 12322 。反过来给定数字 12322 它可以解码成唯一的表达式 λf.ff 。

lambda 表达式的 alpha 和 beta 规约实际是一个字符串到另一个字符串的转换函数，在编码层面就是把一个整数映射到另一个整数的函数。由于这两种规约非常“机械”，使得这种映射函数实际可以用一般的加减乘除来实现（类似上一节中可以用三个寄存器数值的加减乘除来描述图灵机读写头和纸带的变化）。

现在假设存在一个组合子，它由 ADD/DIV/MOD 以及判断、递归等算子构成，类似 Y(D) 形式，它可以继续接受一个用 Church 编码表示的数字，就像 Y(fact)(n) 可以计算阶乘一样，Y(D)(n) 给出的结果是 TRUE 或 FALSE:

如果 N 解码后 lambda 表达式有一个 beta Noraml form, 那么返回 TRUE
如果 N 解码后 lambda 表达式没有 beta Noraml form （类似上一个代码块的例子）, 那么返回 FALSE

现在问题是，一旦有了 Y(D) 组合子，那么可以用这个组合子构造一个新的组合子，记为 H:

H = λf.λn.ISTRUE(Y(D)(n))((λf.f(f))(λf.f(f)))(λfx.f(fx))

H 的逻辑是，给定数字 n, 先用 Y(D)(n) 判断是否有 Normal form, 如果有，那么返回 (λf.ff)(λf.ff) ，它是没有 Normal form 的公式（会永远执行下去），如果没有，那么返回一个有 Normal Form 的公式，比如 λfx.f(fx))

注意这个函数的形式和阶乘函数 FACT=λfn.ISZERO(n)(ONE)(MUL(n)(f(PRED(n)))) 是类似的，它可以传递给 Y 算子，得到 Y(H), 而 Y 算子有一个不动点性质 H(Y(H)) = Y(H)

现在问题是，Y(H) 是有 normal form 还是没有？

H(Y(H)) 是什么？它会判断 Y(H) 是有 normal form:

如果有，那么返回一个没有 normal form 的 (λf.ff)(λf.ff), 而这就等于 Y(H) 本身，导致了矛盾
如果没有，那么返回一个有 normal form 的 (λfx.f(fx)), 而这就等于 Y(H) 本身，导致了矛盾

以上所有构成 H 的算子，除了 D, 我们都是实现过的，因此只有可能 D 是不存在的。

这个证明实际是把停机问题搬到了 lambda 演算上。

参考： The Halting Problem (part 1)

6.4. 万物理论和复杂性

Combinators: A 100-Year Celebration - YouTube 是 Stephen Wolfram 关于组合子逻辑的报告，其中回顾了很多历史以及将组合子扩展到物理世界领域。

组合子、元胞自动机都展现了一种用极为简单的规则却可以产生无限复杂事物的能力，Wolfram 想用它们作为研究复杂的物理宇宙世界的一种简化模型，从中找出一些更为通用的解释物理规律的模式。

6.5. 其他参考资料

lambda 演算基本概念部分，以下是一些个人觉得比较好的参考：

Lambda Calculus_ PyCon 2019 Tutorial (Screencast)_哔哩哔哩_bilibili 讲解非常精彩，本文前半部分 python 实现许多参考自该视频。

以下两个教程很多内容和以上视频类似，但更偏向使用组合子的术语，也值得一看：

解释器（或重写器）部分的实现：

语法解析部分可以参考递归⤵动态规划⤴和语言 parsing🌲 里 LL parsing 的介绍。
alpha 替换的实现可以参考数理逻辑及其 python 实现里谓词逻辑解释器中变量替换的部分（第九章）。

各个概念的维基百科

7. 在线 lambda 演算解释器

这里同时实现了一个 js 版本的 lambda 演算解释器，代码见 numbers/lambda/rewriter.js

可以在下方编辑框里修改代码并执行：

ONE=Lfx.f(x) 是赋值（宏替换），并不会被打印出来
;; Lfx.f(x) 是注释，直接忽略
Lfx.f(x) 是执行，其结果会被打印

;; 在此修改编辑（edit here）
λfx.f(fx)
(λfx.f(fx))(λfx.f(fx))
I = λx.x
K = λxy.x
KI = KI
C = λfxy.fyx
S = λxyz.xz(yz)
NOT = C
TRUE = K
FALSE = KI
AND = λab.aba
OR = λab.aab
CONS = λabs.sab
CAR = λp.pK
CDR = λp.pKI
XOR = λab.OR(AND(NOT(a))(b))(AND(a)(NOT(b)))
CK
CKI
SKK
NOT(TRUE)
NOT(FALSE)
AND(TRUE)(TRUE)
AND(TRUE)(FALSE)
AND(FALSE)(TRUE)
AND(FALSE)(FALSE)
OR(TRUE)(TRUE)
OR(TRUE)(FALSE)
OR(FALSE)(TRUE)
OR(FALSE)(FALSE)
CONS(TRUE)(FALSE)
CAR(CONS(TRUE)(FALSE))
CDR(CONS(TRUE)(FALSE))
XOR(TRUE)(TRUE)
XOR(TRUE)(FALSE)
XOR(FALSE)(TRUE)
XOR(FALSE)(FALSE)

ZERO = λfx.x
ONE = λfx.fx
TWO = λfx.f(fx)
THREE = λfx.f(f(fx))
FOUR = λfx.f(f(f(fx)))
FIVE = λfx.f(f(f(f(fx))))
SUCC = λnfx.f(nfx)
ADD = λmn.m(SUCC)(n)
ADD(ONE)(TWO)
ADD(TWO)(THREE)
ADD(FIVE)(FOUR)
MUL = λmn.m(ADD(n))(ZERO)
MUL(ZERO)(THREE)
MUL(TWO)(THREE)
MUL(THREE)(FOUR)
EXP = λmn.n(m)
EXP(TWO)(THREE)
EXP(THREE)(TWO)

ISZERO = λn.n(K(FALSE))(TRUE)
ISZERO(ZERO)
ISZERO(ONE)
ISZERO(TWO)
LEQ = λmn.ISZERO(SUB(n)(m))

T = λp.CONS(CDR(p))(SUCC(CDR(p)))
PRED = λn.CAR(n(T)(CONS(ZERO)(ZERO)))
PRED(ONE)
PRED(TWO)
PRED(THREE)
PRED(FOUR)
Y = λf.(λx.f(xx))(λx.f(xx))
ACC = λfn.ISZERO(n)(ZERO)(ADD(n)(f(PRED(n))))
ISZERO(ZERO)(ONE)(TWO)
ISZERO(ONE)(ONE)(TWO)
Y(ACC)(ZERO)
Y(ACC)(ONE)
Y(ACC)(TWO)
Y(ACC)(THREE)

;; Running the code below might take up to a few seconds, depending on your system's processing speed.
;;Y(ACC)(FOUR)
;;FACT=λfn.ISZERO(n)(ONE)(MUL(n)(f(PRED(n))))
;;Y(FACT)(ZERO)
;;Y(FACT)(ONE)
;;Y(FACT)(TWO) 
;;Y(FACT)(THREE)

Output:

radioLinkPopups

#rethink

如对本文有任何疑问，欢迎通过 github issue 或进行反馈