Lambda Calculus is one of those topics that a lot of undergrad comp sci students hear about, and sometimes read about, without actually understanding the significance. This is probably a result of the fact that lambda calculus, without context, seems completely useless. From a certain perspective, this is true. No modern programming language directly uses lambda calculus. The value of lambda calculus is primarily theoretical, but some of the ideas and constructs that result from lambda calculus are very practical. This article will serve as a quick overview of lambda calculus with the purpose of showing it’s significance, while staying away from esoteric issues such as typed/untyped lambda calculus. (Disclaimer: I’m not an expert on this subject)

Lambda Calculus is a very simple (yet powerful) language. There are three elements to a lambda calculus expression: Variables, Function Abstraction, and Function Application. Variables in lambda calculus are named and are generally represented by lowercase letters. Function abstraction is represented as “λx.z”, where x is the variable we are “abstracting”, and z is another lambda expression. This can be thought of as defining a function that takes a parameter (called x) and evaluates it in z. The third element, function application, is simply represented as “x y” where y is being “applied” to x. This can be thought of as if x is a function, and y is the parameters. With these three elements, we can express any program you can imagine.

At this point, I expect you are completely incredulous. It is hard to imagine even the simplest of useful programs being written in this language. I assure you, it can be painful at times, but every language feature you can imagine can be implemented with these three constructs. It’s likely that you now have two questions: “How is this possible?” and “Why does this matter?”

To answer the first question, I’ll first give a few brief examples that will give you an idea of how lambda calculus “works”. Suppose I have the following lambda expression:

(λx.x) z

In this expression, consider the parenthesized expression “λx.x” to be defining a function. It takes a parameter named “x”. We are applying z to this function. To evaluate this expression, we perform a textual substitution of every bound occurrence of x in the function. The expression evaluates to:

z

This is as simple as a lambda calculus program gets. One of the key ideas is that function application is evaluated as a textual substitution. This is known as a beta reduction. Because it is expressed as a symbolic replacement, there are some interesting things that you can do. Consider the following lambda calculus expression:

(λx.x x) (λx.x x)

When you use a beta reduction to evaluate this expression, you end up with this:

(λx.x x) (λx.x x)

Which is the exact expression we started with. You can infinitely beta-reduce this expression and never get anywhere. Expressions such as this cannot be reduced any further. There is a special class of expressions that are maximally reduced which are known as Church numerals.

0: λf.λx.x
1: λf.λx.f x
2: λf.λx.f (f x)
3: λf.λx.f (f (f x))

Something to note about these numerals: There are no reductions to be made