Hatena::Groupcsnagoya-sicp

yoshihiro503の日記

2009-04-11Exercise 2.2 2.4 2.6

Exercise 2.6

18:17

; デバッグ用 (チャーチ数をプリントする関数)
(define (p n) (print ((n (lambda (x) (+ 1 x))) 0)))
(define one   (lambda (f) (lambda (x) (f x))))
(define two   (lambda (f) (lambda (x) (f (f x)))))
(define three (lambda (f) (lambda (x) (f (f (f x))))))
(define four  (lambda (f) (lambda (x) (f (f (f (f x)))))))
(define five  (lambda (f) (lambda (x) (f (f (f (f (f x))))))))

(define (+ m n) (lambda (f) (lambda (x) ((m f) ((n f) x)))))

確認

gosh> (p (+ four five))
9
#<undef>

Exercise 2.4

17:47

Ex 2.4 は Coqで証明してみた。

Coqの証明

Exercise 2.2

12:34

line segmentの定義 (ポイントフリースタイルで)

(define make-segment cons)
(define start-segment car)
(define end-segment cdr)

同様にpointの定義

(define make-point cons)
(define x-point car)
(define y-point cdr)
(define (pair-app fg) (lambda (xy) (cons ((car fg) (car xy)) ((cdr fg) (cdr xy)))))

(define (av x1) (lambda (x2) (/ (+ x1 x2) 2)))
(define (midpoint-segment sp ep)((pair-app ((pair-app (cons av av)) sp)) ep)