Scheme でλ計算

Wikipedia のラムダ計算にある例を Scheme で実行して理解してみます。

TRUE と FALSE

TRUE と FALSE は簡単です。

;; TRUE := λx y. x
(define TRUE (lambda (x y) x))
;; FALSE := λx y. y
(define FALSE (lambda (x y) y))

AND、OR、NOT

難しいのは、本体に x y z のように複数の変数が出てきたときです。これは、Scheme でいうと (x y z) という関数呼び出しのことらしいです。という訳で、AND、OR、NOT が定義できます。

;; AND := λp q. p q FALSE
(define AND (lambda (p q) (p q FALSE)))
;;; OR := λp q. p TRUE q
(define OR (lambda (p q) (p TRUE q)))
;; NOT := λp. p FALSE TRUE
(define NOT (lambda (p) (p FALSE TRUE)))

うまく動くか実験してみましょう。

(AND TRUE FALSE) ;; => FALSE
(AND TRUE TRUE) ;; => TRUE
(NOT TRUE) ;; => FALSE

IFTHENELSE

ここまでできれば、IFTHENELSE は簡単でした。

;; IFTHENELSE := λp x y. p x y
(define IFTHENELSE (lambda (p x y) (p x y)))
(IFTHENELSE TRUE 'THEN 'ELSE) => 'THEN
(IFTHENELSE FALSE 'THEN 'ELSE) => 'ELSE

CAR、CDR、CONS

さて、次の問題は CONS です。2つしか引数を取らないはずなのに、3つ取るようになっています。試行錯誤の上、こうしてみました。

;; CONS := λf s b. b f s
(define CONS (lambda (f s) (lambda (b) (b f s))))
;; CAR := λp. p TRUE
(define CAR (lambda (p) (p TRUE)))
;; CDR := λp. p FALSE 
(define CDR (lambda (p) (p FALSE)))

試してみると、うまくいきます。

(CAR (CONS 'A 'B)) ;; => 'A
(CDR (CONS 'A 'B)) ;; => 'B

ふぅ

疲れたので、今日はここまで。