Posterior a de una extensa búsqueda de datos hemos podido resolver esta dificultad que pueden tener algunos de nuestros lectores. Te ofrecemos la solución y nuestro objetivo es servirte de gran ayuda.
Solución:
La conversión beta es la familiar $(lambda xM)N rightsquigarrow M[x:=N]ps
La conversión Eta es $lambda xM x rightsquigarrow M$ cuando $M$ no contiene $x$ gratis.
Eta no es un caso especial de beta, porque todavía no hay redex beta en ninguna parte. Podrías decir que anticipa la redex beta que surgirá si y cuando el lado izquierdo se aplica a algo. En ese punto la reducción $$ (lambda xM x) N rightsquigarrow MN $$ puede justificarse como una reducción beta o eta, pero la reducción eta podría ocurrir incluso antes de que haya un $N$ allí. La conversión eta es intuitivamente justificado por el hecho de que al final lo único que realmente puedes hacer con un término lambda es aplicarlo a algo, por lo que en ese momento no importará si ya has reducido eta o no. Entonces, en ese sentido, la equivalencia eta no agrega nada fundamentalmente nuevo al cálculo. La disponibilidad de eta-reducción no cambia si un término tiene una forma normal, por ejemplo.
Eta, sin embargo, a veces es útil como concepto auxiliar de razonamiento. Por ejemplo, los combinadores $(lambda y.lambda xy x)$ y $(lambda yy)$ son observacionalmente equivalentes, pero ¿cómo podemos demostrar eso? El simple hecho de señalar que son $eta$-equivalentes empaqueta un argumento un tanto sutil y prolijo en un concepto fácilmente reutilizable.
Otra forma más de responder a esta pregunta es proporcionar la siguiente cita de “Lambda Calculus. Su sintaxis y semántica” (Barendregt, 1981). Sin embargo, dado que solo tengo acceso a su traducción al ruso en este momento, tengo que volver a traducirla al inglés. Lo siguiente es de la Sección 3.3.
El objetivo de la introducción de la reducción de $betaeta$ es proporcionar un axioma para enunciados comprobables en el cálculo $lambda$ extensional. [the $lambda + textext$ theory, where $textext$ stands for the rule $M x = N x Rightarrow M = N$] tal que tendría propiedad de Church-Rosser.
Proposición. $M =_betaeta N Leftrightarrow lambdaeta vdash M = N Leftrightarrow lambda + textext vdash M = N$.
[Its proof is based on the following theorem.]
Teorema (de Curry). Las teorías $lambda + textext$ y $lambdaeta$ son equivalentes… [Its proof consists of two parts: $(textext) Rightarrow (eta)$ and vice versa.]
Una de las razones para considerar el sistema $lambdaeta$ es que tiene cierta propiedad de completitud… [Namely, in the sense of the following theorem.]
Teorema. Sean $M$ y $N$ ambos de forma normal. Entonces, $lambdaeta vdash M = N$, o $lambdaeta + M = N$ es inconsistente…
HP-completa [after Hilbert–Post] Las teorías corresponden a teorías máximas consistentes en teoría de modelos para la lógica de primer orden.