あどけない話

インターネットに関する技術的な話など

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

うまくいきました。\^^/

追記

MIT/GNU Scheme には 1+ がありますが、MzScheme や Gauche にはありませんので、以下の定義が必要です。

(define 1+ (lambda (x) (+ x 1)))