Skip to content

Instantly share code, notes, and snippets.

@nicky-zs
Created January 7, 2014 08:57
Show Gist options
  • Star 4 You must be signed in to star a gist
  • Fork 4 You must be signed in to fork a gist
  • Save nicky-zs/8296596 to your computer and use it in GitHub Desktop.
Save nicky-zs/8296596 to your computer and use it in GitHub Desktop.
Church Numerals implementation in scheme.
;; 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)
@nicky-zs
Copy link
Author

nicky-zs commented Feb 8, 2020

       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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment