Learning the Lambda Calculus, cont.

In the last post we looked at the basic syntax of the LC and the three rules. Lets go back a little bit and talk about constructing terms before going forward. Once we know how to construct terms I hope to show what the three rules are really about.

The LC was originally developed to investigate and provide a foundation for math. This project was not successful (hopefully we can get to what I mean by that some other time), but the system has been recognized as being important in itself. I mention this only because the LC gets to the essence of math- math is about writing down symbols that obey rules. To capture this property the LC is really a syntactical system. This means that we are really concerned with writing and rewriting symbols- alpha conversion replaces one symbol with another, beta reduction substitutes one symbol (the name of the parameter) with a term (the argument being applied) (we will talk about eta reduction some other time). If the LC is about syntax, and its meaning is secondary, then we should investigate what are valid statements and how to construct them.

Any sequence of symbols that is valid in the LC is called a term. This means that we must have some way of defining well formed formula's or there would be no way to say what was a term and what was not. All variables by themselves are terms; for any two terms, the application of the first to the second is a term (for e1 and e2 we can write e1(e2) or e1e2); and for any term e and variable x, \x.e is a term. The set of terms has nothing in it except what is given by these rules.

Some example terms are (\p.\y.yzp)x, (\y.yz)x, (\r.rz)x, and xz, as well as the ones we saw in the last post. These four example terms have something in common- they are all the same! This is what the three rules are *really* about- they give a way to turn terms into other terms such that if we are given two terms and we can turn them into the same term using the three rules then the given terms are equal. Lets go over the example terms and see how each one can be turned into the others. The first term is (\p.\y.yzp)x which includes the term (\p.\y.yzp). Notice that this term is in the correct form for a little eta conversion (\p.\y.yzp) =eta (\y.yz). When we talk about equality of terms we will often say which rule we are applying- =eta means the left and right terms are equal after one eta conversion, with =beta and =alpha defined similarly. Now we have the second term, (\y.yz)x which is the same as (\r.rz)x except for the name of the variable y, so we have (\y.yz) =alpha (\r.rz) and therefore (\y.yz)x =alpha (\r.rz)x. The last conversion is between (\r.rz)x and xz and takes the form of a beta-reduction. (\r.rz)x =beta xz by replacing all occurrences of r with x in the term rz, giving xz. This term xz can be written rz[x/r] which is supposed to look like we are dividing out r from rz and replacing it with x.

In the next post I hope to go over some of the more interesting terms in the LC like the Y combinator (and SKI) and go briefly over normalization to show how the LC expresses non-termination. Then I will probably skip over other topics in the untyped LC to get to the stuff that I find really fun- the type systems.