What Is Lambda Calculus?

Lambda calculus and lambda math may seem daunting. But for developers who want to take full advantage of Lambdas in their programming language of choice, or for those who want to pursue functional programming, it's a worthwhile endeavor.

In this article, we give a brief history of lambda calculus, show how it's applied to programming, and give examples of how to use variable substitution, redex, and evaluation in lambda calculations.

What Is Lambda Calculus?

Lambda calculus (also written as λ-calculus or called "the lambda calculus") is a formal system in mathematical logic and computer science for expressing computation by way of variable binding and substitution. It captures the features of a wide variety of programming languages.

First formulated by Alonzo Church, lambda calculus found early successes in the area of computability theory, such as a negative answer to Hilbert's Entscheidungsproblem.

Introduction to Lambda Calculus

Did you know that Alonzo Church invented lambda math? Sadly, he died at the age of 92, but his contributions to theoretical computer science made much of what we do as developers possible today.

Lambda calculus is important in programming language theory, and the symbol λ has even been adopted as an unofficial symbol for the field. It can be considered the smallest universal programming language: any computable function can be evaluated in the context of λ-calculus and evaluating programs in the language consists of a single transformation rule: variable substitution.

Why would it be useful to know? Maybe you want better understanding of programming languages and computation? λ-calculus forms the basis of functional programming and as the world embraces functional programming more and more, perhaps it would be useful to know its roots.

Lambda Calculus in Math

An expression in lambda calculus can be a:

• variable: x
• lambda abstraction (function): λx.x(where . separates the function argument and body)
• function application: x y

Variables are just names that are bound as arguments to lambdas. Each lambda takes a single argument and multiple arguments are obtained by nesting lambdas (λx.(λy. x y)) – this is similar to currying in e.g. Haskell (did you know that Haskell and currying are both named after Haskell Curry, another important mathematician, also known for the Curry-Howard correspondence that relates programs to proofs). A function application consists of two expressions: the left hand side defines the function to apply and the right hand side gives the argument to apply the function to.

Applying Lambda Calculus

Compared to a Turing machine (to which λ-calculus is equivalent in computing capability), lambda calculus puts the emphasis on software, not caring about the details of the machine evaluating it. The lambda calculus in its pure form is untyped and has no concern about the types of expressions at all – it's all about computation in the form of variable substitution. In this post we only look at this untyped lambda calculus.

It's worth mentioning that the lambdas in lambda calculus are pretty much the same lambdas that many programming languages have (including Java 8, Scala, Kotlin etc.). Some of those languages might treat them a bit differently (e.g. non-local returns in Ruby), but mostly they are very similar to the lambda-calculus lambdas.

Lambda Calculus Functions

Functions are all there is in pure λ-calculus, so every value we can pass around must be a function. The simplest function is the identity function λx.x – it takes something (another function) as an argument and returns the same thing. When we want to represent "things" in our program, those must all be represented as functions.

Church Numerals

So if we want to have numbers, we have to encode them as functions. Thankfully, Alonzo Church already came up with such an encoding, where the value of a numeral is equivalent to the number of times a function is applied to an argument. This can be written as λs.λz. sn z, where n is the natural number represented and sn means function s composed with itself n times (we’ll say “applied n times” for short). Thus the first few natural numbers are encoded as follows:

• 0 = λs.λz. z the function s is applied to the argument z zero times
• 1 = λs.λz. s z the function s is applied once
• 2 = λs.λz. s (s z) the function s is applied twice

(the names s and z are short for successor and zero) Lets also quickly look at how we can write simple functions with numbers.

succ = λn.λs.λz. s (n s z) (n + 1)

succ adds 1 to a number. Since a number n is defined as a function that applies the 1st argument to the 2nd argument n times, the result should be a function that applies the 1st argument one more time. When you substitute the variable n in succ with a value x, that's what you get: a function that applies s one more time than x would:

(λn.λs.λz. s (n s z)) x → λs.λz. s (x s z)

Similarly, we define a + b so that it returns a function applying sb times and then a times

add = λa.λb.λs.λz. a s (b s z) (a + b)

To understand this more clearly, lets substitute values x and y for a and b:

(λa.λb.λs.λz. a s (b s z)) x y → (λb.λs.λz. x s (b s z)) y → λs.λz. x s (y s z)

As we can see, after applying x and y, the result is still a function that looks similar in shape to our original definition of numbers. It applies s to zy times, then applies s to the result x more times. Multiplication can be defined in a way that looks even simpler than the addition above:

mul = λa.λb.λs. a b s (a * b)

Substituting x and y gives us:

(λa.λb.λs. a b s) x y → (λb.λs. x b s) y → λs. x y s

It looks simpler, but is perhaps harder to grasp immediately: we used a trick and left out the z argument. Now the shape of the resulting function is different -- it applies y to sx times, but what does it mean to apply a number y to just one argument? Remember that if y is a number, it must perform a computation of the shape λs.λz. sy z. If we apply this to the s in the multiplication x times, we get the following (renaming the outer s to s’ to distinguish from the inner s):

λs’. (λs.λz. sy z)x s’

So in this case we see that the 2nd argument z is there in y, but we apply y only to s. This is similar to partial application in many languages. Lets see what happens if x = y = 1:

λs’. (λs.λz. s1 z)1 s’ = λs’. (λs.λz. s z) s’ → λs’.λz. s’ z(this is equivalent to the definition of 1)

Lets do 2 * 2 as well, where the substitutions become more complex and we rename some variables to distinguish similarly-named ones:

λs’. (λs.λz. s2 z)2 s’ = λs’. (λs.λz. s (s z))2 s’ = λs’. (λs.λz. s (s z)) ((λs’’.λz’’. s’’ (s’’ z’’)) s’) → λs’. (λs.λz. s (s z)) (λz’’. s’ (s’ z’’)) → λs’. λz. (λz’’. s’ (s’ z’’)) ((λz’’. s’ (s’ z’’)) z) → λs’. λz. (λz’’. s’ (s’ z’’)) (s’ (s’ z)) → λs’. λz. s’ (s’ (s’ (s’ z))))(this is equivalent to definition of 4)

To recap, we defined multiplication using partial application of lambdas, without mentioning the second argument z that we usually had in numbers, but the end result still has the correct shape. We could also have defined multiplication in a more verbose way that includes the z argument. Give it a try, or try to come up with an alternative definition of multiplication that uses succ or add.

Church Booleans

Booleans can also be encoded as functions:

• true = λt.λf.t 2-arg function returning the 1st arg
• false = λt.λf.f 2-arg function returning the 2nd arg

Basically, the booleans represent if-then-else expressions. They both take two arguments, true returns the first (then) and false returns the second (else). We’ll take a look at some example programs with booleans in the next posts.

Lambda Calculus Substitution & Evaluation 

Ok, so now we can represent some values and programs in λ-calculus, and we used some examples of variable substitution without defining the exact rules. What do the final results of evaluating programs look like? As evaluation happens by variable substitution, it seems the results should be programs where some substitution has happened, as we saw in the examples of multiplication. But when does the substitution begin and end?

Variable substitution is defined by a few rules, the most important is called β-reduction and means if we have an application with a lambda abstraction on the left hand side, we substitute the right hand side for the argument of the lambda. This kind of reducible expression is also called “redex”, and such a reduction corresponds to a single computation step.

For example:

(λt.λf.t) x → λf.x substituting x for t

There are different strategies for picking the next redex to reduce in a more complex expression. We will look at those in the next post, and implement one of the strategies. We can continue applying β-reduction until there are no more redexes.

Non-Terminating β-Reduction Expression Example

However, we must consider that it's possible to write programs for which β-reduction does not terminate. For example, the following expression:

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

reduces to itself when we apply a single step of β-reduction. An obvious thing we have to be careful of when substituting variables is that we cannot change the semantics of the program by naively replacing all variables with the same name. Consider the following expression: λx.(λx.x). Here the inner λx.x is the identity function, and the argument of the outer lambda is never used. If we substituted all names x, we would incorrectly get an expression with different semantics:

(λx.(λx.x)) y → λx.y

We must assume name collisions will happen and distinguish between bound and free variables. For example, in λx.x y, x is bound and y appears free (must not be substituted). In the λx.(λx.x) example, the outer x -- which is bound to the outer lambda -- should be substituted (however, there are no occurrences); and the inner x should be left as is.

Renaming Bound Variables in Lambda Calculus

One way of making this distinction properly is to rename bound variables during substitution, making sure to always give them unique names. This is called α-conversion and expressions that only differ in bound variable names are considered α-equivalent or even completely equivalent.

But how we implement the renaming technically is not always very important. We can also do the substitutions without any renaming if we keep track of lexical scopes of the variables – each lambda abstraction defining its own scope. Then we substitute x only if it’s defining scope is the scope of the left hand side lambda in the application.

Final Thoughts

Well, this turned out to be quite a lengthy introduction, as we spent quite a lot of time on Church numerals, which are not really useful for day-to-day programming. But on the other hand, the fact that functions can be used to represent any basic building blocks of programs -- such as numbers and booleans -- is quite interesting. In fact, any data structure could be represented as functions.

I think in general knowing lambda calculus isn’t necessarily going to make you a better programmer in any specific language, but it may give you a different perspective on some problems. It’s also useful if you are interested in reading programming language theory research, which often assumes some knowledge of lambda math.

Additional Resources

If you want to know more, stay tuned for the next posts where we look more deeply into parsing, evaluation and substitution strategies and implement the untyped λ-calculus in Scala. If you want a more deeper understanding of the underlying theory, I’d recommend reading Benjamin Pierce’s “Types and Programming Languages.”

Now that you have Lambda calculus mastered, you're bound to make a few mistakes applying them in Java 8! Read our article to help avoid some common Lambda errors.

Read the Article

Accelerate Your Java Development

Begin your free 10-day JRebel trial.

Try JRebel