邱奇计数 (1)

让我们来谈谈抽象。

什么是抽象？几乎所有程序员都听说过。不就是把一些对应的实体抽象成一些数据结构啊，算法啊或者设计模式之类的，然后写成代码呗。

但是你真的懂抽象的威力吗？我们只有数据结构和算法等抽象吗？能不能不使用任何数据结构去表达一个二元组呢？

这一系列短文有3篇（可能），我将从Python的基础入手，带你简单入门Lambda表达式，然后走进邱奇计数的世界，见证函数式编程的高阶抽象能力。

准备好了吗？让我们开始吧。

注：阅读本系列短文你只需要简单接触过Python和初中代数水平即可。

0x00. 基础

为什么选择Python？

Python使用简单，语法易于理解，Lambda Expression虽然比起函数式语言很弱，但是应付邱奇计数绰绰有余。

而如果使用Haskell，阅读者需要对类型论有一定的了解；而Scheme又不利于测试和阅读。

权衡之下，我选择了Python。

一切的开始，我们先了解以下做Lambda Expression。

Lambda Expression，在程序语言中我们可以简单理解为匿名函数。所谓匿名函数，就是没有名称的函数，多为临时使用而创建。

在数学上，一个Lambda Expression是这么表述的：$\lambda x. \lambda y. \lambda z. x^2+y^2+z^2$，它其实和如下的$f$相等：$f(x,y,z)=x^2+y^2+z^2$。这个表达式很好理解，$\lambda$意味着一个函数开始了，后面跟着的$x$是它的第一个参数，然后$.$，这个点号代表求值表达式。上面这个式子实际上是三个参数的级联应用，也就是先应用$x$，再应用$y$，最后应用$z$。我们把一个函数$f$应用$n$次表达为$f^n$，也就是说，$f^n=\underbrace{f\circ f \circ\cdots\circ f}_{\text{n times}}$。

数学上的了解到这里就足够了，我们不会涉及更深入的Lambda Calculus的内容。

首先，我们知道Python的声明函数如下：

1
2
3

def test():
    print('Hello, Python!')
    return

几乎在所有语言中，我们的函数都是这么声明的。这么声明之后，假设当前的test函数是一个object，那么实际上我们是把这个object绑定到了test上。

这是声明了一个有名函数。那么有名自然就可以对应匿名函数，也就是Lambda Expression。

让我们来看一下Lambda Expression的语法：

1
2
3

add = lambda x: lambda y: x + y
# or
add = lambda x, y: x + y

我们看到，一个匿名函数不需要def的语法块，直接使用lambda引起即可，后面跟着参数列表，用一个冒号:分割函数体和参数部分。上面的两个函数都被我绑定在了add这个名字上，实际上使用的时候并不需要，例如：

1

sorted([1, 8, 3, 19, 3 ** 6], cmp=lambda x, y: x < y)

cmp需要一个函数，用于比较两个参数，这里我直接使用了一个Lambda Expression来代替。

之后我们需要讨论闭包的问题。什么是一个闭包？看下面代码：

1
2
3
4
5
6
7
8

def outer(x):
    
    def inner():
        return x
    
    return inner

# outer(15)() ==> 15

这就是一个闭包。一个闭包实际上可以看做一个内部函数，这个内部函数捕获了外部变量。上面的inner函数中，x并不属于它，但是我们调用outer(15)以后返回的这个inner能拿到15，也就是说，内部的inner捕获了外部的x，然后再把x返回了回来。

理解了闭包和Lambda Expression之后，我们就可以开始我们的邱奇计数之旅了。

0x01. 零(zero)和后继函数(succ)

现在就到了正式的邱奇计数环节了！

让我们首先考虑一下皮亚诺公理的几条内容：

I. 0是自然数

……

设S(n)为数n的后继，则

VI. 对任意自然数n，S(n)为自然数

……

从这里我们可以知道：自然数系统的其中两个基础是$0$和后继的定义，所以我们的邱奇计数也需要从$0$和后继开始定义。

在皮亚诺公理系统中，后继就是这个数$+1$。例如$0$的后继就是$0+1=1$，$279$的后继就是$279+1=280$。也就是说，我们需要找到一种办法来描述“后一个”这个关系。

在邱奇计数中，邱奇选择了一种十分聪明的表达方式：函数的复合。什么意思呢？就是函数$f$应用$k$次表达的是自然数$k$。那么这样实际上表达一个数的后继就十分简单了：我们再应用一次函数$f$。

也就是说，假如有$k=f^k=\underbrace{f\circ f \circ\cdots\circ f}_{\text{k times}}$，那么$k+1$实际上就是$f\ (f^k) = f^{k+1}=\underbrace{f\circ f \circ\cdots\circ f}_{\text{k+1 times}}$。

解决了后继的问题，再来考虑$0$的问题。我们从上面应用的角度考虑：$0$意味着函数应用的次数为$0$次，那也就是说，无论我们给什么函数$f$，$0$始终返回来一个和$f$无关的值。$f$本身需要一个参数，那么……我们直接把这个参数返回回来即可！

这样的表达方法下，每一个数都是一个高阶函数，接受了一个函数$f$和一个数$x$作为参数。

那么，我们的表达就很简单了，首先是$0=\lambda f.\lambda x.x$，这是一个接受一个函数$f$和一个参数$x$的高阶函数，返回$x$本身。其次，一个数的后继就是在其身上再调用一次$f$，例如$1=\lambda f.\lambda x.f\ x$，$2=\lambda f.\lambda x.f\ (f\ x)$。

下面这个表就是邱奇计数的一个简单表示总结：

那么，零的代码就很简单了：

1

zero  = lambda f: lambda x: x

这样我们就把$0$表达了出来。

现在我们来考虑后继。后继根据上面的讨论，实际上我们就是在外层套上一个f即可。

怎么套呢？我们考虑f的作用对象，考虑$2$：$\lambda f.\lambda x.f\ (f\ x)$，里面的$f\ x$实际上就是$1$，所以就$2$是$f\ 1$。从这一步我们知道，f的作用对象是上一个数，所以，后继函数是如下的表达：$\text{succ}\ n =\lambda f.\lambda x.f\ n$。

转换成代码其实就是很简单的一行：

1

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

这样我们的后继函数就表达完了。

两个简单函数，就能把整个邱奇计数法的基础表示出来了。

0x02. 邱奇化(toChurch)与去邱奇化(unChurch)

上一节讨论了如何表示$0$和后继，这一节考虑一个问题，我们怎么获得一个邱奇化的数呢？

首先很简单，假如要把$0$邱奇化，我们直接返回zero即可，也就是说：

1

toChurch = lambda x: zero if x == 0

接下来呢？

考虑这么一个情况：$0$的后继是$1$，$2$的后继是$1$。那假如我们需要获得$2$，我们其实只需要获得$1$的后继即可，而需要获得$1$，我们只需要获得$0$的后继即可。

这个情况其实很明确，就是一个简单的递归，从$2$递减到$0$即可，那么toChurch就十分简单了：

1

toChurch = lambda x: zero if x == 0 else succ(toChurch(n - 1))

假如遇到了$0$我们就返回$0$，否则返回$n-1$的后继。代码十分清晰。

邱奇化解决了，接下来我们讨论去邱奇化。

实际上我们考虑两个映射：

• $0$的映射：自然数：$0$；邱奇计数：$\lambda f.\lambda x.x$
• 后继的映射：自然数：$+1$；邱奇计数：$\text{succ}\ n =\lambda f.\lambda x.f\ n$。

那么互转怎么办？我们用$0$来代替邱奇计数的$0$，用$+1$来代替邱奇计数的后继函数。

$0$代替$0$并不难，直接让$x=0$即可，而$0$的后继就是在$0$的基础上应用$+1$这个函数即可，所以我们直接令$f=\lambda m.m+1$。那么这样我们就构造出了unChurch的过程：$\text{unChurch n} = n\ (\lambda m.m+1)\ 0$。

Python代码也就容易得到了：

1

unChurch = lambda n: n(lambda x: x + 1)(0)

到这里，我们邱奇化和去邱奇化都解决了。我们来试试如下的代码：

1
2

unChurch(zero) // ==> 0
unChurch(toChurch(198)) // ==> 198

成功啦 :)。

第一篇就到这里。

相信你到这里已经见识到了邱奇计数法的威力：我们并没有使用任何数或者数据结构，只使用了最简单的高阶函数和参数抽象出了完整的自然数表示法，根据一定变换可以和自然数进行互相的转换。

但是，作为一个自然数系统，不能运算有什么作用呢？

下一节，让我们来分析三个重要但是基础的运算：加、乘和幂运算。与此同时，我还将提到如何使用代换模型来讨论函数的展开形式。

本节Quiz答案如下：

本节的所有代码如下：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

zero = lambda f: lambda x: x
succ = lambda n: lambda f: lambda x: f(n(f)(x))

unChurch = lambda n: n(lambda x: x + 1)(0)
toChurch = lambda n: zero if n == 0 else succ(toChurch(n - 1))
# tail recursive
# tcHelper = lambda n, m: m if n == 0 else tcHelper(n - 1, succ(m))
# toChurch = lambda n: tcHelper(n, zero)

def main():
    """
    Test wrapper

    1. zero and succ
    >>> unChurch(zero)
    0
    >>> unChurch(succ(succ(zero)))
    2

    2. unChurch and toChurch
    >>> unChurch(toChurch(0))
    0
    >>> unChurch(toChurch(198))
    198
    """

if __name__ == "__main__":
    import doctest
    doctest.testmod(verbose=True)