Scheme でλ計算(2)
昨日の続き。今日はチャーチ数です。
ZERO と ONE
ZERO と ONE の定義は簡単です。
;; 0 := λf x. x (define ZERO (lambda (f x) x)) ;; 1 := λf x. f x (define ONE (lambda (f x) (f x)))
SUCC
SUCC の定義も、昨日の CONS が分れば、同じようにできます。
;; SUCC := λn f x. f (n f x) (define SUCC (lambda (n) (lambda (f x) (f (n f x)))))
難しいのは、ONE と (SUCC ZERO) が等しいか調べることです。二つの理由により、equal? では比較できません。
- そもそも Scheme の仕様では、equal? で lambda 式を比較したときの動作は定義されていません。
- SUCC は二重に lambda を使っているので、帰ってくるのはクロージャです。n は展開されません。
Scheme の仕様には、関数の本体を取り出す関数が用意されてないようです。そこで、MIT Scheme の pp を使って ONE を表示してみます。
(pp ONE) ;; >> (lambda (f x) (f (n f x)))
期待した (lambda (f x) (f x)) という形にはなっていません。
しょうがないので、f に 1+、x に 0 を代入することで比較することにしました。
(ONE 1+ 0) ;; => 1 ((SUCC ZERO) 1+ 0) ;; => 1
PLUS
PLUS は以下のように定義できます。
;; PLUS := λm n f x. m f (n f x) (define PLUS (lambda (m n) (lambda (f x) (m f (n f x)))))
うまく動くか、実験してみます。
(define TWO (SUCC ONE)) (define THREE (SUCC TWO)) ((PLUS TWO THREE) 1+ 0) ;; => 5
うまくいきました。\^^/
