;#lang r5rs
; 11111111112222222222333333333344444444445555555555666666666677777777778
;2345678901234567890123456789012345678901234567890123456789012345678901234567890
; ABOUT
;
; Herein I am exploring the Lambda calculus through Scheme.
; Using only define and lambda, I'll build up language features.
; (Though Scheme will be needed for communicating with the world.)
;
; A couple of the sources I used...
; https://en.wikipedia.org/wiki/Church_encoding
; http://www.jetcafe.org/jim/lambda.html
;
; Don't be surprised if I get something wrong...
; A test macro
(define-syntax test
(syntax-rules ()
((test expr result)
(begin
(for-each display `(expr " -> " ,expr ": "))
(if (equal? expr result)
(display "Correct!")
(for-each display `("WRONG-expected: " ,result)))
(newline)))))
; LAMBDA CALCULUS
;
; A lambda expression may be one of...
; variable
; constant
; application
; abstraction
;
; An application is...
; lambda-expression lambda-expression
;
; An abstraction is...
; λvariable.lambda-expression
;
; Lambda expressions are evaluated via Alpha reduction and Beta reduction.
;
; Alpha reduction:
; λx.E -> λz.{z/x}E for any z which is neither free nor bound in E
;
; Beta reduction
; (λx.P)Q -> [Q/x]P
; LAMBDA CALCULUS TO SCHEME
;
; Lambda expression -> Scheme
; λx.M -> (lambda (x) M)
; M N -> (M N)
; M N O -> ((M N) O)
; M(N O) = M(N(O)) -> (M (N O))
; CHURCH ENCODING - NUMERALS
;
; zero = λf.λx.x
(define zero (lambda (f) (lambda (x) x)))
; one = λf.λx.f x
(define one (lambda (f) (lambda (x) (f x))))
; two = λf.λx.f(f x)
(define two (lambda (f) (lambda (x) (f (f x)))))
; succ(n) = n + 1 = plus(1) = λn.λf.λx.f(n f x)
(define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
; plus = λm.λn.λf.λx. m f (n f x)
(define _plus (lambda (m)
(lambda (n)
(lambda (f)
(lambda (x)
((m f) ((n f) x)))))))
; OR plus = λx. x succ
(define plus (lambda (x)
(x succ)))
; mult = λm.λn.λf.m (n f)
(define mult (lambda (m)
(lambda (n)
(lambda (f)
(m (n f))))))
; exp = λm.λn.n m
(define exp (lambda (m)
(lambda (n)
(n m))))
; pred = λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)
(define pred (lambda (n)
(lambda (f)
(lambda (x)
(((n (lambda (g)
(lambda (h)
(h (g f)))))
(lambda (u)
x))
(lambda (u)
u))))))
; minus = λm.λn. n pred m
(define minus (lambda (m)
(lambda (n)
((n pred) m))))
; TBD
; divide
; modulus
; Scheme functions to convert scheme numbers <-> church numbers.
(define (number->church-old n)
(if (= n 0)
(lambda (f)
(lambda (x)
x))
(lambda (f)
(lambda (x)
(f (((number->church-old (- n 1)) f) x))))))
; This version leverages the zero and succ we defined above.
(define (number->church n)
(if (= n 0)
zero
(succ (number->church (- n 1)))))
(define (church->number c)
((c (lambda (x) (+ x 1))) 0))
; Tests
(test (church->number zero) 0)
(test (church->number one) 1)
(test (church->number (number->church 10)) 10)
(test (church->number (succ (number->church 10))) 11)
(test (church->number ((plus (number->church 5))
(number->church 10)))
15)
(test (church->number ((mult (number->church 5))
(number->church 10)))
50)
; 5^10 took too long for codepad.org
(test (church->number ((exp (number->church 2))
(number->church 3)))
8)
(test (church->number (pred (number->church 10))) 9)
(test (church->number ((minus (number->church 10))
(number->church 5)))
5)
; CHURCH ENCODING - BOOLEANS
;
; T = λx.λy.x
(define T (lambda (x) (lambda (y) x)))
; F = λx.λy.y
(define F (lambda (x) (lambda (y) y)))
; if-then-else = λp.λc.λa.p c a
; (p = predicate, c = consequent, a = alternate)
(define if-then-else (lambda (p) (lambda (c) (lambda (a) ((p c) a)))))
; NOTE TO SELF
; In Scheme, you can't implement if as a function this way
; because Scheme predicates return #f or not-#f.
; The if-then-else function above requires predicates to return
; the T and F functions.
; Now back to Church numerals...
;
; zero? = λn.n (λx.F) T
(define zero? (lambda (n) ((n (lambda (x) F)) T)))
; Now for a test.
(test (((if-then-else (zero? zero)) 'yes) 'no) 'yes)
(test (((if-then-else (zero? two)) 'yes) 'no) 'no)
; le? = λx.λy. zero? (minus x y)
; This one is buggy.
(define lt? (lambda (x)
(lambda (y)
(zero? ((minus x) y)))))
'(test (((if-then-else ((lt? 10) 5)) 'yes) 'no) 'no)
'(test (((if-then-else ((lt? 5) 10)) 'yes) 'no) 'yes)
; TBD
; lt
; gt
; ge
; More Boolean operations (TBD)
; and = λm.λn. m n m
; or = λm.λn. m m n
(define and (lambda (m)
(lambda (n)
((m n) m))))
(define or (lambda (m)
(lambda (n)
((m m) n))))
; not = λm.λa.λb. m b a = λm. m (λa.λb. b) (λa.λb. a)
; Hmm...isn't that: λm. m F T
; This is buggy.
(define not (lambda (m)
((m F) T)))
(test (((if-then-else ((and (zero? zero))
(zero? one)))
'yes)
'no)
'no)
(test (((if-then-else ((or (zero? zero))
(zero? one)))
'yes)
'no)
'yes)
(test (((if-then-else (not (zero? zero))) 'yes) 'no) 'yes)
; CHURCH PAIRS (TBD)
; pair = λx.λy.λz. z x y
; first = λp. p (λx.λy.x)
; second = λp. p (λx.λy.y)
; Pairs, of course, lead to lists.
; Church numerals could be used for characters.
; Lists of Church numerals could be used for strings.
; Pairs can also be used to extend Church numerals from natural numbers to
; ...integers
; ...ratios
; ...floating point
; ...complex
; (There was a good Stack Overflow on this, but I can't find it right now.)
; CURRYING (TBD)
; The Lambda calculus uses only unary functions.
;
; Instead of...
; (lambda (x y) ...)
; ...we use...
; (lambda (x) (lambda (y) ...)
; Instead of...
; (f x y)
; ...we use...
; ((f x) y)
;
; Currying can be used to simulate n-ary functions.
; An extension to Lambda expressions to represent n-ary functions:
; λx.λy.x = λxy.x
; The Y-combinator (TBD)
; The Lambda calculus doesn't have a way to name functions.
; The Y-combinator is a way to create recursion without naming.
; I've been using Scheme's define, so I don't really need the Y-combinator.