Eta Reduction

What Is Eta Reduction?

Eta reduction simplifies a term of the form λx.f x to just f, provided x does not occur free in f.

The intuition: λx.f x is a function that takes x and immediately hands it to f. It behaves identically to f on every input. Since the wrapper adds nothing, we can remove it.

The rule:

λx.M x →η M when x ∉ FV(M)

Example: λy.g y →η g (since y is not free in g).

The Eta Reduction Rule

The eta reduction rule:

λx.M x →η M when x ∉ FV(M)

Three requirements must all hold:

1. The body has the form M x — some term M applied to the bound variable x
2. x is the last thing applied — the body is exactly M x, not M x y or M (x x)
3. x does not occur free in M — the only role of x is being passed to M

Eta reduction captures extensional equality: two functions that produce the same output on every input are considered equal.

Apply Eta Reduction

Eta reduction: λx.M x →η M when x ∉ FV(M)

To apply the rule:

1. Check the body has the form M x — some term applied to the bound variable
2. Verify x does not appear free in M
3. The result is just M

Example: λy.g y →η g

• Body is g y (form M x with M = g)
• y is not free in g
• Result: g

When Eta-Reduction Does Not Apply

$\eta$-reduction applies only when the body has the exact form M x: some term M applied to the bound variable x, and nothing else.

These can be $\eta$-reduced:

• λx.f x $\to_\eta$ f (body is f applied to x)
• λx.(g h) x $\to_\eta$ g h (body is g h applied to x)

These cannot be $\eta$-reduced:

• λx.f x x — body is f x x, not M x with $x \notin \text{FV}(M)$. Here M would be f x, and x occurs free in f x.
• λx.x — body is just x, not M x form at all
• λx.f (g x) — body is f (g x), not M x form. The x is nested inside, not in the final application position.

The Free Variable Check

The side condition x ∉ FV(M) in the eta rule is essential. Without it, eta reduction would change the meaning of terms.

Consider λx.(x y) x:

• The body is (x y) x — the form M x with M = x y
• But x occurs free in x y
• Reducing to x y would turn x from a bound parameter into a free variable — completely different meaning

Compare with λx.(f y) x:

• The body is (f y) x with M = f y
• x does not occur free in f y
• Safe to reduce: λx.(f y) x →η f y

The check ensures the bound variable is truly just a pass-through.

Why Eta Matters

Eta reduction embodies the principle of extensional equality: two functions are equal if they produce the same result on every input.

λx.f x and f are extensionally equal because for any argument a:

(λx.f x) a →β f a

The wrapped version always gives the same result as applying f directly. Eta reduction recognizes this and allows us to simplify the wrapped form.

This matters because it gives us a formal way to say "these two terms behave the same" even when they look different syntactically. Without eta, λx.f x and f would be considered distinct terms despite being indistinguishable in use.