;; from http://www.jetcafe.org/~jim/lambda.html
;; lambda-calculus to scheme translation
;; Lx.M -> (lambda (x) M)
;; (M)N -> (M N)
;; function application
;; Lx.chocolate-covered x
(define f1 (lambda (x) (list 'chocolate-covered x)))
;; (Lx.chocolate-covered x)peanuts
(print (f1 'peanuts))
;; covering function maker
;; Ly.Lx.y-covered x
(define f2 (lambda (y) (lambda (x) (list y 'covered x))))
;; caramel-covering function
;; (Ly.Lx.y-covered x)caramel -> Lx.caramel-covered x
(define f3 (f2 'caramel))
(print (f3 'ants))
;; apply-to-ants function
;; Lf.(f)ants
(define f4 (lambda (f) (f 'ants)))
;; (Lf.(f)ants)Lx.chocolate-covered x
;; -> (Lx.chocolate-covered x)ants
;; -> chocolate-covered ants
(print (f4 f1))
;; if-then-else
;; true = Lx.Ly.x
(define true (lambda (x) (lambda (y) x)))
;; false = Lx.Ly.y
(define false (lambda (x) (lambda (y) y)))
;; if-then-else = La.Lb.Lc.((a)b)c
(define if-then-else (lambda (a)
(lambda (b)
(lambda (c)
((a b) c)))))
;; (((if-then-else)false)apple)banana
;; -> (((La.Lb.Lc.((a)b)c)Lx.Ly.y)apple)banana
;; -> ((Lb.Lc.((Lx.Ly.y)b)c)apple)banana
;; -> (Lc.((Lx.Ly.y)apple)c)banana
;; -> ((Lx.Ly.y)apple)banana
;; -> (Ly.y)banana
;; -> banana
(print (((if-then-else false) 'apple) 'banana))
;; cons = if-then-else
;; head = Lx.(x)true
;; tail = Lx.(x)false
;; 0 = Lf.Lx.x
;; 1 = Lf.Lx.(f)x
;; 2 = Lf.Lx.(f)(f)x
;; 3 = Lf.Lx.(f)(f)(f)x
(define number-0 (lambda (f) (lambda (x) x)))
(define number-1 (lambda (f) (lambda (x) (f x))))
(define number-2 (lambda (f) (lambda (x) (f (f x)))))
(define number-3 (lambda (f) (lambda (x) (f (f (f x))))))
;; succ = Ln.Lf.Lx.(f)((n)f)x
;; + = Lm.Ln.Lf.Lx.((m)f)((n)f)x
(define add (lambda (m)
(lambda (n)
(lambda (f)
(lambda (x)
(((m f) (n f))) x)))))
;; * = Lm.Ln.Lf.(m)(n)f
(define mul (lambda (m)
(print "lambda m")
(lambda (n)
(print "lambda n")
(lambda (f)
(print "lambda f")
(m (n f))))))
;; TODO how to formulate this?
;;(print ((mul number-2) number-3))
;;(print ((mul (number-1 (number-2 1)))))
;; zero? = Ln.((n)(true)false)true
;; pred = Ln.(((n)Lp.Lz.((z)(succ)(p)true)(p)true)Lz.((z)0)0)false
;; Y-combinator
;; Y = Ly.(Lx.(y)(x)x)Lx.(y)(x)x
;; (Y)E -> (E)(Y)E -> ... -> (E)...(E)(Y)E