让我们来谈谈抽象。

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

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

这一系列短文有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}}$。

Quiz 1

$\lambda f. \lambda x.f(x)$是什么意思?

数学上的了解到这里就足够了,我们不会涉及更深入的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之后,我们就可以开始我们的邱奇计数之旅了。

Quiz 2

上面两种`add`的调用方式有区别吗?有什么区别?为什么?

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)$。

Quiz 3

$4$用邱奇计数怎么表达?

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

邱奇计数
$0$ $\lambda f.\lambda x.x$
$1$ $\lambda f.\lambda x.f\ x$
$2$ $\lambda f.\lambda x.f\ (f\ x)$
$3$ $\lambda f.\lambda x.f\ (f\ (f\ x))$
$\cdots$ $\cdots$
$n$ $\lambda f.\lambda x.f^n\ 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))

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

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

Quiz 4

用Python代码写出来$4$的邱奇表示法。如果用`succ`表达呢?

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$的后继。代码十分清晰。

Quiz 5

尝试把`toChurch`改写成尾递归的版本。

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

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

  • $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 6

如果我把`unChurch`定义成:`unChurch = lambda n: n(lambda x: x * x)(1)`,那么`unChurch(toChurch(100))`会得到什么结果?解释你的结果。

第一篇就到这里。

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

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

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

本节Quiz答案如下:

答案

  1. $\lambda f. \lambda x.f(x)$是什么意思?

    这个表达式接受两个参数,一个是函数$f$,一个是数$x$,返回把$x$应用到函数$f$上的结果。

  2. 上面两种add的调用方式有区别吗?有什么区别?为什么?
    有区别,第一种的调用方式是:add(2)(4),第二种的调用方式是:add(2, 4)。 区别产生的原因是这样,我们考虑第一种表达:

    1
    
    add = lambda x: lambda y: x + y

    这里面是两个嵌套的Lambda Expression,第一个是一个参数为x的匿名函数,这个函数内部又是一个匿名函数,内部的匿名函数捕获了外部的自由变量x,然后返回它加y的结果。

    第二个则是一个有两个参数的匿名函数,和普通的函数一样。

  3. $4$用邱奇计数怎么表达?

    $4=\lambda f.\lambda x.f\ (f\ (f\ (f\ x)))$

  4. 用Python代码写出来$4$的邱奇表示法。如果用succ表达呢?

    1
    2
    3
    
    four = lambda f: lambda x: f(f(f(f(x))))
    # 使用succ
    four = succ(succ(succ(succ(zero))))
  5. 尝试把toChurch改写成尾递归的版本。

    1
    2
    
    tcHelper = lambda n, m: m if n == 0 else tcHelper(n - 1, succ(m))
    toChurch = lambda n: tcHelper(n, zero)
  6. 如果我把unChurch定义成:unChurch = lambda n: n(lambda x: x * x)(1),那么unChurch(toChurch(100))会得到什么结果?解释你的结果。

    结果其实很简单,是1。这里考虑一个问题:x是多少?我们考虑2的情况,展开得到:

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

    我们把它应用进去以后得到:

    1
    2
    3
    4
    5
    6
    7
    8
    9
    
    (lambda x: x * x)((lambda x: x * x)(1))
    # ==>
    (lambda x: x * x)(1 * 1)
    # ==>
    (lambda x: x * x)(1)
    # ==>
    (1 * 1)
    # ==>
    1

    可以看到,即使是多次调用,总是返回$1\times1$,所以无论$f$复合多少次都只会返回1

本节的所有代码如下:

 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)