别样的 Lambda 大战之邱奇数（Church Numerals）

提示

写作背景：

本人周六不知道为什么还要补线性代数的课，好巧不巧在机房上课，于是玩弄了一下电脑上的 Python，并深刻学习了 Lambda 相关的理论。

此处的 Lambda 指的不是匿名函数。

众所周知，Lambda 的计算能力和图灵机等效^[1]。

于是自然而然的，我们可以考虑使用纯 Lambda 来定义自然数。显然我们一切都是 Lambda，于是我们不能使用 Python 自带的 int 数据类型。所以我们定义如下的工具函数来显示数值：

def to_int(n):
    print(n(lambda x: x + 1)(0))

显然我们可以从这里反推出我们定义的 Lambda 自然数，也就是 Church 数的形式如下：

NUM = f(f(f(...f(x))))

即对于 Church 数 NUM，对于给定的参数函数 f 和另外一个参数 x，有以 x 为初始参数嵌套执行 f 这个东西 NUM 次。总之差不多这个意思，具体定义看 Wiki 去吧。

于是我们不难得出零的定义：

ZERO = lambda f : lambda x : x

显然就是什么都不执行。

根据皮亚诺公理，然后我们就要开始构思如何表示一个数的后继了，在这里很显然就是在执行 NUM 次 f 过后再执行一次 f 就行，于是有：

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

注意到这里使用的 Lambda 是嵌套的，即我们返回的也是一个 Lambda，考虑工程中一般的对于有多个变量的 Lambda 的写法可能是 lambda x, y, z: ...，但是我们在这里的写法叫做柯里化，具体看 Wiki 去，总之就是把多个参数的函数转化为多个单一参数函数的调用。这样的做法至少在这里是有若干好处的，但我也不知道具体怎么形容，总之把函数看作一等公民，我们返回的就是函数。

于是我们顺便定义几个常用数字：

ONE = SUCC(ZERO)
TWO = SUCC(ONE)
THREE = SUCC(TWO)

于是我们现在实现了无数个自然数了。但是我们现在光有这些数字的确太过无聊，我们可以定义几个运算，比如加法：

ADD = lambda a : lambda b : lambda f : lambda x : a(f)(b(f)(x))

因为不难想象加法就是先执行 a 次然后执行 b 次嘛，以此类推，我们可以有乘法：

MUL = lambda a : lambda b : lambda f : lambda x : a(b(f))(x)

就是执行 a 次重复 b 次 f 的过程。当然如果你比较闲，觉得可以根据我们小学数学的知识把加法看作多次求后继的过程，乘法看作多次相加的过程，可以写成下面这样：

ADD = lambda a: a(SUCC)
MUL = lambda a: lambda b: b(ADD(a))(ZERO)

显然上面的是执行 SUCC 操作 a 次，下面是执行 ADD(b) 操作 a 次。因为 ADD 实际上是二元运算符，所以这里有一个 ZERO。不过这种写法感觉很蛋疼啊。

以此类推我们还有乘方操作，这个似乎是最简单的

POW = lambda a : lambda b : b(a)

如果你觉得乘方是多个乘法：

POW = lambda a: lambda b: b(MUL(a))(ONE)

然后我们突然发现我们缺少了一个重要的东西——前驱。

仔细一想确实是这样的，于是我们可以尝试构造 F = 0， F F = 1，F (F F) = 2 这样的玩意。这样我们就有 N F 就是前驱了。

于是我们可以构造一个下面一样的东西：

PAIR = lambda x: lambda y: lambda f: f(x)(y)
TRUE = lambda x: lambda y: x
FALSE = lambda x: lambda y: y

INIT = PAIR(ZERO)(ZERO)
NXT = lambda p: PAIR(p(FALSE))(SUCC(p(FALSE)))
PRED = lambda n: n(NXT)(INIT)(TRUE)

这里我们保存一个二元组 (n - 1, n) 然后不断轮转，这样我们就能找到前驱了。在这里因为是自然数所以零的前驱是零。

另外一种更加优雅的写法是：

PRED = lambda n: lambda f: lambda x: n(lambda a: lambda b: b(a(f)))(lambda u: x)(
    lambda i: i
)

原理也是差不多的。

然后我们有 PRED(SUCC(ZERO))=ZERO，我们就可以做减法了，对于 SUB(a)(b) 来说，我们有：

SUB = lambda a: lambda b: b(PRED)(a)

这里如果 b 比 a 大的话会减到零。

然后我们考虑实现一个简单的应用——斐波那契数列。

显然有：

$$f(0)=0\\ f(1)=1\\ f(x)=f(x-1)+f(x-2)$$

不难发现如果我们要实现这个还需要判断是否相等，显然我们这里有减法，那么 EQ(a)(b) 当且仅当 AND(IS_ZERO(SUB(a)(b)))(IS_ZERO(SUB(b)(a)))

然后我们就要实现一下判断是否为零，不难实现：

IS_ZERO = lambda n: n(lambda x: FALSE)(TRUE)

如果 n 不是零的话，就会进入那个永远只能返回 FALSE 的 Lambda，否则返回 TRUE。然后我们实现一下 AND：

AND = lambda a: lambda b: a(b)(FALSE)

这里由乘法原理可以得到。

于是我们可以写 EQ 了：

EQ = lambda a: lambda b: AND(IS_ZERO(SUB(a)(b)))(IS_ZERO(SUB(b)(a)))

其实我们也懒得写 IF，因为考虑 EQ(x)(y)，如果为 TRUE 就是前者，否则是后者，我们直接用就好了。

但是我们还是不能直接写一个 FIB 出来，原因和 C++ 里面 Lambda 不能直接写递归类似，我们需要用一个用其他方式来实现递归。需要写一个 Y 组合子——准确地说是 Z 组合子，因为 Python 不是惰性求值的语言。

实际上我们之前写的有一部分没有用到，因此下面给出用到的部分的完整代码：

def to_int(n):
    print(n(lambda x: x + 1)(0))


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

ADD = lambda a: lambda b: lambda f: lambda x: a(f)(b(f)(x))

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

PRED = lambda n: lambda f: lambda x: n(lambda a: lambda b: b(a(f)))(lambda u: x)(
    lambda i: i
)

IS_ZERO = lambda n: n(lambda x: FALSE)(TRUE)

AND = lambda a: lambda b: a(b)(FALSE)

F = lambda f: lambda n: IS_ZERO(n)(lambda: ZERO)(
    lambda: IS_ZERO(PRED(n))(lambda: SUCC(ZERO))(
        lambda: ADD(f(PRED(n)))(f(PRED(PRED(n))))
    )()
)()


Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))

FIB = Z(F)

n = ZERO
for _ in range(10):
    to_int(FIB(n))
    n = SUCC(n)

有输出：

0
1
1
2
3
5
8
13
21
34

以上～

---

1. 随便百度可以得知。 ↩︎