What is the lambda (λ) calculus?

---

This article is part of a series of articles on the lambda calculus and is also available as a YouTube video.

1. (This article) What is the lambda (λ) calculus?
2. Bound vs. free variables in the lambda (λ) calculus
3. Delta (δ) rules in the lambda (λ) calculus
4. Beta (β) reduction in the lambda (λ) calculus
5. Alpha (α) conversion in the lambda (λ) calculus
6. Eta (η) conversion in the lambda (λ) calculus
7. Summary of the lambda calculus (λ) evaluation rules
8. Lambda calculus (λ) reduction orders and normal form
9. The Church-Rosser theorem and the lambda (λ) calculus

---

So, what exactly is the lambda calculus? The lambda calculus (λ-calculus) is a formal system for expressing computation developed by Alonzo Church. Church was in 1903 and died in 1995 in the United States. It’s called the lambda calculus because the Greek letter lambda, λ, is used to define expressions and terms within the system (as we will see later). It is often useful to think of the lambda calculus as a sort of “assembly language” for functional languages. This is because higher level functional programming languages like Haskell, Ocaml and others usually translate their source code into an intermediate form of one of the many variants of lambda calculus. There are many variants of the lambda calculus which exist, including:

• The simple untyped lambda calculus.
• The simple typed lambda calculus.
• System F, the polymorphic lambda calculus.
• System Fω, a variant of system F with type operators.
• And others..

In this article we are going to look at the simple untyped lambda calculus. For those who are interested in finding out more I would recommend researching about the Hindley-Milner type system and System F. Before we look at the actual definition of the lambda calculus let’s take a minute to understand another concept: a lambda abstraction.

Defining a function as a λ-abstraction

“Lambda abstraction” is the term used within the lambda calculus for a function. Consider the following traditional mathematical function: \[f(x) = x + 1\] This defines a function called f which has a single argument x and the function body simply adds 1 to x. And you apply an argument to the function like so: \[f(1) = 1 + 1 = 2\] Now let’s consider the lambda abstraction equivalent: \[\lambda x.(+\  x \ 1)\] This may look like an alien language, but that is fine – I’ll explain it:

• First, it starts with the lambda symbol, then an x, then a dot, and then the function body.
• The lambda symbol denotes that a lambda abstraction is being defined.
• The x is the formal parameter to the lambda abstraction.
• Then within the brackets is the function body:
• In the lambda calculus function application is always written in the prefix form. So the + is always before its arguments.
  • It might be a bit weird to see at first because we are taught to place the plus operator in an infix position in mathematics classes but you will get used to it after a while.

All lambda abstractions follow this template: \[\lambda <variable>.<exp>\] where the <variable> is a name (like ‘x’) and the <exp> stands for the expression that makes up the function body. Unlike the traditional mathematical function, f, the lambda abstraction does not have a name. It is said to be an anonymous function. This is an important point. In the lambda calculus, functions do not have names – they remain anonymous. You apply an argument to the function using juxtaposition – meaning you place the argument next to lambda abstraction definition like so: \[(\lambda x.(+\  x \ 1)) 1 = (+ \ 1 \ 1) = 2\]

The simple untyped lambda (λ) calculus definition

Now that we know what a lambda abstraction is we can look at the actual definition of the lambda calculus. The image below (labelled Figure 2.1) contains the definition*: This definition is written in BNF which stands for Backus–Naur form. This is a simple way of describing the syntax of a language. The symbol “colon colon equals” (::=) can be read as “is defined as” and the pipe symbol (|) can be read as “or”. Anything within the less than (<) and greater than (>) signs is a name for a class of symbol within the language. So we can see that the lambda calculus is a language which allows you to define an <exp> (expression) where an expression is defined as: a constant OR a variable OR an expression placed next to another expression, OR a lambda abstraction. Now you see why we covered what a lambda abstraction is earlier in the article. An important thing to note about this definition is that it is recursive – that means that the thing that we are defining, <exp> is defined in terms of itself. Also, for our definition of <constant> we are including all numbers, as well as built in arithmetic functions such as addition, multiplication, etc. We can slowly build up lambda calculus programs by starting with an <exp> and replacing it with one of the options on the right. Let’s walk through a simple example confirming that (* 3 4) is a valid lambda calculus expression:

1. <exp>
   • We always begin with the <exp>
2. <exp> <exp>
   • One of the definitions of an <exp> is two expressions next to each other (application), so we replace the <exp> with <exp> <exp>.
3. <constant><exp>
   • We replace the first <exp> with <constant>, since one of the things an <exp> is defined as is a <constant>.
4. * <exp>
   • For our definition of <constant> we also include built in arithmetic functions, and so we can replace it with the multiplication function.
5. * <exp> <exp>
   • Just like from step 1 to 2 we replace the single <exp> with two next to each other.
6. * <constant> <exp>
   • We replace the first <exp> with <constant>.
7. * 3 <exp>
   • We swap the <constant> for the actual constant value 3.
8. * 3 <constant>
   • We replace the <exp> with a <constant>.
9. * 3 4
   • We replace the <constant> with the constant value 4.
10. (* 3 4)
    • We add brackets onto the final expression for grouping it together as one.

The ten steps shown above illustrate how the lambda calculus is a language with its definition and how that definition works in practice to write programs (even though this was an extremely simple one!). In the next article we look at the concept of “bound” vs. “free” variables in the lambda calculus.

---

*The image of the definition of the untyped lambda calculus is taken from the book The Implementation of Functional Programming Languages (1987) authored by Simon Peyton Jones. The book itself is available for free from here.