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)))
確認は・・・まぁいいか。