Lambda calculus revolves around the application of anonymous functions -- lambda expressions.
[For the sake of clarity, I'll be using the syntax
(a -> b) over (lambda a. b).]It's best to explain by example.
(a -> b) x becomes b(a -> a) x becomes x(a b -> b a) x y becomes y x(a b -> b a) (a -> b) (a -> a) becomes (a -> a) (a -> b) becomes (a -> b)Everything is a function in this extremely minimal lambda calculus. I'll introduce you to some of the most important ones:
I = (x -> x)I doesn't do much -- it just returns its argument.true = (a b -> a)false = (a b -> b)true returns its first argument while false returns its second argument. They're the archetypal Boolean values of lambda calculus.0 = (f x -> x)
1 = (f x -> f x)
2 = (f x -> f (f x))
3 = (f x -> f (f (f x)))
...These are called the Church numerals, and they're used to apply a function to an argument a variable number of times. Note the similarity (in fact, equivalence) between 0 and false.
succ = (n f x -> f (n f x))We can use succ to go from one Church numeral to the next. It is now trivial to do arithmetic on Church numerals.
add = (a b -> a succ b)mul = (a b -> a (add b) 0)G'night. Tomorrow: More lambda calculus.
