λ-Calculus Explained via CoffeeScript
Pull requests please to improve this document.
The lambda abstraction
λx.x is equivalent to the mathematical
f(x) = x is equivalent to the CoffeeScript function definition
(x) -> x.
The application of
(λx.x)(2) is equivalent to the mathematical
f(x) = x where x=2 is equivalent to the CoffeeScript
((x) -> x)(2).
We can use the λ-calculus to encode data, predicate logic, and recursion. For a programmer this is one way to hint at the λ-calculus's ability to compute all that is computable. Alonzo Church's methods of doing this encoding are not immediately intuitive. By giving parallel examples in an easily executable and familiar programming environment, it becomes easier to adopt these concepts.
Church booleans are an elegant way of representing "true" and "false".
TRUE = (x) -> (y) -> x # λx.λy.x FALSE = (x) -> (y) -> y # λx.λy.y
We implement a function
b that converts Church Booleans to literal
b = (f) -> f(true)(false)
This can be printed out like so:
console.log b(TRUE) # --> true console.log b(FALSE) # --> false
We can then construct logic operators
AND = (p) -> (q) -> p(q)(p) # λp.λq.p q p OR = (p) -> (q) -> p(p)(q) # λp.λq.p p q NOT = (p) -> (a) -> (b) -> p(b)(a) # λp.λa.λb.p b a IFTHENELSE = (p) -> (a) -> (b) -> p(a)(b) # λp.λa.λb.p a b
Note the symmetry between "AND" <-> "OR" and "NOT" <-> "IFTHENELSE".
We can apply the operators like so
AND(TRUE)(TRUE) # --> TRUE
Note that the return value of
AND(TRUE)(TRUE) is a "lambda abstraction"
(aka function) whose η-conversion is equivalent to
TRUE. To verify this
console.log b AND(TRUE)(TRUE) # --> true console.log b AND(TRUE)(FALSE) # --> false console.log b AND(FALSE)(TRUE) # --> false console.log b AND(FALSE)(FALSE) # --> false
We can also create predicates that return Church Booleans
ISZERO = (n) -> n((x) -> FALSE)(TRUE) # λn.n (λx.FALSE) TRUE
We can use
IFTHENELSE to perform logic
IFTHENELSE(TRUE)(THREE)(FOUR) # --> THREE IFTHENELSE(FALSE)(THREE)(FOUR) # --> FOUR IFTHENELSE(ISZERO(ZERO))(THREE)(FOUR) # --> THREE IFTHENELSE(ISZERO(ONE))(THREE)(FOUR) # --> FOUR
We can represent the natural numbers using Church Numerals.
$0 = ZERO = (f) -> (x) -> x # λf.λx.x $1 = ONE = (f) -> (x) -> f x # λf.λx.f x $2 = TWO = (f) -> (x) -> f f x # λf.λx.f (f x) $3 = THREE = (f) -> (x) -> f f f x # λf.λx.f (f (f x)) $4 = FOUR = (f) -> (x) -> f f f f x # λf.λx.f (f (f (f x))) $5 = FIVE = (f) -> (x) -> f f f f f x # λf.λx.f (f (f (f (f x))))
We implement a function
int that converts a Church Numeral into a
int = (n) -> n((x) -> ++x)(0)
We can then define operations that can use our Church Numerals to do math.
SUCC = (n) -> (f) -> (x) -> f (n(f)(x)) # λn.λf.λx.f (n f x) PLUS = (m) -> (n) -> (f) -> (x) -> m(f)(n(f)(x)) # λm.λn.λf.λx.m f (n f x) PLUS = (m) -> (n) -> m(SUCC)(n) # λm.λn.m SUCC n MULT = (m) -> (n) -> (f) -> m n f # λm.λn.λf.m (n f) POW = (b) -> (e) -> e b # λb.λe.e b # λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u) PRED = (n) -> (f) -> (x) -> n((g) -> (h) -> h g f)((u) -> x)((u) -> u) SUB = (m) -> (n) -> n(PRED)(m) # λm.λn.n PRED m,
Above we have defined the successor
PRED, and subtraction
SUB operators. The additive operators work by repeating an operation
times. The subtraction operators are more complex.
These operators, when given Church Numerals perform as expected
PLUS(ONE)(TWO) # --> THREE
We can use our
int operator to convert a Church Numeral into a
console.log int PLUS(ONE)(TWO) # --> 3 console.log int SUCC(ONE) # --> 2 console.log int MULT(TWO)(FIVE) # --> 10 console.log int POW(TWO)(FIVE) # --> 32 console.log int PRED(TWO) # --> 1 console.log int SUB(THREE)(TWO) # --> 1 console.log int SUB(TWO)(THREE) # --> 0
We can also define combinators, which are lambda expressions with no free variables. The simplest is the Identity combinator
I = (x) -> x # λx.x
A more useful combinator is the Y-Combinator. This allows us to use an anonymous function recursively.
Y = (g) -> ((x) -> g (x x))((x) -> g (x x)) # λg.(λx.g (x x)) (λx.g (x x))
For example, say we had the following FACTORIAL function
# λr.λn.(1, if n = 0; else n × (r (n−1))) FACTORIAL = (r) -> (n) -> IFTHENELSE(ISZERO n)(ONE)(MULT(n)(r PRED(n)))
Since it is illegal to use our function name in the function body (since λ-calculus abstractions are anonymous), we need to use the Y-Combinator.
Y(FACTORIAL)(FOUR) # --> 24