Lambda calculus (λ) reduction orders and normal form

---

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

1. 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. (This video) Lambda calculus (λ) reduction orders and normal form
9. The Church-Rosser theorem and the lambda (λ) calculus

---

Reducible Expressions and Normal Form

If an expression can be reduced to a simpler form using one of the reduction rules then it is known as a “reducible expression”.

If a lambda calculus expression contains no more reducible expressions within it then evaluation of the expression is complete and it is said to be in “normal form”.

Essentially, the evaluation of a lambda calculus programme, consists of successively reducing all of the reducible expressions of the program until it is in normal form.

That itself begs the question, when we have a large program, consisting of multiple reducible expressions – which one should we reduce? What is the order in which we should choose to reduce the expressions?

Lambda (λ) Calculus Reduction Orders

Consider the following expression:

\[(+ \ (* \ 3 \ 4)(* \ 7 \ 8)))\]

There are multiple ways in which we can reduce this expression to normal form: let’s look at two:

Reduction Order 1 – “leftmost outermost reducible”

In this reduction order we always choose the leftmost, outermost reducible expression and reduce that, until we reach normal form. So the reduction proceeds like so:

\[(+ \ (* \ 3 \ 4)(* \ 7 \ 8)))\] \[(+ \ 12(* \ 7 \ 8)))\] \[(+ \ 12 \ 56)\] \[ 68\]

Reduction Order 2 – “rightmost reducible”

In this reduction order we always choose the rightmost reducible expression and reduce that, until we reach normal form. So the reduction proceeds like so:

\[(+ \ (* \ 3 \ 4)(* \ 7 \ 8)))\] \[(+ \ (* \ 3 \ 4)\ 56)\] \[(+ \ 12\ 56)\] \[68\]

In both cases the reduction orders ended with the same result. But as you will see below: that is not always going to happen, and so the choice of reduction order can be important!

Reduction Orders Matter!

Consider the following expression:

\[(\lambda x.\color{red}{x \ x}) \color{blue}{(\lambda x.\ x \ x)}\]

We know that to reduce this expression we need to perform a beta reduction where we copy of the body of the lambda abstraction and replace it with the argument. The body of the lambda abstraction is highlighted in red, and the argument we need to overwrite it with in blue.

If we do the reduction:

\[\overset{\beta}{\longrightarrow} \ (\lambda x.\ x \ x) (\lambda x.\ x \ x)\]

Then you can see that we get the same expression back and if we reduce that we get the same expression again! What we have here is an infinite loop. This expression will never terminate.

It is important to note that whereas some reduction orders may reach normal form, others will not.

Now, let’s consider the following expression:

\[(\lambda x.\ 3)(\color{blue}{(\lambda x.\ x \ x) (\lambda x.\ x \ x)})\]

The expression in the blue is the same as the one above – resulting in an infinite loop if evaluated, and so if we choose to evaluate that first we will end up in an infinite loop which never terminates. But if we choose to evaluate the expression on the left first then we will immediately terminate with the value of 3: since the lambda abstraction just disregards the argument that is applied and always returns 3. Since after that reduction there are no more reducible expressions, we have reached normal form!

By choosing the leftmost expression we are using a reduction order which allows us to be lazy and not evaluate the argument to the lambda abstraction unless they are actually needed! Lazy evaluation is the default of some functional programming languages like Haskell. Sometimes it pays to be lazy, like in this situation, and sometimes it pays to be eager and evaluate the argument first.

Can we know if an expression has a normal form?

The unfortunate answer to that is no! In a specific case like the simple expression above then it is easily to calculate that the expression will terminate, but that is not possible in the general case. We cannot know whether an expression will terminate in the general case as we run into the halting problem.

Another question you may have is:

• Can two different reduction sequences lead to different normal forms?

We’ll explore the answer to that question in the next article in the series which covers the Church-Rosser theorems.