# Beta (β) reduction in the lambda (λ) calculus

**by** Liger Learn

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

- What is the lambda (λ) calculus?
- Bound vs. free variables in the lambda (λ) calculus
- Delta (δ) rules in the lambda (λ) calculus
- (This article) Beta (β) reduction in the lambda (λ) calculus
- Alpha (α) conversion in the lambda (λ) calculus
- Eta (η) conversion in the lambda (λ) calculus
- Summary of the lambda calculus (λ) evaluation rules
- Lambda calculus (λ) reduction orders and normal form
- 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)

- by replacing all

- 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.

- 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).

- We need to see what occurrences of the formal parameter x are
- 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.

**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.

### Recommended Posts

##### Church-Rosser theorems and the lambda (λ) calculus

October 19, 2023

##### Lambda calculus (λ) reduction orders and normal form

October 19, 2023

##### Summary of the lambda calculus (λ) evaluation rules

October 19, 2023