La Beta de conversión es familiar,$(\lambda x.M)N \rightsquigarrow M[x:=N]$.
Eta conversión es $\lambda x.M x \rightsquigarrow M$ al $M$ no contiene $x$ gratis.
Eta no es un caso especial de la beta, porque no hay ninguna beta redex en cualquier lugar todavía. Se podría decir que se anticipa a la beta redex que surgirán si y cuando la mano izquierda se aplica a algo. En ese punto la reducción de la
$$ (\lambda x.M x) N \rightsquigarrow M N $$
puede ser justificada como una versión beta o una reducción de eta, pero la eta reducción podría suceder antes de que incluso hay un $N$ no. La eta de conversión es intuitivamente justificado por el hecho de que, al final, la única cosa que usted puede realmente hacer con una lambda término para aplicarlo a algo, así que en ese punto no va a importar si ya has eta reducido o no. Así que en ese sentido, eta equivalencia no añade nada fundamentalmente nuevo para el cálculo. La disponibilidad de eta-reducción no cambia si un término tiene una forma normal, por ejemplo.
Eta es, sin embargo, a veces útiles como auxiliar de razonamiento concepto. Por ejemplo, los combinadores $(\lambda y.\lambda x.y x)$ $(\lambda y.y)$ son observacionalmente equivalente -- pero, ¿cómo podemos mostrar que? Simplemente señalar que son $\eta$-equivalente paquetes de una forma un tanto sutil y de largo aliento argumento en un lugar fácilmente reutilizables concepto.
