Mathematical logic and foundations Definition

Eta conversion

Builds on Lambda calculus Beta reduction

Definition

Let $\Lambda$ be the set of terms of the lambda calculus, up to renaming of bound variables. An $\eta$ -redex is a term $\lambda x.\, M\, x$ in which the variable $x$ has no free occurrence in $M$ .

One-step $\eta$ -reduction $\to_\eta$ is the least relation on $\Lambda$ with these properties.

$\lambda x.\, M\, x \to_\eta M$ whenever $x$ is not free in $M$ .
If $M \to_\eta M'$ , then $M\, N \to_\eta M'\, N$ , $N\, M \to_\eta N\, M'$ and $\lambda y.\, M \to_\eta \lambda y.\, M'$ .

$\eta$ -conversion $=_\eta$ is the least equivalence relation that contains $\to_\eta$ . $\beta\eta$ -conversion $=_{\beta\eta}$ is the least equivalence relation that contains both $\to_\eta$ and the one-step beta reduction $\to_\beta$ .

Remarks

Example: $\lambda x.\, (\lambda y.\, y)\, x \to_\eta \lambda y.\, y$ , since $x$ is not free in $\lambda y.\, y$ . The same term also $\beta$ -reduces to $\lambda x.\, x$ , which is the same term up to renaming.

Non-example: $\lambda x.\, x\, x$ is not an $\eta$ -redex. It has the form $\lambda x.\, M\, x$ with $M = x$ , but $x$ is free in $M$ .

Adding $\eta$ to $\beta$ is equivalent to adding the extensionality rule: if $M\, x = N\, x$ for a variable $x$ free in neither $M$ nor $N$ , then $M = N$ . So $=_{\beta\eta}$ is the least equivalence relation that contains $=_\beta$ , is compatible with application and abstraction, and is closed under this rule.

Reading path

To understand this page from the ground up, read these 3 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Beta reduction concept
Lambda calculus concept
Eta conversion definition

Tag	`58TYSMQDA4`
URI	`m2://58TYSMQDA4`
Kind	definition
Writing	W0 stub
MSC	03B40, 68N18
Defines	Eta conversion
Uses	Lambda calculus, Beta reduction
Changed	3 November 2026

Eta conversion

Definition

Remarks

Reading path

Further reading

What this page needs for W1

What links here