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

Question

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?

Answer 1

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.

Answer 2

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.