チャーチ数

(define I (lambda (x) x))
(define K (lambda (x) (lambda (y) x)))
 
(define S (lambda (x)
      (lambda (y)
        (lambda (z) ((x z) (y z))))))
(define C (lambda (x)
      (lambda (y)
        (lambda (z) ((x z) y)))))
(define V (lambda (x)
      (lambda (y)
        (lambda (z) ((z x) y)))))
(define R (lambda (x)
      (lambda (y)
        (lambda (z) ((y z) x)))))
(define T (lambda (x)
      (lambda (y) (y x))))
 
(define B (lambda (x)
      (lambda (y)
        (lambda (z) (x (y z))))))

;;ブール値
(define f (K I))
(define t K)


;; チャーチ数
(define %succ (S B))
(define %0  f)
(define %zero?  ((V (K f)) t))

;; plus = (S (K S) (S (K (S (K S))) (S (K K))))
;;      = (S (S K) (B B))) = (B S (B B))
(define %plus ((B S) (B B)))
;;(define %plus  (lambda (n) (lambda (m) (lambda (s) (lambda (z) ((n s) ((m s) z)))))))
;(define %plus  ((S (K S)) ((S (K (S (K S)))) (S (K K)))))
;;(define %mult  (lambda (n) (lambda (m) (lambda (s) (lambda (z) ((n (m s)) z)))))))
;;(define %mult ((S (K S)) K))
(define %mult B)
;;(define %exp  (lambda (n) (lambda (m) (lambda (s) (lambda (z) (((m n) s) z)))))))
;;(define %exp ((S (K (S I))) K))
(define %exp T)
 
 
(define (decode-n n) ((n (lambda (x) (+ x 1))) 0))

;; pred wikipediaより
;; pred : λn f x. n (λg h. h (g f)) (λu. x) (λu. u)
;; pred = (S (S (K S) (S (K (S (K S))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) K) (K (S (K (S (K (S I)))) (S (K (S (K K))) (S (K (S I)) K)))))))) (K (K K))))) (K (K (K I))))
;;
;;(define %pred ((S ((S (K S)) ((S (K (S (K S)))) ((S ((S (K S)) ((S (K (S (K S)))) ((S (K (S (K K)))) ((S ((S (K S)) K)) (K ((S (K (S (K (S I))))) ((S (K (S (K K)))) ((S (K (S I))) K))))))))) (K (K K)))))) (K (K (K I)))))
 
;; pred TAPLより
(define %zz ((V f) f))
(define %ss ((S ((S (K V)) (T f))) ((S (K (S B))) (T f))))
(define %pred ((S (K (T t))) ((S ((S I) (K %ss))) (K %zz))))
 
 
(define churchnat
  (lambda (n)
    (if (= n 0)
      (lambda (f) (lambda (z) z))
        (lambda (f) (lambda (z) (f (((churchnat (- n 1)) f) z)))))))