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:


$$ 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.