SICP 読み (15)

Church Numeral はカンニングに頼るしかないです (弱
以下に理解できた事をメモ。

前提となっている定義は以下。

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

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

で、(add-1 zero) を評価すると

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

なので、とりあえず ((zero f) x) を評価したらどうなるか、を見てみる。

((zero f) x)

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

((lambda (x) x) x)

x

とゆー事で (add-1 zero) が返すのは

(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 x))) f) x)

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

(f x)

という事はこうなるのか

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

こんな感じで定義可能かな。

(define zero 
  (lambda (f) (lambda (x) x)))
(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))))))

で、加算ですがカンニング (Church Numerals And Lambda Calculus より)

(define (%add n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))) )

ううむ。(%add one two) だとどうなるか。ここも中からカワを剥いだ方が分かりやすそげ、という事で以下。

まず、(m f) と ((n f) x) を部分的に。

(m f)

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

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

次。

((n f) x)

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

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

(f x)

という事は、((m f) ((n f) x)) は以下か。

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

(f (f (f x)))

加算はイメージし易いんですが、減算とかワケワカ。
参考にした文書は別途見ながら色々試してみても良いかも。