Eta (η) 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. Alpha (α) conversion in the lambda (λ) calculus
6. (This article) 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

---

We now move on to the final reduction rule in the lambda calculus: eta (η) conversion.

Consider the following two lambda expressions:

\[(\lambda x. + \ 1 \ x) \ \text{and} \ (+ \ 1)\]

The first one contains a lambda abstraction but the second does not – it is just a simple expression. But in essence, the two expressions ought to be equivalent, right? They each take a parameter and add the number one to it. In the first case the parameter is formally defined with the x and in the second case the parameter is implicit because you are using the plus function which needs two parameters to operate on.

Here is where eta (η) conversion kicks in. Eta (η) conversion, is another reduction rule:

• If we have two expressions which behave in exactly the same way when an argument is applied then they can be eta converted into each other.
• Eta conversion is also known as eta reduction.
• An eta reduction allows us to replace the first expression, which is a lambda abstraction, with the simpler second expression which does not contain a lambda abstraction.

Formally we can define eta conversion:

• When we have a lambda abstraction with a formal parameter x
• And x is not free in E and E denotes a function
• It can be eta reduced to just the E

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

Eta reduction allows us to eliminate the lambda abstraction and so it is sometimes said to be an optimisation. Strictly speaking you don’t actually need it – but sometimes it does make a lambda expression simpler and compilers can perform it to optimise code.

That’s it – in the next article we will summarise all of the lambda calculus evaluation rules!