Saltar al contenido

¿Cuál es el punto de la conversión eta en el cálculo lambda?

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.

¡Haz clic para puntuar esta entrada!
(Votos: 0 Promedio: 0)



Utiliza Nuestro Buscador

Deja una respuesta

Tu dirección de correo electrónico no será publicada. Los campos obligatorios están marcados con *