最近在看SICP,然后看到练习2.6,十分的有趣,刚好和上学期计科导讲过的自然数的构造有点类似。题目首先给了0和加一的实现,然后问1和2应该怎么直接定义,再问如何直接定义加法。

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

one, two

一开始问我1和2是怎么直接定义的,我是拒绝回答的,因为我根本看不懂这是什么东西。不妨先仔细看下给的两个东西是什么。

zero 是一个接受一个参数 f 的函数,调用(zero f)会生成一个函数,这个函数接受一个参数 x 并且直接返回这个参数 x ,即执行了0次函数 f。也就是说 (zero f) 实际上就是一个 id 的函数。也就是说,Church Number实际上是一个(接受一个函数然后)生成函数的函数。

add-1 接受一个 Church Number n,比如zero,注意到这实际上是一个函数。然后我们用个lambda表达式把这个Church Number具体化成为 (n f)。对于函数 (n f) 来说,它接受一个参数,然后对这个参数执行若干次f。因此,add-1就是一个生成函数的函数,它生成一个函数,这个函数对执行完若干次f之后x的值再执行一次f

所以说我们大概可以这么理解这里定义的 Church Number num,如果这里定义的 num 和自然数当中的 n 等价,那么

((num f) x) = (f (f (f ... (f x))))

也就是对 xnf

那么好了,我们很容易的根据这个含义可以写出 onetwo 甚至是 three 了,这和我们直接从 add-1 展开的结果是一样的:

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))
(define three (lambda (f) (lambda (x) (f (f (f x))))))

具体的例子

首先我们只有两个东西:0元素 \(0\) 以及后继操作符 \(+(\cdot)\) 。如果应用在自然数上那么就有

如果我们定义一个0为一个空字符串,定义后继函数为在字符串后面加上一个#,那么我们就会有

用 scheme 代码来表达上面两个后继函数就是:

(define (inc n) (+ n 1))
(define (append-# s) (string-append s "#"))

那么我们下面的结果:

((three inc) 0)        ; 3
((three append-#) "")  ; "###"

这是个很神奇的结果,因为 3 代表了3,而同时 ### 也代表了3!

加法

怎么从定义出发写出一个加法的函数呢?首先,根据前面的这些函数,我们可以猜到,add肯定也是一个生成函数的函数,而且具有如下的形式:

(define (add a b)
  (lambda (f)
    (lambda (x)
     ...)))

这个函数怎么写呢?按照前面那个直白的理解,如果令 c(add a b),那么 ((c f) x) 就是要对 x 执行 a+bf。这其实等同于:令 yx 执行了 af 的结果,那么 ((c f) x) 就是再对 y 执行 bf 的结果。

跟着这个感觉,可以写出来

(define (add a b)
  (lambda (f)
    (lambda (x)
      ((b f) ((a f) x)))))

实际上运行起来也是完全没有问题的

(define five (add two three))
((five inc) 0)         ; 3
((five append-#) "")   ; "#####"

乘法?

好了,书上的练习结束了,不过我突然想到了乘法。乘法怎么根据定义来弄呢?当然还是先套上前面的形式,但是里面应该是什么呢?

回想刚才的加法,我们用了一个 y 来表示做了 af 之后的 x,于是我们只需要再对 ybf 就可以了。那我们现在想要什么?

如果我们现在有一个函数 g ,它是 fa 次复合,也就是 (g x) 等同于 (f (f (f ... (f x)))) 。那么令 c(mul a b) ,那么 ((c f) x) 就是对 xbg 函数,也就是 ((b g) x)

所以就可以得到乘法的实现

(define (mul a b)
  (lambda (f)
    (lambda (x)
      ((b (a f)) x))))

可以发现乘法和加法很像,几乎就是换了下括号的位置!当然,运行起来也是很愉快的

(define fifteen (mul five three))
((fifteen inc) 0)         ; 15
((fifteen append-#) "")   ; "###############"

写到这里,我对 Church Number 又有了个更形象的认识:前面说到 ((num f) x) = (f (f (f ... (f x)))) 这是从具体的求值的角度来理解的。那么 (num f) 呢?不正好就是 fn 次复合吗!这是从函数的角度来理解的。

Have Fun!

于是我们可以写出 Church Number 和自然数以及#串相互转换的函数

(define (int->church n)
  (if (= n 0)
      zero
      (add-1 (int->church (dec n)))))
(define (church->int num)
  ((num inc) 0))
(define (church-># num)
  ((num append-#) ""))

(define sixteen (int->church 16))
(church->int sixteen)

试一下

(church-># sixteen)    ; "################"
(church->int sixteen)  ; 16

嗯,我已经服气了!