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?
 A: 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.
A: 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.
