The Lambda Calculus
Mads Torgersen’s post the other day was very cool! The first time I really understood Lambda Calculus was from this little 8-page paper. Relating it to Scheme made it stick for me. After reading Dr. T’s post I was just now having some fun playing with it in Scheme and couldn’t resist making a post of my own :-)
To start off, we can define true, false and if:
(true a b) a) (define (false a b) b) (define (if c a b) (c a b)) ; doesn't do much besides adding familiar 'if' syntax
Each of ‘true’ and ‘false’ are functions taking a pair of arguments and return one or the other of them. Then ‘if’ simply takes a boolean (instance of our true/false function) and applies it to a pair. Very strange to think of ‘true’ and ‘false’ as functions but everything is a function in Lambda Calculus. We can test it out with:
(if true 1 2) 1
> (if false 1 2) 2
It works! This is very similar to how ‘cons’, ‘car’ and ‘cdr’ are defined:
(cons a b) (λ (c) (if c a b))) (define (car c) (c true)) (define (cdr c) (c false))
Ah, our first use of λ. Calling ‘cons’ creates a pair in the form of a closure that when passed ‘true’ returns the head and when passed ‘false’ returned the tail. Again, it’s strange to think of a pair not as a data structure but as a function - everything is a function in LC. Seeing this was one of the awe moments for me when going through SICP. So, the ‘car’, just takes a pair and calls it with ‘true.’ Likewise ‘cdr’ calls with ‘false.’ Simple as that. We can test it:
(define foo (cons 1 2)) > (car foo) 1
> (cdr foo) 2
For demonstration, we’re using the Scheme number literals ‘1’ and ‘2’ but these don’t exist in LC. Instead, how do you get numbers? Did I mention that everything is a function in LC? Yes, these too are functions:
(zero f) (λ (x) x)) (define (one f) (λ (x) (f x))) (define (two f) (λ (x) (f (f x)))) (define (three f) (λ (x) (f (f (f x))))) ...
What the heck? In Church encoded numerals, ‘one’ is a function that takes a function as an argument and applies it once. Similarly, ‘two’ takes a function and applies it twice (f of f of x), ‘three’ applies three times, etc. Does your brain hurt yet? That's all part of the fun!
Once we start working with Church Numerals, we'll need a way to visualize them. Here's a helper to convert Church Numerals to normal Scheme Numerals:
( define (print n) ((n (λ (n) (+ n 1))) 0))
It uses the fact that Church Numerals are functions that apply functions n times. (print n) will apply n to a simple “increment” function, producing a result we can see printed for human consumption. It uses the ‘+’ operator and Scheme literals ‘0’ and ‘1’ which aren’t part of LC - just for demo purposes. So now we can do things like:
(print one) 1
> (print three) 3
Another useful function for dealing with Church numerals is to be able to recognize zero (from this we could build greater-than/less-than/equal-to operators):
( define (zero? n) ((n (λ (x) false)) true))
This ‘zero?’ function works by the fact that the Church numeral ‘zero’ applies its argument (a function) zero times, so we pass a function that, if called at all, returns false. Funny, eh? We can try it out (along with our ‘if’):
(if (zero? three) "yes" "no") "no"
> (if (zero? zero ) "yes" "no") "yes"
It’s a pain to define each of our ‘one’, ‘two’, ‘three’ literals. We can generalize the process with a ‘succ’ (successor) function:
( define (succ n) (λ (f) (λ (x) (f ((n f) x)))))
... and then redefine our natural number literals in terms each other; ultimately in terms of just ‘zero’ (like Peano's 5th and 6th postulates):
one (succ zero)) (define two (succ one)) (define three (succ two)) (define four (succ three)) (define five (succ four)) (define six (succ five)) (define seven (succ six)) (define eight (succ seven)) (define nine (succ eight)) (define ten (succ nine))
Cool, now we can even generate numbers for which we have no literal defined:
(print (succ ten)) 11
Defining ‘pred’ (predecessor) is a little tricky:
( define (pred n) (cdr ((n (λ (p) (cons (succ (car p)) (car p)))) (cons zero zero))))
We define a function that generates pairs of numbers (using our ‘cons’) which represent the next (using our ‘succ’) and the previous number. Given a pair, it will generate the next pair. So we can call it n times starting with (cons zero zero) and then take the ‘cdr’ and voila, we have the number prior to n. Of course, we call it n times by passing it to n(working with Church numerals is so weird). It all works:
(print (pred seven)) 6
Using ‘pred’ we can define ‘sub’ (subtract) and we can define ‘add’ in terms of ‘succ.’ Then we can define ‘mult’ in terms of ‘add.’ In fact, there’s nothing in mathematics that cannot be defined ultimately in LC!
(sub a b) ((b pred) a)) (define (add a b) ((b succ) a)) (define (mult a b) ((a (λ (x) (add x b))) zero))
The most insane thing of all is when you get to the Y Combinator which finds the fixed point of other functions so that they can “generate themselves” to do recursion. Some people love it so much they have it tattooed on their arm!
(http://blogs.discovermagazine.com/loom/wp-content/blogs.dir/27/files/science-tattoo-emporium/y-combinator.jpg ""<p>"I don’t quite have a science tattoo, but I have a math tattoo. That’s close enough, right?
"Now, for the explanation. This is a formula called the Y Combinator. It is a fixed-point combinator in the lambda calculus and was discover")
Below is the Z Combinator (just like Y but made for applicative order languages like Scheme - where just the definition of Y would cause infinite evaluation). I’m not going to try to explain it (the two links at the top of this post do a better job than I ever could):
( define Z (λ (f) ((λ (x) (f (λ (y) ((x x) y)))) (λ (x) (f (λ (y) ((x x) y)))))))
Now, for the grand finale. We can define good ol’ factorial as a function that takes an instance of itself (here ‘f’) and does the normal, “if n is zero then return 1, otherwise return n * factorial of n – 1” only when it says “factorial of ...” it means “apply the instance of ourselves that was passed in.” Very strange stuff, but this essentially defines ‘fac’ in terms of itself without itself referring to the name ‘fac’ anywhere in it’s body:
( define fac (Z (λ (f) (λ (n) (if (zero? n) one (mult n (f (sub n one))))))))
And finally, we can test this out:
(print (fac seven)) 5040
If we really want to get crazy we can go through and curry all the functions we’ve defined. For example, ‘add’ could be redefined as:
( define add (λ (a) (λ (b) ((b succ) a))))
In other words, instead of taking two arguments (‘a’ and ‘b’ as it was defined earlier), ‘add’ is now a λ that takes just one (‘a’) and returns a new λ that takes the second argument (‘ b ’) and does the calculation. Any function taking multiple arguments can be reduced to a chain of functions like this; each taking just one argument. This was one of the big contributions of Haskell Curry. It's more of a pain to call this new definition of ‘add’ but it works:
(print ((add three) four)) 7
Furthermore, if we want to go completely out of our minds, because of referential transparency we can go through our definition of ‘fac’ and replace all the references to various things we’ve defined (‘sub’, ‘one’, ‘mult’, ‘if’, etc.) with the bodies of those definitions and in turn, replace any references in those bodies. For example, replacing “add” with “(λ (a) (λ (b) ((b succ) a)))” and inside that replacing ‘succ’ its definition, etc. We can do this blindly without breaking anything and since ‘fac’ doesn't even refer to its own name (due to the beautiful Y/Z Combinator) we can systematically reduce our ‘fac’ to only a bunch of functions calling functions and returning functions. Here's the result:
( define fac ((λ (f) ((λ (x) (f (λ (y) ((x x) y)))) (λ (x) (f (λ (y) ((x x) y)))))) (λ (f) (λ (n) ((((λ (c) (λ (a) (λ (b) ((c a) b)))) ((λ (n) ((n (λ (x) (λ (a) (λ (b) b)))) (λ (a) (λ (b) a)))) n)) (λ (f) (λ (x) (f x)))) (((λ (a) (λ (b) ((a (λ (x) (((λ (a) (λ (b) ((b (λ (n) (λ (f) (λ (x) (f ((n f) x)))))) a))) x) b))) (λ (f) (λ (x) x))))) n) (f (((λ (a) (λ (b) ((b (λ (n) ((λ (c) (c (λ (a) (λ (b) b)))) ((n (λ (p) (((λ (a) (λ (b) (λ (c) ((((λ (c) (λ (a) (λ (b) ((c a) b)))) c) a) b)))) ((λ (n) (λ (f) (λ (x) (f ((n f) x))))) ((λ (c) (c (λ (a) (λ (b) a)))) p))) ((λ (c) (c (λ (a) (λ (b) a)))) p)))) (((λ (a) (λ (b) (λ (c) ((((λ (c) (λ (a) (λ (b) ((c a) b)))) c) a) b)))) (λ (f) (λ (x) x))) (λ (f) (λ (x) x))))))) a))) n) (λ (f) (λ (x) (f x)))))))))))
(print (fac seven)) 5040
Holy smokes! All we need is ‘λ’ - it's the ultimate all right! Totally crazy! But it proves that once we boil everything away, what we're left with is the very essence of computation: only functions taking a single function as an argument and returning a function (of the same). That's The Lambda Calculus.