Alpha (α) conversion 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. Beta (β) reduction in the lambda (λ) calculus
5. (This article) 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 delta (δ) rules and beta (β) reduction we now move on to another reduction rule known as alpha (α) conversion. This rule is also sometimes known as alpha (α) renaming, for reasons we shall see below.

Consider the following lambda expression:

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

Let’s try to perform a beta reduction as we learned how to do in a previous article:

• First: we consider the body of the lambda abstraction (which I have marked in red) to see which variables occur free.
• The two occurrences of f occur free since there is no λf within the body (red bit) to bind it (the only λf in the expression occurs outside of the body).
• The occurrence of x does not occur free since there is a λx within the body (red bit) which binds it.

So we perform our beta reduction by copying the body of the lambda abstraction and replacing all occurrences of f with the argument (which is x):

\[\overset{\beta}{\longrightarrow} \lambda x. x \ (x \ x) \\ \text{This is an incorrect result!}\]

Have you spotted why this is an incorrect way of performing the reduction? It is because the value we are replacing f with (x) is already used as a formal parameter inside the body!

We cannot replace a variable with another variable which is already captured by an inner binding because there is a clash – this is known as the name-capture problem. To fix this issue it’s alpha-conversion to the rescue.

If we just change the name of the formal parameter x, along with all of its occurrences in the original expression to something else, then surely they ought to be equivalent? Changing the name of a formal parameter, as long as it is done consistently, does not change the meaning of the expression and is known as alpha conversion. And sometimes, when the name-capture problem exists, alpha renaming is actually necessary.

To deal with the name capture problem, we first perform an alpha conversion, changing the name of the variable x to y (note: only the variable name is changed – not the argument!):

\[(\lambda f.\color{red}{\lambda x. \ f \ (f \ x)}) \ x \overset{\alpha}{\longrightarrow} (\lambda f.\color{red}{\lambda y. \ f \ (f \ y)}) \ x \]

Having removed the name-capture problem, we can now perform the beta reduction. We copy the body of the lambda abstraction (marked red) and replace the free occurrences of the formal parameter (the two f occurrences) with the argument x:

\[ \overset{\beta}{\longrightarrow}  \lambda y. \ x \ (x \ y) \\ \text{This is the correct result!}\]

Compare this to the incorrect result above and you will see why it is necessary to perform the alpha conversion.

Formally, alpha conversion is defined as:

\[\text{If y is not free in E, then:} \\ (\lambda\ x. \ E) \ z \overset{\alpha}{\longrightarrow} \ \lambda\ y.E[\frac{y}{x}]\]

You can read the definition above as:

• when you have a lambda abstraction:
  • with a formal parameter named x
  • and a function body of expression, E
  • And y is not free in E
• then it is alpha converted by replacing the formal lambda parameter x to y and replacing occurrences of x in the expression E with y

In summary, alpha conversion (or alpha renaming as it is sometimes called) is another reduction rule which is sometimes necessary to perform before applying a beta-reduction. Some compilers include an alpha-conversion stage so that all variable names become unique. This is done to simplify subsequent processing and avoid any potential name-capture problems.

In the next article we explore eta conversion.