Beta (β) reduction in 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. What is the lambda (λ) calculus?
2. Bound vs. free variables in the lambda (λ) calculus
3. Delta (δ) rules in the lambda (λ) calculus
4. (This article) 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

---

Having covered the lambda calculus delta (δ) rules in a previous article, let’s now move on to another reduction rule known as beta (β) reduction. Formally, beta reduction is defined as: \[(\lambda\ x. \ E) \ z \overset{\beta}{\longrightarrow} \ E[\frac{z}{x}]\] That’s a lot of new notation! Let’s go through it together. You can read the definition above as:

• A lambda abstraction
  • with a formal parameter named x
  • and a function body of expression, E
  • and argument z
• is beta reduced:
  • by replacing all free occurrences of x in the expression E with z
    • (if you need a refresher on what it means for a variable to be free, check out this article)

Even the elaboration above is quite confusing and so let’s make the definition concrete by looking at an example. Consider the following lambda expression: \[(\lambda x.\color{red}{(+\  x \ 1))} \ 4\] As we’ve understood from a previous article, a lambda abstraction effectively defines an anonymous function. This one has a single variable and the function body just adds 1 to it. Let’s see how the parts of this lambda abstraction relate to the definition of beta reduction above:

• First, we have the λx. which is the same in both.
• Then we have the body of the lambda abstraction which is marked as red. This corresponds to the part of the beta reduction definition denoted by the capital E.
• And the value 4 corresponds to z in the beta reduction definition.

Now we want to perform a beta reduction on this expression and so, following the definition:

• We first consider the body of the lambda abstraction – which we have marked in red.
  • We need to see what occurrences of the formal parameter x are free within the expression.
  • When you consider only the body (that is the bit in red) there is no λx. declaration to bind x to, and so x occurs free in the body.
  • Since x occurs free in the function body, it is eligible to be replaced by z (which has the value 4 in our lambda expression).
• The result of the beta reduction is a copy of the body of the lambda abstraction with all free occurrences of the formal parameter replaced with the argument.

So, we copy the body and replace x with 4 since x occurs free, and we can reduce that expression further by using a delta rule to get to the final answer: \[(\lambda x.\color{red}{(+\  x \ 1))} \ 4 \overset{\beta}{\longrightarrow} (+ \ 4 \ 1) \overset{\delta}{\longrightarrow} 5\] That’s it for beta reduction! Remember, you need to consider what occurs free in the body of the lamdba abstraction, and a beta reduction is a copy of the body of the lambda abstraction with the occurrences of the free variable replaced with the argument! Let’s now move on to another reduction rule in the next article: α-conversion.