# In Lambda calculus, Is there some alternative equivalence to $\eta$ conversion?

In Lambda calculus, is there some alternative equivalence to $$\eta$$ conversion?

I am reading Hendrik Pieter Barendregt's Introduction to Lambda Calculus. On Page 11, I saw $$\beta$$-reduction, $$\alpha$$-conversion, and $$ξ$$-rules (compatibility rules) which is:

Equality:

$$M = M;$$ $$M = N ⇒ N = M;$$ $$M = N, N = L ⇒ M = L.$$

Compatibility rules:

$$M = M' ⇒ MZ = M' Z;$$ $$M = M' ⇒ ZM = ZM' ;$$ $$M = M' ⇒ λx.M = λx.M' . (ξ)$$

But I do not find $$\eta$$-conversion in the book. Does the book mention $$\eta$$ conversion, possibly under a different name or indirectly via an alternative equivalence? Are $$ξ$$ rules by any chance an alternative equivalence to $$\eta$$ conversion?

No, those notes do not talk about $$\eta$$-conversion or $$\eta$$-reduction at all, not even under a different name.

$$\eta$$-conversion is the least equivalence relation on $$\lambda$$-terms that is closed under compatible rules and contains the following relation ($$\textrm{fv}(M)$$ stands for the set of the free variables of the $$\lambda$$-term $$M$$): \begin{align}\tag{1} \lambda x.M x &=_\eta M & \text{if } x \notin \textrm{fv}(M). \end{align}

$$\eta$$-conversion cannot be derived by the conversion rules presented in those notes. For instance, \begin{align} \lambda x. yx =_\eta y \end{align} but there is no hope to derive that using the conversion rules of those notes.

The main reason why $$\eta$$-conversion is important is that, when joined with $$\beta$$-conversion, it captures the notion of extensionality, which roughly means that $$\beta\eta$$-conversion equates all the $$\lambda$$-terms that ''represent'' the same funciton. Formally, it can be proved that $$M =_{\beta\eta} N$$ if and only if $$MP =_{\beta\eta} NP$$ for every $$\lambda$$-term $$P$$. Said differently (very roughly), up to $$\beta\eta$$-conversion, two $$\lambda$$-terms that always have the same output on the same inputs are equal (it does not matter how they compute that output).

Since the $$\lambda$$-calculus is interesting especially for studying intensional (as opposed to extensional) properties of computation, the lack of $$\eta$$-conversion in those notes is not so harmful.

A good reference for $$\eta$$-conversion (and many other topics about the $$\lambda$$-calculus) is Branedregt's book "The Lambda Calulus: Its Syntax and Semantics", North Holland, 1984.

From what I see, $$\eta$$-reduction is not introduced in the book at all.

The equality and compatibility rules you cited are merely natural consequences of the way $$\beta$$-reduction is defined; these axioms can all be justified on the base of the semantics of the $$\twoheadrightarrow_\beta$$ operation. $$\eta$$-conversion, on the other hand, is an operation on its own, which can not be derived from $$\alpha$$-conversion and $$\beta$$-conversion alone.

The operation of $$\eta$$-reduction is defined as follows:

$$P[\lambda x. M x] \to_\eta P[M]$$, $$\quad$$ if $$x \not \in \mathrm{FV}(M)$$.

Here, $$\to_\eta$$ is reduction in one step. In analogy to the relations $$\twoheadrightarrow_\beta$$ and $$=_\beta$$ defined on p. 23 in your book, the relation $$\twoheadrightarrow_{\beta \eta}$$ is then the transitive closure of the $$\to_\beta$$ and $$\to_\eta$$ operations, that is, $$M \twoheadrightarrow_{\beta \eta} N$$ iff there is a reduction series from $$M$$ to $$N$$ where each step is a $$\to_\alpha$$, $$\to_\beta$$ or $$\to_\eta$$ reduction; and $$=_{\beta \eta}$$, $$\beta\eta$$-convertibility, is the extension of the $$=_\beta$$ relation to include $$\to_\eta$$ and $$\leftarrow_\eta$$ reduction steps.

Intuitively, $$\beta \eta$$-convertibility expresses extensionality, that is, for two $$\lambda$$ terms to be the same, it suffices if they have the same behavior in application to other terms.

"Normal" $$\lambda$$ calculus is intensional, that is, two terms are not necessarily considered equal just because they have the same reduction behavior. The addition of $$\eta$$-conversion provides an extension to the calculus, that is, establishing further equivalences between $$\lambda$$ terms that can not be established on the basis of $$\beta$$-reduction alone, in a way that makes the theory of $$\lambda$$-calculus extensional.
Whether or not you want to include $$\eta$$-conversion in your system depends on which variant of equality you favor. Thinking in terms of ZF set theory and functions as a special kind of relation -- that is, a function seen as a set of tuples representing the course of values of the function, and two sets seen as equivalent if they have all the same elements -- the idea of extensionality (two functions are considered the same if they behave the same on any given input/if the input-output tuples in the set descibing the relation expressed by the function are all the same) might seem natural. However, from a computational/programming perspective, you might not want to consider any two programs the same just because they produce the same output, since they might implement two conceptually different algorithms. In pure $$\lambda$$-calculus without $$\eta$$, two programs which have the same behavior but a different "implementation" would not be considered equivalent.