λ Calculus

A lambda calculus is a set of rules and strategies for manipulating logical expressions. As Church defined them, these logical expressions are linear lists of symbols. A symbol is effectively a variable. Two expressions in sequence indicate a function application. The special symbol λ is just a marker to indicate a function. Parenthesis can be used to group expressions.

McCarthy’s S-expressions are an alternative representation of a logical expression that is more suitable for a computer. Rather than a linear list of symbols, S-expressions use a tree structure of linked lists in memory. Symbols are still variables, lists represent function application, the special symbol lambda at the beginning of a list indicates a function, and grouping is achieved by nesting a list within another.

When McCarthy invented S-expressions, he wanted to show that the nested list structure of S-expressions could faithfully represent the logical expressions from lambda calculus. (It can.) A lambda calculus can be restated as a set of rules and strategies for manipulating S-expressions. This makes it easier for a computer to do lambda calculus. As a Lisp hacker, I find it also makes it easier for me to think about lambda calculus.

Your basic lambda calculus just has symbols, lists, and λ expressions. That’s it. But let us introduce one more element. Recall that we can think of a LET expression as syntactic sugar for a list (function call) where the first element (the operator) is a lambda expression. We’ll keep our S-expressions fully sugared and write all such lists as LET expressions. So now our S-expressions have symbols, lists, λ expressions, and LET expressions.

The two basic rules for manipulating S-expressions are α, which is a recursive rule for renaming a symbol in an S-expression, and β, which gets rid of a selected LET expression. A basic lambda calculus consists of these two rules and a strategy for selecting which LET expressions to get rid of. β reduces a LET expession by substituting the variables for their bindings in the body of the LET. α is used as needed to avoid unwanted variable capture during β-reduction. β eliminates one LET expression, but it can introduce more if you end up substituting a λ expression into operator position.

If an expression contains no LET expressions, we say it is in “normal form”. A common task in lambda calculus is to try to reduce an expression to normal form by attempting to eliminate all the LET expressions. Sometimes you cannot achieve this goal because every time you apply the β rule to eliminate a LET expression, it ends up introducing further LET expressions.

There are many strategies for selecting LET expressions to eliminate. Not all strategies will necessarily end up getting you to a normal form, but all strategies that do end up at a normal form end up at the same normal form (modulo the variable names). One strategy is of note: selecting the leftmost, outermost LET expression and reducing it first is called “normal order”. It is notable because if any strategy converges to normal form, then the normal order strategy will, too. However, the normal order strategy can lead to an exponential explosion of intermediate expressions. There are other strategies that avoid the exponential explosion, but they don’t always converge to normal form. Pick your poison.

α and β are the only rules we need to compute with S-expressions. The simple lambda calculus with α and β is universal — it can compute anything that can be computed. It is Turing complete.

I don’t know about you, but I find it quite remarkable that this can compute anything, let alone everything. Nothing is going on here. α just renames symbols. Using α-conversion to rename all the foos to bars doesn’t change anything but the symbol names. We define expression equivalence modulo α, so the actual names of the symbols isn’t important. Apparently β-reduction does computation, but it is hard to say how, exactly. It is just simplifying LET expressions by replacing variables with what they are bound to. But a variable is simply a name for a binding. When you replace a variable with what it is bound to, you don’t change any values. The resulting expression may be simpler, but it means the same thing as the original.

We use β reduction as a model of subroutine (function) calls. In a subroutine call, the values of the arguments are bound to the names of the arguments before evaluating the body of the subroutine. In β reduction, the body of the expression is substituted with the names bound to the value expressions. The lambda calculus model of a computer program will have a β reduction wherever the program has a subroutine call. A lambda calculus expression with opportunities for β reduction can be translated into a computer program with subroutine calls at those locations. It’s a one-to-one mapping. Since we can compute anything using just the α and β rules, we can likewise compute anything with just function calls. I think that’s pretty remarkable, too.

Turing’s machine formalism was designed to be understandable as a physical machine. Turing was particular that his machine could be realized as a mechanical object or electronically. It is far less clear how to make a lambda calculus into a physical machine. Once we recognize that β can be realized as a subroutine in software, we can see that Church’s lambda calculus formalism can be understable as a virtual machine.

Church’s Calculi of Lambda Conversion is a cool book where he lays out the principals of lambda calculus. It is pretty accessible if you have experience in Lisp, and the examples in the book will run in a Scheme interpreter if you translate them.