原始帰納法

今度は原始帰納法．もちろん単なるif文でいけるのだけど，それだとちょっと見栄えが違うので違和感があるのと，一般の分岐ができてしまう普通のif文ではうっかり原始帰納法に依らないコードを書いてしまいそうな気がして．ただエラーチェックはしてないんで，意図的におかしな使い方をされては困る．
使用例：

gosh> (define ichi (S 0))
ichi
gosh> (define ni (S ichi))
ni
gosh> (define san (S ni)) 
san
gosh> (define-PR  ; 自然数の和
        ((plus 0 y) y)
        ((plus (S x) y) (S plus))) ; ここで右の plus は plus(x, y) の意
plus
gosh> (plus ichi ni)
(S (S (S 0)))
gosh> (plus san san)
(S (S (S (S (S (S 0))))))
gosh> (define-PR
        ((times 0 y) 0)
        ((times (S x) y) (plus y times)))
times
gosh> (times ni san)
(S (S (S (S (S (S 0))))))
gosh> (times san 0) 
0
gosh> (define-PR  ; 前者関数は「内部表現」に依らずとも原始帰納法で定義できる
        ((prd 0) 0)
        ((prd (S x)) x))
prd
gosh> (prd 0)
0
gosh> (prd ichi)
0
gosh> (prd ni)  
(S 0)
gosh> (define-PR  ; 自然数の差，負になるなら0
        ((minus-N 0 y) 0)
        ((minus-N x (S y)) (prd minus-N)))
minus-N
gosh> (minus-N san ni)
(S 0)
gosh> (minus-N ni san)
0
gosh> (minus-N ichi ichi)
0

実装：

(define (S x) ; successor
  (list 'S x))

(define (predecessor x) ; (S x) |-> x を行う．プログラマには見せない．
  (cadr x))

(define-syntax define-PR
  (syntax-rules ()
    ((define-PR ((f1 args1 ...) e1) ((f2 args2 ...) e2))
     (define-PR ((f1 args1 ...) () e1) ((f2 args2 ...) () e2)))
    ((define-PR ((f1 arg1 args1 ...) (reversed1 ...) e1)
                ((f2 arg2 args2 ...) (reversed2 ...) e2))
     (define-PR ((f1 args1 ...) (arg1 reversed1 ...) e1)
                ((f2 args2 ...) (arg2 reversed2 ...) e2)))
    ((define-PR ((f1) (reversed1 ...) e1) ((f2) (reversed2 ...) e2))
     (define-PR-aux (f1 (reversed1 ...) e1) (f2 (reversed2 ...) e2) () () ()))))

(define-syntax define-PR-aux
  (syntax-rules (S)
    ((define-PR-aux (f1 (0 reversed1 ...) e1) (f2 ((S x) reversed2 ...) e2)
                    (args1 ...) (args2 ...) ())
     (define-PR-aux (f1 (reversed1 ...) e1) (f2 (reversed2 ...) e2)
                    (xr args1 ...) (x args2 ...) (xr 0 x)))
    ((define-PR-aux (f1 (arg1 reversed1 ...) e1) (f2 (arg2 reversed2 ...) e2)
                    (args1 ...) (args2 ...) (xr ...))
     (define-PR-aux (f1 (reversed1 ...) e1) (f2 (reversed2 ...) e2)
                    (arg1 args1 ...) (arg1 args2 ...) (xr ...)))
    ((define-PR-aux (f1 () e1) (f2 () e2) (args1 ...) (args2 ...) (xr 0 x))
     (define (f1 args1 ...)
       (if (equal? xr 0)
           e1
           (let* ((x (predecessor xr))
                 (f1 (f1 args2 ...))) e2))))))

><