Learning the Lambda Calculus, church numerals

In the first post in this series I wrote a lambda term (\xy.x+y) and promised I would make sense of it some other time. Well, the time has come! The reason I want to make this clear before moving to other subjects is that it is important that the LC consists entirely of the things we already defined- variables (x, y, z, ...), lambda abstractions ((\x.E) where E is a term and x a variable), and applications (E1 E2 or E1(E2) where E1 and E2 are terms and putting them next to each other means application). Even though there are variables, it is perfectly valid to say x(\y.y) or something like this, where the "function" in this term is x, and the argument is (\y.y) as its really functions on functions that return functions of function with functions all the way.

So, for something like x+y to make sense we would need a way of expressing number (natural numbers) with functions. We want them to have the same characteristics as our usual notion of a natural number: there should be one number called zero and a function that, if given any natural number, gives the number's successor. Notice that the whole of the natural numbers can be defined this way, and there is a clear connection with induction with zero as the base case and the successor map as the recursive case.

So, lets start with zero, defining it as (\f.\x.x). This term takes a function and returns a term that takes an argument and applied the function to the argument 0 times. This may make more sense if we look at the definition of 1- (\f.\x.fx)- which applied the function once, and 2- (\f.\x.f(fx))- which applies the function twice. I mentioned a successor function, which we expect to turn (\f.\x.x) into (\f.\x.fx) and must look like this: (\n.\f.\x.f(nx)). This function applies the function f to the result of nx which is f applied to the argument x n number of times, so the result is x with n+1 applied to f n+1 times.

So, back to the original term (\xy. x+y) we have to define addition. Well, this is simply (\n.\m.\f.\x.nf(mfx)) assuming n and m are numbers encoded as shown above. We can even give multiplication just as easily as (\n.\m.\f.\x.n(mf)x) which applies m exactly n times giving a total of n*m applications of f to x.

While the point of all of this was to clear up something in the first post in this series, there are several important topics that this brings up. What happens if we take the successor function and give it the multiplication function as its argument? It is certainly a valid lambda term, but does it make any sense? This is a fundamental problem with untyped systems- we don't have a way of expressing meaning and we can't restrict ourselves to only meaningful operations. Another point that I will not develop is that the ability to express simple arithmetic is a hugely important property in terms of computability.

While we are thinking about encoding things in the untyped lambda calculus, lets look at the expression of True and False, if statements and pairs. True is defined as (\x.\y.x) which may look familiar as it is simply the combinator K. False is (\x.\y.y) which is again familiar as it is just the encoding of zero. The reason that these definition make sense is that if we define "if" as (\b.\x.\y.bxy) then writing (informally) if false x y will reduce to x and if true x y will reduce to x, which makes it very much like branching based of off a condition that returns true or false.

Pairs are just as easy to encode- (\x.\y.\s.sxy) where x is the first thing in the pair and y is the second. If we put something in a pair- (\x.\y.\s.sxy)ab =beta (\s.sab) then we can get the first thing out by applying as the argument s the "fst" function (\p.p(\x.\y.x)) and we can get the second thing out by applying the "snd" function (\p.p(\x.\y.y)). Notice that fst = true and snd = false.

Having seen that we can encode interesting things in the untyped lambda calculus and further seen that it can lead to the problem that we can't enforce that the encodings are used in a meaningful way, I think we are finally ready to move on to type systems as I have been promising for a while.