計算機プログラムの構造と解釈 第二版 P52 問題2.4

おれ、がんばる。

• (car (cons x y))がxを生じることを証明。
• これに対するcdrの定義

証明ってどうスリゃいいかな。
具体的におっていけばいいのかな？

こんな感じかな？

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

;;1
(define g (cons 1 2))


;;2
(define (g f)
  (f 1 2)))

上の、1と2のgは等価です。
pの共通した性質は、ある手続きfを引数としてとって作用させる手続きだということ。
んだもんで、

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

;;4
(car g)

;;5
(define (f2 p q)
  p)

;;6
(g f2)

;;7
(f2 1 2)

んで、4のなかでは、5踏まえて考えると、6を行っている。
んで、6を置き換えると7だから、そうすると、値「1」出るよね。

そんで、cdrの実装は別に迷う必要もないと思うので。。んで、cdrの実装は以下へ。

#!/usr/local/bin/gosh
;; -*- coding: utf-8 -*-

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


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


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


(define p (cons 2 3)) 



;; main
(define (main args)

  (display "あらかじめ、(define p (cons 2 3))を実行しておく")(newline)

  (display "(car p): ")
  (display (car p)) 
  (newline)

  (display "(cdr p): ")
  (display (cdr p)) 

  (newline)
0)

実行

あらかじめ、(define p (cons 2 3))を実行しておく
(car p): 2
(cdr p): 3

なんか置き換えの証明って難しいな。