忙过了这一茬,趁着下一茬还没来,我先填填坑~

上一篇文章里面,我们谈到了如何去表达一个自然数系统:0以及后继,然后写出了邱奇计数法中的0和后继表达方式。作为一种验证和转化手段,我们也描述了邱奇化和去邱奇化的有关内容,更好的去验证我们的结果。

然而,一个代数系统,光有数可远远不够,我们还需要有各种运算。

今天,让我们来谈谈运算的内容,除了加法、乘法、乘方以外,我还将给你展示使用代换模型来展开函数,从而去更好的理解整个运算过程。

准备好了吗?让我们开始吧!

0x03. 从后继谈起

我们在上一篇文章已经提到了后继,所谓的后继,就是一个数的后一个数,比如$2$的后继是$3$。从这里其实很容易得到一个想法,我们假如要在$m$上加上$n$,我们只需要在$n$上应用$m$次后继即可呀。而我们考虑$m$的意义:应用$m$次$f$函数……对!我们把这个$f$换成$\text{succ}$不就可以了!

所以,我们这里很容易推到得出这个式子:$n+m=m\ \text{succ}\ n$。

那我们就可以写出这样的函数:

1
add = lambda n, lambda m: m(succ)(n)

你可以看到,我们的模型很巧妙,我们对$m$应用$\text{succ}$和$n$,那么$n$上原来有$n$次$\text{succ}$,现在再应用了$m$次$\text{succ}$,正好就是$m+n$次!

这是加法最简单,最容易理解的实现。然而,这个实现不容易帮我们理解,到底内部做了什么,而当我们知道了准确的应用过程,我们才能更好的推断乘法和乘方。

Quiz 1

解释使用add(zero, zero)时会发生什么,为什么会得到$0$?

0x04. 加法

那现在让我们抛弃$\text{succ}$,我们直接从$m$和$n$推导加法。说的很壮观,其实也不难:我们只需要知道加法到底做了什么即可。

首先我们考虑$n$的含义。假设现在我有一个$f$和$x$,然后应用得到$n\ f\ x$,那么实际上我得到了一个。那么我们就考虑,所谓的邱奇计数,是在$x$上应用多次$f$,那么现在假如我想对这个新的数再应用多次怎么办?我们会产生如下调用:$m\ f\ (n\ f\ x)$。这样下来,我们就对这个数又应用了$m$次$f$,实际上$f$应用了几次?$n+m$!

对,加法模型的推导就是如此的直观,我们首先把$n$应用到最终结果得到$n$这个数,然后再在$n$这个数上应用多次$m$,我们就得到了$n+m$。

从这个角度,我们可以得到如下这个式子:$n+m=\lambda f.\lambda x.m\ f\ (n\ f\ x)$。一切都是那么的直观。

那么我们也就很容易写出这样的函数了:

1
add = lambda n, m: lambda f: lambda x: m(f)(n(f)(x))

让我们掉过头来,再从$\text{succ}$的角度看我们新推导的这个式子:

首先我们有$n+m=m\ \text{succ}\ n$,展开得到:$n+m=\underbrace{\text{succ}(\cdots(\text{succ}\ n)\cdots)}_{\text{m times}}$。而我们又知道$\text{succ}\ n=\lambda f.\lambda x. f\ n$,我们代换到前一个式子,我们可以得到$n+m=\underbrace{\lambda f.\lambda x. f(\cdots(\lambda f.\lambda x. f\ n)\cdots)}_{\text{m times}}$,我们把外侧的$m$个$\lambda f.\lambda x.f$合并,就得到了$n+m=\lambda f.\lambda x.m\ f\ (n\ f\ x)$。

你看,我们使用代换模型展开使用后继的加法后,实际上得到的是与我们推导的不使用后继的加法等价的。

让我们试试使用Python代码展开$1+2$。

我们很容易得到$1$和$2$:

1
2
one = lambda f: lambda x: f(x)
two = lambda f: lambda x: f(f(x))

接下来,我们调用add(one, two)。首先,我们把二者带入进去,得到:

1
lambda f: lambda x: two(f)(one(f)(x))

然后我们先展开two(直接在对应位置上用展开式替换two即可):

1
lambda f: lambda x: (lambda x: f(f(x)))(one(f)(x))

现在展开one就简单许多:

1
lambda f: lambda x: (lambda x: f(f(x)))((lambda x: f(x))(x))

仔细数一数,刚好是三层调用 :)。

Quiz 2

写出add(two, three)的Python代码展开,其中two = succ(succ(zero))three = succ(two)

0x05. 乘法

加法之后,让我们来看看乘法。

所谓的乘法其实很简单,我们多次应用加法即可。但是这里存在一个问题,我们怎么确定加法的界限?我们的$n$,$m$是邱奇数,我们并没有很好的直接比较的方法,不管怎么写都不好写。

让我们来看看邱奇数本身。首先,讨论一个一般的邱奇数$n$,展开它,$n=\lambda f.\lambda x.f\ x$(我们就先假设$n=1$吧。)在这里面,$f$是一个函数,$x$是一个数,它的意义是我们把$f$应用一次在$x$上。在上面的加法中,我们把$x$换成了我们换成了其中的一个数,完成一步代换。

我们重点思考这么一个描述:把$f$应用一次在$x$上。对于更一般的邱奇数$n$,我们邱奇数的表达方法实际上是应用了$n$次$f$。我们现在掉头回来考虑乘法:我们的乘法是怎么回事呢?考虑$n\times m$,我们实际上是应用$m$次原数加上$n$……

这两个描述是一致的!也就是说,我们所谓的乘法,就是在原数的外侧套上多次$f$的过程。我们现在可以看到,所谓的$m\ f\ x$是把$f$应用$m$次到$x$上,那如果我们要$n\times m$呢,我们只需要在$x$上应用$m$次$n$即可!

经过这一番推导,我们可以得到这样的展开式:$n\times n =\lambda f.\lambda x. m\ (n \ f)\ x$。 这个式子是很好理解的:我们首先应用$n$次$f$,把这个看成一组,再应用$m$组,就是$n\times m$。

那这样,我们的mult函数也就十分容易了:

1
mult = lambda n, m: lambda f: lambda x: m(n(f))(x)

这里面我们稍微讨论一下每一个的类型:我们的n接受两个参数,目前我们只应用了一个,所以n(f)是一个签名类似于这样的函数:lambda x:……,这个函数的签名完全适合m的需要(复习:f是一个只接受单参数的函数),然后代换下来,每一个的函数签名都需要x,可以正确的应用下去。下面的展开也将展示这一点。

接下来让我们展开$1\times2$的Python代码。

我们直接调用mult(one, two)吧:

1
lambda f: lambda x: two(one(f))(x)

接下来,我们先展开one

1
lambda f: lambda x: two((lambda x: f(x))(x)

然后展开two

1
lambda f: lambda x: (lambda f: lambda x: f(f(x)))(lambda x: f(x))(x)

这个式子可能比较难理解,因为我把f应用到了one上但是没有把展开后的one应用到two上,其实这个式子本身表达的还是$m\ f\ x$。乘法的式子我们再做深入展开就会显得很复杂,而且冗余部分太多,所以我展开到这里就结束了。

Quiz 3

写出mult(two, three)的Python代码展开,其中two = succ(succ(zero))three = succ(two)

0x06. 乘方

我们先回味一下上面两个运算:加法,我们把数应用到了$x$上,乘法,我们把函数应用到了$f$上。我们还能应用什么?

让我们再突破一次极限吧。

首先考虑乘方运算本身:$n^m$,我们是把乘以$n$应用$m$次。计数吗?我们上一节讨论过,并不是很可行。

我们现在再度考察我们的乘法:$n\times m=\lambda f.\lambda x. m\ (n \ f)\ x$。我们这里是应用了$m$次$n$,实际上是应用了$m$次$n\ f$。那么,假如说,我们单独应用$m$次$n$呢?不行,不行。为什么?$n$是一个接受两个参数的函数,$m$的$f$参数是接受一个参数的函数,这连类型都不符合怎么可能能应用呢?

现在清空一下你的大脑,我们重新讨论$f$和$x$。

在这之前我说过,$f$是一个接受单参数的函数,$x$呢是一个数,我们的邱奇计数表达的是$x$嵌套应用到$f$上的过程。这句话隐含的内容是,$f$有一个参数位,$x$没有参数位。但是我们考虑其中的这一个情况,假如说$f$有两个参数位,$x$有一个参数位呢?$x$会被应用到$f$的第一个参数位上,然后返回一个什么?返回一个新的函数!这是一个接受一个参数的函数。这个参数应用到哪儿了?$f$的第二个参数位上!

这就是函数作为一级对象的另一个抽象武器:函数作为返回值。之前我们讨论的函数作为参数我们用了许多:邱奇数本身就是个函数。然而,在之前的运算中,我都或多或少的略过了函数作为返回值的内容,因为运算返回邱奇数都是返回了一个函数。为什么这里要提?因为这一条将作为我们最强大的武器去解决乘方运算。

乘方运算难度并不高,我们的关键是在要了解清楚整个流程。根据上面的讨论,我们的$f$、$x$都可以是函数,那么我们考虑这么一个应用:我们首先单独把$n$应用到$m$的$f$上,这里得到了应用$m$次$n$,也就是$m\ n$,这里我们就会对之后的内容应用$m$次$n$。接下来我们考虑,我们对$f$应用一次$n$,得到的是$n\ f$,那就是$n$,应用两次呢?$n\ (n\ f)$,这个模型应该是很眼熟了(如果我们把$x$应用上去就是$n\ (n\ f)\ x$),是我们的乘法模型,得到的是$n\times n=n^2$。那也就是说,我们对$f$应用了多少次$n$,就是$n$的多少次方,那么,应用$m$次就是……$n^m$!我们再看上面那个式子,可以看到,我们的应用对象是$f$,也就是说,这里我们的$f’=n,x’=f$。所以说,我们有了内部的应用:$m\ n\ f$,它的含义就是我们对$f$应用$m$次$n$。还没有结束,$n$是一个双参数函数,$f$是一个单参数函数,应用结束后返回了一个需要一个参数的函数,所以我们需要再应用一个数上去,我们上面什么没用?$x$!我们把$x$应用进去即可:$(m\ n\ f)\ x$。

所以,我们的乘方就是这么一个式子:$n^m=\lambda f.\lambda x.(m\ n\ f)\ x$。

写成Python的函数就是这样了:

1
2
3
4
cpow = lambda n, m: lambda f: lambda x: (m(n)(f))(x)
# pow是一个内置函数,避免重名
# 我们也可以这么写, 去掉那个多余的括号
# cpow = lambda n, m: lambda f: lambda x: m(n)(f)(x)

来,惯例让我们展开$1^2$。

我们也是直接调用cpow(one, two)

1
lambda f: lambda x: (two(one)(f))(x)

依据国际惯例,我们还是先展开one

1
lambda f: lambda x: (two(lambda f: lambda x: f(x))(f))(x)

最后展开two

1
lambda f: lambda x: ((lambda f: lambda x: f(f(x)))(lambda f: lambda x: f(x))(f))(x)

结束了。这个展开式的签名和我们期待的一样:当我们逐步应用进去后,前面刚好缺一个参数x,然后我们紧接着就有一步应用,完成了整个乘方过程。

Quiz 4

写出cpow(two, three)的Python代码展开,其中two = succ(succ(zero))three = succ(two)


我们这一次的内容就到这里。

相信你再一次被邱奇计数所震撼:我们从最简单的后继开始,展开得到加法,然后不断推进运算中$n$所在的位置,从在$n$外侧套上$m$次$f$调用,到$m$次调用$n\ f$,再到$m$调用$n$,一步步把答案往更高层次推进。

在这个推进过程中,我们一次次突破了我们心目中的抽象极限:先是使用一个并不存在的数(应用时还没有被求值)去替换了$m$的$x$调用,然后使用邱奇数这个函数本身去替换了$m$的$f$调用,到最后,我们甚至部分应用了$m$,仅仅使用没有调用$f$的$n$去替代$f_m$。这一个个过程,依赖于函数作为一级对象。邱奇数是逻辑意义上的数,程序意义上的函数,我们把邱奇数(函数)作为一级对象,获得的是远比基础数据类型作为一级对象更加强大的抽象能力。

本节你看到了lambda表示法和函数作为一级对象带来的强大抽象能力。事实上,这二者的结合远比你想象中的更强大,这一部分稍后有机会我们再讨论。

在本节,我还对每个运算使用代换模型进行展开,这是一个洞悉函数内部运算过程和机理的很有力的手段,在算法分析过程中也十分重要。每一块的习题都要求你使用代换模型展开我们的式子,不知道你是否对这个工具稍稍熟悉了?

下一篇文章,也就是这系列短文的终结,让我们回归lambda表示法的本源,数学,从数学推导和函数应用来探讨前驱与减法。如果有机会,我们还可以展望一下Scott Encoding以及邱奇计数的本质。

之后再见了!

本节Quiz的答案如下:

答案
  1. 解释使用add(zero, zero)时会发生什么,为什么会得到$0$?

    这一条的解释十分简单,我们调用这条以后会得到的是如下形式:zero(succ)(zero),你可以发现,由于在zero中,f并没有任何作用,所以后面的zero根本就没有调用上succ,然后我们再调用zero,那自然而然就是$0$了。

  2. 写出add(two, three)的Python代码展开,其中two = succ(succ(zero))three = succ(two)

    1
    
    lambda f: lambda x: ((lambda x: f(f(x)))((lambda x: f(f(f(x))))(x)))
    1. 写出mult(two, three)的Python代码展开,其中two = succ(succ(zero))three = succ(two)
    1
    
    lambda f: lambda x: (lambda f: lambda x: f(f(x)))(lambda x: f(f(f(x))))(x)
  3. 写出cpow(two, three)的Python代码展开,其中two = succ(succ(zero))three = succ(two)

    1
    
    lambda f: lambda x: ((lambda f: lambda x: f(f(f(x))))(lambda f: lambda x: f(f(x))))(f)(x)

本节的所有代码如下(包含上节):

 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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
zero = lambda f: lambda x: x
one = lambda f: lambda x: f(x)
succ = lambda n: lambda f: lambda x: f(n(f)(x))

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

# add(two, three)
# using succ: add = lambda n, m: m(succ)(n)
add = lambda n, m: lambda f: lambda x: m(f)(n(f)(x))
mult = lambda n, m: lambda f: lambda x: m(n(f))(x)
cpow = lambda n, m: lambda f: lambda x: (m(n)(f))(x)


def main():
    """
    Test wrapper.
    The test of Church numeral.

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

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

    3. add
    >>> unChurch(add(zero, zero)) == 0 + 0
    True
    >>> unChurch(add(toChurch(195),toChurch(267))) == 195 + 267
    True

    4. mult
    >>> unChurch(mult(zero, zero)) == 0 * 0
    True
    >>> unChurch(mult(toChurch(195), toChurch(233))) == 195 * 233
    True

    5. cpow
    >>> unChurch(cpow(zero, zero)) == 0 ** 0
    True
    >>> unChurch(cpow(toChurch(6),toChurch(7))) == 6 ** 7
    True
    """


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