在Python中写lambda calculus

前言

可能会有一个系列，专门记录自己研究过的奇技淫巧。 虽然有时候我们会觉得奇技淫巧是花里胡哨，华而不实的，但是当自己写出来的时候，就还是“真香”。 况且奇技淫巧之中其实蕴含着优美与真理，主要看你怎么去理解它们了。 这次的问题来源于我在网上看到的一个用lambda表达式写递归的Python语句

factorial = (lambda a:lambda v:a(a)(v))(lambda s: lambda x:1 if x==0 else x*s(s)(x-1))  # 实现了递归
print(factorial(5)) # 120

上面这个求阶乘的表达式我看了快半个小时才觉得自己大概是看懂了。好奇心驱使我开始往下挖坑，想看怎样能更好地理解这种写法。 因为学过Haskell，所以我知道这里可能涉及到了lambda calculus和 Y combinator的内容。 之前看过一点这个topic，但是也没有太深入研究。

先扯扯lambda calculus

lambda calculus可以理解为一个数学系统，其中最基本的元素或者说研究对象是函数, 通过函数来构造出我们做计算所需要的所有“材料”（比如自然数，四则运算符等）。 其实这有点像集合论，通过集合论可以构造出现代数学的几乎所有内容，比如皮亚诺公理就是用集合（集合套空集，集合套集合的骚操作）构造自然数。 说回lambda calculus，lambda calculus中的函数具有一些特征，这些函数是单参数的，它们能且只能接受一个函数作为参数； 当我们把一个函数作用于另一个函数（后者作为前者的参数），得到的返回值也是一个单参数函数。 这样整个系统其实就封闭了，我们可以在里面搭积木而不再需要其他任何东西了。 然后看看notation:

λ x. E   # 这表示一个函数，函数参数为x，E为函数所作运算的具体表达式
M N      # 将函数M作用于函数N，函数作用是可以省略括号的

第一个式子中的E可以包含x，也可以不包含，E就相当于一个f(x)， 如果f(x)的表达式中不包含x，就意味着函数的输出和输入无关。 lambda calculus中所有合法的表达式的值都是单参数函数。 另外函数是左结合的，即X Y Z = (X Y) Z =(X(Y))(Z)，所以X (Y Z)这个式子里的括号是不能去的。 函数式编程中的lambda表达式就是借鉴了λ x. E这样的写法，例如我们可以在Python中这样定义函数（Python借鉴了函数式编程）:

f = lambda x: x + x  # f(2) 的值是4
g = lambda x, y: x * y  # f(2, 3) 的值是6

但是λ x. E和编程语言中的lambda表达式其实是有区别的，首先语法上lambda表达式并没有限制参数的个数（对于有柯里化特性的语言写两个参数在语义上还是可以理解成单参数函数的，例如Haskell），然后就是参数的类型不一定是函数，所创建的函数的返回值类型也不一定是函数。注意，lambda表达式的返回值是函数，但是这个函数的返回值，即它的输出是要看它接收参数后的运算结果，在lambda calculus中这种运算结果的值仍然是函数。 然后看一些基本的恒等式

λ x. F x = F
(λ x. E) T = E[x:=T]
λ x. E[x] = λ y. E[y]

第二个式子的右侧是值把表达式E中的所有x都替换成T，第三个式子是说把参数名字换掉不改变它所代表的函数。 这三个式子的成立都很显然，应用它们做一些数学证明的时候可能从左推到右，也可能从右推到左。
然后我们看看，lambda calculus中是如何定义自然数的

0 = λ f. λ x. x
1 = λ f. λ x. f x
2 = λ f. λ x. f (f x)
3 = λ f. λ x. f (f (f x))

我们称这样定义的自然数为Church数（不是教堂，是lambda calculus的发明者的名字）。 对这种定义的一种粗略的理解是，自然数n是这样一个函数，它接收任意一个函数f，返回了一个函数A，这个函数A在接收任意一个函数x,返回一个函数B，这个B的值等价于f作用于x，连续作用n次的结果。 但是，为什么要这样定义呢？后面我们还要定义各种运算，定义完的结果就是1+1=2这样的等式的成立是可以在lambda calculus框架下进行证明的。所以为什么这样定义，因为自洽。 虽然可以证明某某等式的成立，但是lambda calculus中的表达式往往又“臭”又长，用人脑去解析它们真的十分费力，所以我就想能不能用Python对表达式进行计算，然后print出一个函数所代表的Church数的值。

Python模拟lambda calculus

我希望的模拟不是字符串的规约推导，而是用Python的lambda表达式去比较真实的模拟，同时尽可能的保持lambda calculus的特性，也就是所有表达式或名字的值都是函数类型。 所以我写了下面一段十分神奇的代码：

# interpreting and visualize
def x_():
    return 0

def f_(x=None):
    return lambda : 1 + x()

def interpret(f):
    '''查看一个函数的自然数值，具体见下文'''
    print(f(f_)(x_)())

def predicate(f):
    '''查看一个函数的bool值，具体见下文'''
    if f(f_)(x_)() == 0:
        print(False)
    else:
        print(True)

这段代码几乎满足了我的所有要求，唯一的不足已经是语言本身的不足了（Python不支持惰性求值）。 具体的使用看后面的例子，后面例子里的所有代码（除了调用interpret或predicate）都是在对函数进行运算了，输入、输出和各种变量什么的全都是单变量函数。

自然数

我们现在开始做一些定义和测试。 根据上面提到的Church数的定义，我们可以这样写

Church_0 = lambda f: lambda x: x
Church_1 = lambda f: lambda x: f(x)
Church_2 = lambda f: lambda x: f(f(x))
Church_3 = lambda f: lambda x: f(f(f(x)))

代码定义完全照抄上面的数学定义。 然后我们print它们的值看看

interpret(Church_0)  # 0
interpret(Church_2)  # 2
interpret(Church_3)  # 3

后面的注释就是打印的结果，十分完美。

运算符

然后我们再利用这套代码定义一些运算符看看。 下面是我们在这篇文章中将要使用的运算符的数学定义

SUCC = λ n. λ f. λ x. f (n f x)  # 加1运算
PLUS = λ m. λ n. λ f. λ x. m f (n f x)  # 求和运算
MULT = λ m. λ n. m (PLUS n) 0  # 求积运算
PRED = λ n. λ f. λ x. n (λ g. λ h. h (g f)) (λ u. x) (λ u. u) # 减一运算

这里先讲一下二元运算符PLUS和MULT，PLUS x y 这个式子表示 x + y，如果x是Church数1，y是Church数2，PLUS x y的返回值就是Church数3。 但是PLUS仍然是一个单参数函数，它接收函数x然后返回 PLUS x，PLUS x是一个函数，这个函数接收一个函数y然后返回x + y，即PLUS x y = (PLUS x) y，这就是所谓的柯里化。 MULT运算同理。 下面我们上代码

SUCC = lambda n: lambda f: lambda x: f(n(f)(x))
interpret(SUCC(Church_3)) # 4

PLUS = lambda m: lambda n: lambda f: lambda x: m(f)(n(f)(x))
interpret(PLUS(Church_3)(Church_2)) # 5

MULT = lambda m: lambda n: m(PLUS(n))(Church_0)
interpret(MULT(Church_2)(Church_3)) # 6

PRED = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u: x)(lambda u: u)
interpret(PRED(Church_3)) # 2

虽然这些定义看起来很吓人，但是结果都十分正确。 我们试一个更复杂的

interpret(PRED(MULT(Church_2)(Church_3))) # 5

也是正确的。 当我照抄数学定义然后成功print出正确的结果的时候，感到惊喜且惊奇。 我们只是搭好了一个简单的地基，然后就看着这些建立在地基之上的复杂事物表现出我们所期待的行为。 这就是数学的魅力吧。

逻辑运算

上文说lambda calculus可以定义出我们用来做计算需要的所有东西，这里的计算就包括逻辑计算。和C语言类似，我们定义表示0的函数为False，而其他的函数为True。 看一下具体的数学定义

TRUE = λ u. λ v. u
FALSE = λ u. λ v. v

Python的代码定义如下

Church_True = lambda u: lambda v: u
Church_False = lambda u: lambda v: v

根据我们之前提过的恒等式中的第三条，我们知道False和0在lambda calculus中是同一个函数。所以除了interpret，我写了另一个函数predicate，它把函数看作是一个逻辑断言，并打印出其真值。我们来测试一下

predicate(Church_False)  # False
predicate(Church_True)   # True
predicate(Church_0)      # False
predicate(Church_2)      # True

与我们预期的一样，除了0, 我们之前定义的Church数都被认为是逻辑True。 这样我们就在lambda calculus的背景下构造了一个布尔代数系统，我们可以定义各种逻辑运算符和布尔函数

# AND = λ p.λ q.p q p
AND = lambda p: lambda q: p(q)(p)
# OR = λ p.λ q.p p q
OR = lambda p: lambda q: p(p)(q)
# NOT = λ p.p FALSE TRUE
NOT = lambda p: p(Church_False)(Church_True)
predicate(NOT(OR(Church_False)(Church_True)))  # False

基于0和False的一致性，我们可以定义一个判断输入是否为0的函数，当且仅当输入为0时返回True：

# 数学定义： ISZERO = λ n. n (λ x. FALSE) TRUE
ISZERO = lambda n: n(lambda x: Church_False)(Church_True)
predicate(ISZERO(Church_0))  # True
predicate(ISZERO(Church_3))  # False

递归

现在到了最激动人心的part。 我们以阶乘函数为例来进行探讨，首先来看看在Haskell中我们如何用递归的方式定义阶乘函数（用Haskell举例是因为Haskell写出来的阶乘函数特别接近我们用自然语言进行的递归算法的描述，同时又可以比较形式化）

factorial 0 = 1
factorial n = n * factorial (n-1)

从中我们看到了递归函数的一个重要特征，就是函数名会出现在函数定义里头。 所以乍看之下我们会觉得lambda表达式无法表达递归函数，如果硬着头皮，我们会写出像下面这样的式子

F = λ x. F (PRED x)

这个式子存在两个问题，一是在数学中我们一般不允许循环定义，你还没有定义完成F是啥，就还不能使用F，另一方面，即使语法上允许我们这么表达一个函数，这个函数也有可能是个没有尽头的死循环（注意没有输出就不是函数了）。 不过Python中的lambda表达式允许我们进行“循环定义”，因为与数学不同，Python中的函数是先定义再调用的，只有在调用的时候（也就是你在函数名后面加()的时候，如fun()）才会真正去执行一个函数的代码，而定义的时候只是将一个函数名和一串代码绑定起来，并不会去分析这段代码究竟干了什么。所以我们可以像下面这样定义

FACT_ = lambda n: n(lambda u: MULT(n)(FACT_(PRED(n))))(Church_1)
interpret(FACT_(Church_0))  # 1
interpret(FACT_(Church_3))  # 6

这个FACT_功能良好。 有两点十分有趣，我们看到0的阶乘十分自然的等于1，说明数学家们当初规定0! = 1不是随便规定的，是有一定的道理的。 另一点就是FACT_并没有陷入死循环，这一点看似很奇怪，因为我们似乎并没有像传统递归写法那样设置临界条件，那这个循环函数调用是如何停下来的呢？ 这里就涉及到Church0的定义的奥妙之处了

0 = λ f. λ x. x

实际上函数运算到最后会出现0(MULT n (PRED n))(1)这样的情况，这个时候按0的定义，他会直接忽略传进去的(MULT n (PRED n))而直接返回函数1。 (MULT n (PRED n))只出现在参数里但不再出现在函数表达式里，所以也就不会再去往下计算它了。
说到这里，阶乘函数的实现还是依赖于Python的语言特性，而不是纯数学的lambda calculus的定义，而且看起来lambda calculus没法使用还没定义好的名字，所以似乎也写不出递归函数。 但是别慌，数学家们还是研究出来了，lambda calculus中有个叫Y combinator（Y组合子）的东西为lambda calculus提供了递归的实现手段

Y = λ f. (λ x. f (x x)) (λ x. f (x x))

其实并不神秘，稍作思考我们就可以得到下面这个结论

Y F = F(F(F(F(. . .)))) # 无限循环调用

然后我尝试在Python中实现Y combinator

Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))
F = lambda g: lambda n: n(lambda u: MULT(n)(g(PRED(n))))(Church_1)
FACT = Y(F)
interpret(FACT(Church_3))

然后不幸发生了，到第三行Python报错了，说是递归爆栈了，也就是陷入了死循环。这是因为Python不是惰性求值的，当我执行FACT = Y(F)的时候，解释器就会去执行Y函数的计算，按照定义自然会出现无限调用的情况。 lambda calculus所希望的是，你先别去计算Y(F)的返回值究竟是个什么函数，等这个函数作用了Church_3再去实施计算，到时候Church_0就会负责把死循环截断。所以很多函数式编程语言都会设计成惰性求值来增强语言的表达能力，避免不必要的死循环。
那么路走到这里，就走到尽头了吗？并没有，回顾我们开篇提到的阶乘函数的实现，它也是用lambda表达式写的，也没有使用未定义的名字，于是我仿照它不使用Y combinator，重新定义了阶乘函数

T = λ f. λ x. f f x
G = λ g. λ n. n (λ u. MULT n (g g (PRED n))) 1
FACT = T G

然后使用Python实现并测试

T = lambda f: lambda x: f(f)(x)
G = lambda g: lambda n: n(lambda u: MULT(n)(g(g)(PRED(n))))(Church_1)
FACT = T(G)
interpret(FACT(PLUS(Church_3)(Church_2)))  # 120

成功了。 一个合理的解释是，在数学上两个FACT是同一个函数，只是我们通过数学上的变换调整了函数的组织方式，从而改变了其中的运算顺序，避免了因为不支持惰性求值而造成的问题。 这个猜想的正确性需要需要通过数学证明来保证，也就是证明Y F = T G。

证明

我们观察到G和F的主要区别就在于g (PRED n)和g g (PRED n)，所以我们的入手点也是这里，先尝试把两个g变成一个函数来表示

G = λ g. (λ h. λ n. n (λ u. MULT n (h (PRED n))) 1)(g g)
  = λ g. F (g g)

所以有

T G = (λ f. λ x. f f x)(λ g. F (g g))
    = λ x. (λ g. F (g g)) (λ g. F (g g)) x
    = (λ g. F (g g)) (λ g. F (g g))
    = (λ f. (λ g. f (g g)) (λ g. f (g g))) F
    = Y F

证明成功。

结尾

这次的探究启发了我们写递归函数的方式，并不是只有自己定义（中出现）自己才能实现递归。当然我不会在Python中这样写递归函数，因为可读性太差，对于不了解函数式编程的人，这样的代码非常不友好。即使在Haskell中，我也不会这样写，因为Haskell中有更优美的递归写法。但是lambda calculus中对函数的变换、组合和使用的精髓是值得我们学习的，这有助于我在写函数式的Python语句或写Haskell时更清楚我能写什么，我能怎么写。

参考

1. Lambda_calculus
2. 各语言Y组合子大比拼