# What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda abstraction because there is nothing to do, kind of a pointless $\beta$-conversion.

So maybe $\eta$-conversion is something really deep and different from this, but, if it is, I don't get it, and I hope you can help me with it.

(Thank you and sorry, I know this is part of the very basics in lambda calculus)

-

Update [2011-09-20]: I expanded the paragraph about $\eta$-expansion and extensionality. Thanks to Anton Salikhmetov for pointing out a good reference.

$\eta$-conversion $(\lambda x . f x) = f$ is a special case of $\beta$- conversion only in the special case when $f$ is itself an abstraction, e.g., if $f = \lambda y . y y$ then $$(\lambda x . f x) = (\lambda x . (\lambda y . y y) x) =_\beta (\lambda x . x x) =_\alpha f.$$ But what if $f$ is a variable, or an application which does not reduce to an abstraction?

In a way $\eta$-rule is like a special kind of extensionality, but we have to be a bit careful about how that is stated. We can state extensionality as:

1. for all $\lambda$-terms $M$ and $N$, if $M x = N x$ then $M = N$, or
2. for all $f, g$ if $\forall x . f x = g x$ then $f = g$.

The first one is a meta-statement about the terms of the $\lambda$-calculus. In it $x$ appears as a formal variable, i.e., it is part of the $\lambda$-calculus. It can be proved from $\beta\eta$-rules, see for example Theorem 2.1.29 in "Lambda Calculus: its Syntax and Semantics" by Barendregt (1985). It can be understood as a statement about all the definable functions, i.e., those which are denotations of $\lambda$-terms.

The second statement is how mathematicians usually understand mathematical statements. The theory of $\lambda$-calculus describes a certain kind of structures, let us call them "$\lambda$-models". A $\lambda$-model might be uncountable, so there is no guarantee that every element of it corresponds to a $\lambda$-term (just like there are more real numbers than there are expressions describing reals). Extensionality then says: if we take any two things $f$ and $g$ in a $\lambda$-model, if $f x = g x$ for all $x$ in the model, then $f = g$. Now even if the model satisfies the $\eta$-rule, it need not satisfy extensionality in this sense. (Reference needed here, and I think we need to be careful how equality is interpreted.)

There are several ways in which we can motivate $\beta$- and $\eta$-conversions. I will randomly pick the category-theoretic one, disguised as $\lambda$-calculus, and someone else can explain other reasons.

Let us consider the typed $\lambda$-calculus (because it is less confusing, but more or less the same reasoning works for the untyped $\lambda$-calculus). One of the basic laws that should holds is the exponential law $$C^{A \times B} \cong (C^B)^A.$$ (I am using notations $A \to B$ and $B^A$ interchangably, picking whichever seems to look better.) What do the isomorphisms $i : C^{A \times B} \to (C^B)^A$ and $j : (C^B)^A \to C^{A \times B}$ look like, written in $\lambda$-calculus? Presumably they would be $$i = \lambda f : C^{A \times B} . \lambda a : A . \lambda b : B . f \langle a, b \rangle$$ and $$j = \lambda g : (C^B)^A . \lambda p : A \times B . g (\pi_1 p) (\pi_2 p).$$ A short calculation with a couple of $\beta$-reductions (including the $\beta$-reductions $\pi_1 \langle a, b \rangle = a$ and $\pi_2 \langle a, b \rangle = b$ for products) tells us that, for every $g : (C^B)^A$ we have $$i (j g) = \lambda a : A . \lambda b : B . g a b.$$ Since $i$ and $j$ are inverses of each other, we expect $i (j g) = g$, but to actually prove this we need to use $\eta$-reduction twice: $$i(j g) = (\lambda a : A . \lambda b : B . g a b) =_\eta (\lambda a : A . g a) =_\eta g.$$ So this is one reason for having $\eta$-reductions. Exercise: which $\eta$-rule is needed to show that $j (i f) = f$?

-
"Also, I have heard it said that η-rule is about extensionality of functions. This is false" If you augment the $\beta$-equality axioms and inference rules with the extensionality rule (see my answer), this set of inference rules captures exactly $\beta\eta$-equality, doesn't it? (i.e two terms are equal in this theory iff they are $\beta\eta$-equal) – Marcin Kotowski Sep 19 '11 at 0:03
@Marcin: yes, extensionality implies $\eta$-rule, but not vice versa. How would you derive extensionality from $\beta$- and $\eta$-rules? – Andrej Bauer Sep 19 '11 at 0:06
let $=$ denote the smallest congruence that contains $=_{\beta}$ and satisfies extensionality (if $Mx=Nx$, then $M=N$). Then $M=N$ iff $M=_{\beta\eta}N$ (see e.g. first chapter of Urzyczyn, Sorensen "Lecture on Curry-Howard isomorphism) and in this sense $\eta$-rule captures the notion of extensionality. – Marcin Kotowski Sep 19 '11 at 0:22
I see, you're thinking of extensionality as a schema, i.e., we prove that it holds for every particular pair of terms $M$ and $N$. I was thinking of extensionality as a statement. I think. Now I have to think about it. – Andrej Bauer Sep 19 '11 at 4:57
@AndrejBauer I agree that η-rule isn't full extensionality, but don't you think it is still a limited form of extensionality, i.e. it represents a class of obvious cases of extensionality. The original question is looking for motivations and concepts, and in this case I believe that thinking in terms of extensionality is useful (with some care taken of course not to go too far). – Marc Hamann Sep 20 '11 at 13:06

In order to answer this question, we can provide the following quotation from the corresponding monograph “Lambda Calculus. Its Syntax and Semantics“ (Barendregt, 1981):

The point of introducing of $\beta\eta$-reduction is to provide an axiom for provable statements in extensional $\lambda$-calculus [the $\lambda + \text{ext}$ theory, where $\text{ext}$ stands for the rule $M x = N x \Rightarrow M = N$] such that it would have Church–Rosser property.

Proposition. $M =_{\beta\eta} N \Leftrightarrow \lambda\eta \vdash M = N \Leftrightarrow \lambda + \text{ext} \vdash M = N$.

[Its proof is based on the following theorem.]

Theorem (by Curry). The theories $\lambda + \text{ext}$ and $\lambda\eta$ are equivalent… [Its proof consists of two parts: $(\text{ext}) \Rightarrow (\eta)$ and vice versa.]

One of the reasons to consider the system $\lambda\eta$ is that it has a certain property of completeness… [Namely, in the sense of the following theorem.]

Theorem. Let $M$ and $N$ both have a normal form. Then, either $\lambda\eta \vdash M = N$, or $\lambda\eta + M = N$ is inconsistent…

HP-complete [after Hilbert–Post] theories correspond to maximum consistent theories in theory of models for the first-order logic.

-

$\eta$-reduction captures the notion of extensionality - two functions are considered equal iff they give the same outputs on the same inputs.

One way of formalizing this notion is the following: if we consider the relation $=_{\beta \eta}$, the transitive-reflexive closure of relation $\rightarrow_{\beta\eta}$, it is natural to characterize this relation in terms of inference rules of an equational theory (e.g.: rules of the form: if $M=N$, then $\lambda x.M = \lambda x.N$ and so on - characterizing $=_{\beta}$ requires about 7 rules of this kind).

Now, replacing $=_{\beta}$ with $=_{\beta\eta}$ amounts to introducing the axiom $\lambda x. Mx = M$, which is equivalent to the extensionality rule: if $Mx=Nx$, then $M=N$. This is exactly the notion that two functions equal on all input arguments should be considered identical.

-
It is false that extensionality follows from $\eta$-rule. – Andrej Bauer Sep 19 '11 at 0:00
See Theorem 2.1.29 in the monograph by Barendregt (Lambda Calculus and its Semantics, 1985). – user5456 Sep 19 '11 at 5:17
@Anton: I suppose I am not too happy about the $\xi$-rule. – Andrej Bauer Sep 19 '11 at 13:02
And I am in turn not too happy that happiness and “heard of”-like answers gain more attention than direct relevant quotes with the corresponding references. – user5456 Sep 20 '11 at 11:34
@Anton: It's a popularity contest, didn't you know? ;-) Anyhow, what's with the $\xi$-rule that gets used in Barendregt. I don't recall anyone dragging the $\xi$-rule into discussion. We only have $\alpha$ and $\beta$. – Andrej Bauer Sep 20 '11 at 14:24

Just to add to Andrej's very good answer: the theory of untyped $\lambda$-calculus with $\beta$ and $\eta$ reduction rules satisfies some very nice properties:

• It is consistent in the sense that there are two terms, for example $\lambda x y.x$ and $\lambda x y.y$ that are not $\beta\eta$ equivalent. This is a consequence of the confluence theorem for $\beta\eta$ reduction.

• It is a maximal consistent theory in the following sense: if $\iota$ is an
equivalence relation on terms such that:

1. It is closed by congruence: $u\ =_\iota\ v \Rightarrow t\ u\ =_\iota\ t\ v$ etc.

2. It equates 2 non $\beta\eta$ equivalent terms that are normal forms: there exists $t$ and $u$ in normal form such that $t=_\iota u$ and $t\neq_{\beta\eta}u$. Then the theory is inconsistent: for every term $t$, $u$ in normal form, $t=_{\beta\eta\iota}u$.

This is a consequence of Böhm's theorem.

-