問題解答
引き続き Church 数と格闘。今日は加算手続き + の定義。
加算手続き (+ a b) は “a に対して手続きを b 回繰り返す手続き”。
普通に書くとこうなる
(define (add a b)
(define (add-iter f n)
(if (= n 0)
((lambda (x) (x))
((lambda (x) (f (add-iter (a b f (- n 1)))))))))
(add-iter f b))
ここで、置き替えないといけないのは if, True, False
404 Blog Not Found の記事を見ていたので、うろ覚えなのをしっかり理解する。
まずは記事中の記法の確認。
0 := λ f x . x 1 := λ f x . f x 2 := λ f x . f f x (define zefo (lambda (f) (lambda (x) x))) (define one (lambda (f) (lambda (x) (f x)))) (define two (lambda (f) (lambda (x) (f (f x)))))
λ式の展開が怪しいので手を動かしてみる
(define zefo (lambda (f) (lambda (x) x))) (define one (lambda (f) (lambda (x) (f x)) (define two (lambda (f) (lambda (x) (f (f x))))) (define (inc n) (+ n 1)) (define (to-s z) ((z inc) 0)) (to-s zero) (to-s (lambda (f) (lambda (x) x))) ;;zero を展開 (((z inc) 0) (lambda (f) (lambda (x) x))) ;;to-s を展開 (((lambda (f) (lambda (x) x)) inc) 0) ;;z に代入 ( ((lambda (f) (lambda (x) x)) inc) 0) ;;ブロックをわかりやすくした ((lambda (x) x) 0) ;;f に代入 0 ;;x に代入 (to-s one) (to-s (lambda (f) (lambda (x) (f x)))) (((z inc) 0) (lambda (f) (lambda (x) (f x)))) (((lambda (f) (lambda (x) (f x))) inc) 0) ((lambda (x) (inc x)) 0) (inc 0) ((lambda (n) (+ n 1)) 0) (+ 0 1) 1 (to-s two) (to-s (lambda (f) (lambda (x) (f (f x))))) (((z inc) 0) (lambda (f) (lambda (x) (f (f x))))) (((lambda (f) (lambda (x) (f (f x)))) inc) 0) ((lambda (x) (inc (inc x))) 0) (inc (inc 0)) ((lambda (n) (+ n 1)) ((lambda (n) (+ n 1)) 0)) ((lambda (n) (+ n 1)) (+ 0 1)) ((lambda (n) (+ n 1)) 1) (+ 1 1) 2
うーん。まあ慣れてきた。。。かな?
記事中の SUCC の復習。
SUCC := λ n f x . f(n f x) 2 := (λn f x . f(n f x)) 1 2 := λ f x . f(1 f x) 2 := λ f x . f(f x)
試しに 3 もやってみる。。。と思ったらうまくいかない。
ラムダ計算でよく出てくる謎の記法、これは何だ?
Wikipedia に載っていた。
“BNFで書かれた以下の文脈自由文法によって定義される。”
OK.もう一回やってみる。
3 := (λn f x . f(n f x)) 2 3 := λf x . f(2 f x) 3 := λf x . f(λ a b . a(a b) f x) 3 := λf x . f(f(f x)) 4 := (λn f x . f(n f x)) 3 4 := λf x . f(3 f x) 4 := λf x . f(λa b . a(a(a b)) f x) 4 := λf x . f(f(f(f x)))
カッコの扱いにちょっと慣れてきた。あと、lambda ではなくて λ と書けるのがありがたい。
SUCC の求め方も謎だったけど、思考を追った記事発見。これも手を動かして理解する。
ONE : λ f x.f x SUCC : λ n f x.f n (SUCC ONE) とした結果、TWO が得られれば OK. (SUCC ONE) (SUCC λ f x.f x) (λ n f x.f n λ f x.f x) λ f x.f λ a b.a b
“ここでα変換したλa.λb.a bを数ではなく、ひとつの函数*2として捉えると、どうやったら(f x)になるのかが見えてきます。”
見えてこないよ!! λ f x を展開するのか?
(a b) f x ;; λ a b.a b を二つの引数を取る関数とみなす (f x)
ONE に ONE を作用させたい場合、こうなるらしい。謎。
SUCC : λ n f x.f (n f x) (SUCC ONE) (λ n f x.f (n f x) ONE) (λ n f x.f (n f x) λ f x.f x) λ f x.f (λ a b.a b f x) λ f x.f (f x)
結論。理解できなかった。。。orz
泥沼化してるし、どこまで攻めるべきか。ちょっと考える必要がありそう。
そもそも SICP の先生を探したほうがいいのかも。