(define (cons x y) (lambda (m) (m x y))) (define (car z) (z (lambda (p q) p)))
以上の定義によって(car (cons x y))がxを生じることの証明、なんていわれてもアレですね。証明恐怖症++。
consは「2変数引数の関数」を引数として、それに対してx、yを渡した結果を返す関数になっている。それじゃ(car (cons x y))が何をしているかというと、置き換えれば分かる。
(car (cons x y)) ->((lambda (m) (m x y)) (lambda (p q) p)) ->((lambda (p q) p) x y) ->(x)
carはconsに対して、2つの引数のうち後ろの引数を返すような関数を渡している。
というわけでcdrについては、前の引数を返すような関数を、引数としてconsに渡してやればいいので、
(define (cdr z) (z (lambda (p q) q)))
でおｋ。
