チャーチ数
(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)))))))