丘奇数
来自sicp练习2.6,题目是这样说的:
在一个可以对过程进行各种操作的语言里,我们可以完全没有数(至少在只考虑非负整数的情况下),可以将0和加一操作实现为:
(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
(λ(f)
(λ(x)
(f ((n f) x)))))
这一表示形式称为Church计数,名字来源于其发明人数理逻辑学家Alonzo Church (丘奇),λ演算也是他发明的.
请直接定义one和two(不用zero和add-1)(提示:利用代换去求值(add-1 zero)).请给出加法过程 + 的一个直接定义(不要通过反复应用add-1)
在做题之前,先来看看其他用λ算子的有趣实现.
1.表示布尔值
(define true
(λ (x)
(λ (y) x)))
(define false
(λ (x)
(λ (y) y)))
(define if
(λ (v)
(λ (t)
(λ (f) ((v t) f)))))
true是一个接受一个参数x的函数.此函数返回一个接受参数y的函数.此函数返回true接受的参数x.
现在我们希望 (if true 1 0) 返回1,来看下是不是这样的.归约过程如下:
(((if true)1)0)
((((λ (v)
(λ (t)
(λ (f)
((v t) f))))
(λ (x)
(λ (y) x)))1)0)
(((λ (t)
(λ (f)
(((λ (x)
(λ (y) x)) t) f)))1)0)
(((λ (x)
(λ (y) x))
1) 0)
((λ (y) 1)0)
1
应用(λ (v) (λ (t) (λ (f) ((v t) f)))) == (λ (v t f)((v t) f))
if可以简写为:
(define if
(λ (v t f)
((v t) f)))
这样就可以直接用 (if true 1 0) 而不是 (((if true)1)0) 了.
2.表示序对
用过程表示序对在sicp里已经有了.这里是另一个版本.
(define mkpair
(λ (x)
(λ (y)
(λ (s)
((s x) y)))))
(define fst
(λ(p)
(p true)))
(define snd
(λ(p)
(p false)))
调用:
> (fst ((mkpair 1) 2)) 1
3.现在来看丘奇数
已经定义了zero和add-1,那么我们希望(add-1 zero)就能得到one的第一定义:
(add-1 zero)
(add-1 (λ(f)
(λ(x) x)))
;α relation:
;different name means nothing
((λ(n)
(λ(f)
(λ(x)
(f ((n f) x)))))
(λ(b)
(λ(a) a)))
(λ(f)
(λ(x)
(f
(((λ(b)
(λ(a) a)) f) x))))
(λ(f)
(λ(x)
(f
((λ(a) a) x))))
(λ(f)
(λ(x)
(f x)))
那么one的定义就是:
(define one
(λ(f)
(λ(x)
(f x))))
同理,two的定义就是:
(define two
(λ(f)
(λ (x)
(f (f x)))))
由此可见.丘奇数中的数字n就是一个以一个函数f为参数的一个高阶函数.它返回一个函数,此函数有一个参数x,它将f作用在x上n次.
由此,add接受两个丘奇数n和m.返回的丘奇数n+m是将f作用于x上n+m次的函数,由此.可将add定义如下:
(define add
(λ(m)
(λ(n)
(λ(f)
(λ(x)
???)))))
现在来做填空题了.先来观察题目中已经定义的add-1:
(define (add-1 n)
(λ(f)
(λ(x)
(f ((n f) x)))))
其中的((n f) x)得到的是什么?回想n的定义是将f作用于x n次,那么((n f) x)得到的就是将f作用于x n次后的值.
那么(f ((n f) x))就是将得到的这个值在作用一次f,而f和x都是不知道的,因为它们是函数的参数.如此就得到了n+1的定义.
那么add中的问号就应该是得到f作用于x n次后的值.再将这个值当作x,并它作用m次f,于是,add的定义得到:
(define add
(λ(m)
(λ(n)
(λ(f)
(λ(x)
((m f)
((n f) x)))))))
验证下:
> ((((add one) two) add1) 4) 7
正确~
可以得到乘法mult和sub-1的定义.mult接受m和n,将(n f)作为新的f,并传入m.sub-1则是先判断n是不是0,是则返回0,否则返回n-1.
(define mult
(λ(m)
(λ(n)
(λ(f)
(m(n f))))))
(define sub1
(λ(n)
(λ(f)
(λ(x)
(((n (λ(g)
(λ(h)
(h (g f)))))
(λ(u)
x))
(λ(u)
u))))))
参考:
