Church Numerals implementation in scheme.

church-nums.ss

;; A Church-Numberal is a function, which takes a function f(x)
;; as its argument and returns a new function f'(x).
;; Church-Numerals N applies the function f(x) N times on x.

; predefined Church-Numerals 0 to 9
(define zero  (lambda (f) (lambda (x) x)))
(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 six   (lambda (f) (lambda (x) (f (f (f (f (f (f x)))))))))
(define seven (lambda (f) (lambda (x) (f (f (f (f (f (f (f x))))))))))
(define eight (lambda (f) (lambda (x) (f (f (f (f (f (f (f (f x)))))))))))
(define nine  (lambda (f) (lambda (x) (f (f (f (f (f (f (f (f (f x))))))))))))

; operations on Church-Numerals m and n
(define (succ   n) (lambda (f) (lambda (x) (f ((n f) x)))))
(define (add  m n) (lambda (f) (lambda (x) ((m f) ((n f) x)))))
(define (mult m n) (lambda (f) (lambda (x) ((m (n f)) x))))
(define (pow  m n) (lambda (f) (lambda (x) (((n m) f) x))))
(define (pred   n) (lambda (f) (lambda (x) (((n (lambda (g) (lambda (h) (h (g f))))) (lambda (u) x)) (lambda (u) u)))))
(define (sub  m n) (lambda (f) (lambda (x) ((((n pred) m) f) x))))

; verifying
(define (inc n) (+ n 1)) 

(printf "0 = ~a~n" ((zero inc) 0)) 
(printf "1 = ~a~n" ((one inc) 0)) 
(printf "2 = ~a~n" ((two inc) 0)) 
(newline)
(printf "succ(5) = ~a~n" (((succ five) inc) 0)) 
(printf "add(4, 7) = ~a~n" (((add four seven) inc) 0)) 
(printf "mult(0, 8) = ~a~n" (((mult zero eight) inc) 0)) 
(printf "mult(3, 8) = ~a~n" (((mult three eight) inc) 0)) 
(printf "pow(2, 9) = ~a~n" (((pow two nine) inc) 0)) 
(printf "pow(9, 0) = ~a~n" (((pow nine zero) inc) 0)) 
(printf "pred(6) = ~a~n" (((pred six) inc) 0)) 
(printf "sub(9, 5) = ~a~n" (((sub nine five) inc) 0)) 
(newline)

       one = λf.λx.f x
       two = λf.λx.f (f x)
     three = λf.λx.f (f (f x))

      pred = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

  pred two = (λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)) two
           = (λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)) (λf'.λx'.f' (f' x'))
           = λf.λx.(λf'.λx'.f' (f' x')) (λg.λh.h (g f)) (λu.x) (λu.u)
           = λf.λx.(λx'.(λg.λh.h (g f)) ((λg.λh.h (g f)) x')) (λu.x) (λu.u)
           = λf.λx.(λg.λh.h (g f)) ((λg.λh.h (g f)) (λu.x)) (λu.u)
           = λf.λx.(λg.λh.h (g f)) (λh.h ((λu.x) f)) (λu.u)
           = λf.λx.(λg.λh.h (g f)) (λh.h x) (λu.u)
           = λf.λx.(λh.h ((λh.h x) f)) (λu.u)
           = λf.λx.(λh.h (f x)) (λu.u)
           = λf.λx.((λu.u) (f x))
           = λf.λx.(f x)
           = λf.λx.f x
           = one

pred three = (λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)) three
           = (λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)) (λf'.λx'.f' (f' (f' x')))
           = λf.λx.(λf'.λx'.f' (f' (f' x'))) (λg.λh.h (g f)) (λu.x) (λu.u)
           = λf.λx.(λx'.(λg.λh.h (g f)) ((λg.λh.h (g f)) ((λg.λh.h (g f)) x'))) (λu.x) (λu.u)
           = λf.λx.((λg.λh.h (g f)) ((λg.λh.h (g f)) ((λg.λh.h (g f)) (λu.x)))) (λu.u)
           = λf.λx.((λg.λh.h (g f)) ((λg.λh.h (g f)) (λh.h ((λu.x) f)))) (λu.u)
           = λf.λx.((λg.λh.h (g f)) ((λg.λh.h (g f)) (λh.h x))) (λu.u)
           = λf.λx.((λg.λh.h (g f)) ((λh.h ((λh.h x) f)))) (λu.u)
           = λf.λx.((λg.λh.h (g f)) (λh.h (f x))) (λu.u)
           = λf.λx.(λh.h ((λh.h (f x)) f)) (λu.u)
           = λf.λx.((λu.u) ((λh.h (f x)) f))
           = λf.λx.((λh.h (f x)) f)
           = λf.λx.(f (f x))
           = λf.λx.f (f x)
           = two