SICP 読み (14)

Church 数って知りませなんだ。以下、インターネットなカンペの元に。

問題 2.6

これはこれは。

以下、問題に出ている手続き。

(define zero (lambda (f) (lambda (x) x)))

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

ヒントの通り、(add-1 zero) を机上で評価し (置き換え) てみる。

(add-1 zero)

(add-1 (lambda (f) (lambda (x) x)))

(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) x)) f) x))))

;; (((lambda (f) (lambda (x) x)) f) x) は x 返却ですな
(lambda (f) (lambda (x) (f x)))

zero は微妙なので add-1 から置き換えてみるとどうなるか。

(add-1 zero)

(lambda (f) (lambda (x) (f ((zero f) x))))

;; ((zero f) x) は (lambda (f) (lambda (x) x)) と置き換えられて
;; そのまま x に

(lambda (f) (lambda (x) (f x)))

上記の手続きを add-1 に渡してみるとどうなるか。

(add-1 (lambda (f) (lambda (x) (f x))))

(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) (f x))) f) x))))

(lambda (f) (lambda (x) (f ((lambda (x) (f x)) x))))

(lambda (f) (lambda (x) (f (f x))))

再度、上記を add-1 に。

(add-1 (lambda (f) (lambda (x) (f (f x)))))

(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) (f (f x)))) f) x))))

;; むむむむ
(lambda (f) (lambda (x) (f ((lambda (x) (f (f x))) x))))

(lambda (f) (lambda (x) (f (f (f x)))))

なんか、これで良いのかどうかが微妙やっさ。

参考にしたのは以下のサイト
Church Numerals と Lambda Calculus

これはこれは、と言いつつ

• one と two の定義
• 加算手続き + の定義

などとゆーオーダーがあるのに気づく。(こら

これ、置き換えしただけではなくって、上記サイトの検証も含め、きちんと理解しないと解をヒネり出せんよ。

そろそろ他所はどうか、なチェキを入れてみても良いのかなぁ。