SICP 問題 2.4(consの別表現)

例によって休み時間中に問題文を。。

問題

これは対のもう一つの手続き表現である。この表現について任意のオブジェクト x と y に対し、(car (cons x y)) が x を生じることを証明せよ。

(define (cons x y)
  (lambda (m) (m x y)))

(define (car z)
  (z (lambda (p q) p)))

これに対する cdr の定義は何か。(ヒント:これが働くことを調べるには、1.1.5節の置き換えモデル利用せよ。)

解答

ヒントをありがたく頂戴し、置き換えモデルをやってみよう。

(car (cons x y))

;↓

(car (lambda (m) (m x y)))

;↓

((lambda (m) (m x y)) (lambda (p q) p))

;↓

((lambda (p q) p) x y)

;↓

x

ということで、(car (cons x y)) が x を生じることは証明完了。
次、cdr の定義だが、まぁ上記の置き換えの最後の辺りを見れば、こうなることは明白。

(define  (cdr z)
  (z (lambda (p q) q)))

確認は・・・まぁいいか。