church pairs

Question

SICP 的练习 2.4 提到了一种构造 pair 的方法以及相应的选择函数（cons, car, cdr），见下面的地址

[url:][看第8楼]。

虽然没有明说，但该习题实际上介绍了所谓的 church pair，即用 lambda 表达式来表示 pari. 在本贴中，我将更详细地说明 church pair, 并在此基础上给出列表的构造。

[ 本帖最后由 win_hate 于 2008-10-26 13:34 编辑 ]

Answer 1

完整代码

2. #lang lazy
4. (define (CONS x y)
5.   (lambda (f) (f x y)))
7. (define (TURE x y) x)
8. (define (FALSE x y) y)
10. (define (CAR pair)
11.   (pair TURE))
13. (define (CDR pair)
14.   (pair FALSE))
16. (define NIL
17.   (lambda (x) TURE))
19. (define (NULL? l)
20.   (l (lambda (x y)
21.        ((lambda (y) FALSE) y))))
23. (define (SUM xs)
24.   ((NULL? xs) 0 (+ (CAR xs) (SUM (CDR xs)))))

复制代码

Answer 2

把 pair 定义为一个 lambda 表达式：λxyf . fxy，或 λxy . λf . fxy

即构造出来的 x,y 被包在 lambda 表达式中。这个表达式将作用在一个选择函数 f 上，f 从中选出 x 或 y.

所以我们有如下的 CONS 代码（in Scheme）

2. (define (CONS x y)
3.   (lambda (f) (f x y)))

复制代码

在 Scheme 中，不能定义一个带 3 个参数的函数，并作用在 2 个参数上，返回一个单参函数。即在语法上不支持直接 currying，而 Haskell 是支持的。

显然 CAR 应被定义为选取第一个参数，而 CDR 选取第二个参数。可见，CAR, CDR 可以用 church booleans TRUE 和 FALSE 来实现。church booleans 见下面的地址：

[url:][church booleans].

所以有如下代码

2. (define (TURE x y) x)
3. (define (FALSE x y) y)
5. (define (CAR pair)
6.   (pair TURE))
8. (define (CDR pair)
9.   (pair FALSE))

复制代码

看效果：

2. > (define foo (CONS 1 2))
3. > (CAR foo)
4. 1
5. > (CDR foo)
6. 2
7. >

复制代码

如果要在 CONS, CAR, CDR 的基础上构造出 list，我们还需要 NIL，以及相应的谓词 NULL?

先考虑 NULL?，设 NULL? 构造一个选择函数 f，让 pair 作用在其上

pari = (λ.xy) xy
NULL?=λ p. pf

NULL? pair = pair f = f x y = FALSE

所以 NULL? 也许可以定义为： λz . z(λxy. FALSE)

这个 lambda 表达式对 church pair 是返回 FALSE 了，NIL 应该设计成使得 NULL? 返回 TRUE

NULL? NIL = NIL f = TRUE

所以 NIL 可以定义为: λx . TRUE.

相应的 scheme 代码：

2. (define NIL
3.   (lambda (x) TURE))
5. (define (NULL? l)
6.   (l (lambda (x y)
7.        ((lambda (y) FALSE) y))))

复制代码

NULL? 也可以简单写为

2. (define (NULL? l)
3.   (l (lambda (x y)
4.        FALSE)))

复制代码

复杂的写法是为了在 scheme 中与 lambda 表达式保持一致。

效果：

2. > NIL
3. #<procedure NIL (x)>
4. > (NULL? NIL)
5. #<procedure TURE (x y)>
6. > (NULL? (CONS 1 2))
7. #<procedure FALSE (x y)>
8. > ((NULL? NIL) #t #f)
9. #t
10. > ((NULL? (CONS 1 2)) #t #f)
11. #f

复制代码

有了 NIL，我们就可以构造出 list 了。下面是一个对列表求和的小程序。由于要求 TRUE, FLASE 有 "短路" 效果(对参数延迟求值)，所以使用了 Lazy Scheme

2. (define (SUM xs)
3.   ((NULL? xs) 0 (+ (CAR xs) (SUM (CDR xs)))))

复制代码

效果：

2. > (SUM (CONS 1 (CONS 2 (CONS 3 NIL))))
3. 6
4. >

复制代码

在 lambda 表达式中，CONS, CAR, CDR 一般称为 PAIR, FIRST, SECOND。Haskell 的记号跟 lambda 表达式是一致的。

[ 本帖最后由 win_hate 于 2008-10-26 14:07 编辑 ]