Reducciones Lambda

En el Cálculo Lambda, la semántica operacional indica que la evaluación de una expresión es una serie de pasos de reducción donde cada paso siguiente se obtiene por reescritura. Una reducción tiene la forma $f(x)=E[x]⟹f(u)=E[x:=u]$ de manera que cada aparición de $x$ en la expresión se sustituye por $u$.

Dada una expresión reducible $E$, cada reducción de $E$ reemplaza una redex (reducible expression) de acuerdo a ciertas reglas. Existen 4 tipos de reducciones lambda:

1. $\delta$-reducción: transforma constantes evaluando operadores. Ejemplo: $\ast 33\to \delta 9$.
2. $\alpha$-reducción: renombra variables ligadas de expresiones $\lambda$. Matemáticamente, sea $\lambda x.M\stackrel{\alpha }{\to }\lambda y[x:=y]M$ si $y\notin Free(M)$. Esto desambigua identificadores iguales pero en distintos ámbitos, lo que asegura una sustitución segura para evitar problemas en la captura de variables. Ejemplo: $\lambda x(\lambda x.x)\stackrel{\alpha }{\to }\lambda x(\lambda y.y)x$.
3. $\beta -$reducción: sustituye el argumento sobre el cuerpo de la función, reemplazando todas las ocurrencias de la variable instanciada. $(\lambda x.M)N\stackrel{\beta }{\to }[x:=N]M$. Esto aplica un argumento, lo que es similar a llamar la función. Ejemplo: $(\lambda x.\ast xx)2\stackrel{\beta }{\to }(\ast 22)$.
4. $\eta$-reducción: dos funciones son lo mismo si dan el mismo resultado para todos sus argumentos. Matemáticamente, $\lambda x.Mx\stackrel{\eta }{\to }M$ si $x\notin Free(M)\wedge M$ es función. Ejemplo: $(\lambda x.(\lambda y.y))x\stackrel{\eta }{\to }\lambda y.y$.

Un redex es un término de la forma $(\lambda x.M)N$. Dada una $\lambda$-expresión, se dice que está en forma normal si no contiene redexs. No toda $\lambda$-expresión admite una forma normal. Por ejemplo: $(\lambda x.xx)(\lambda y.yy)\stackrel{\beta }{\to }(\lambda y.yy)(\lambda y.yy)\stackrel{\beta }{\to }...$

Órdenes de Reducción

El orden en el que se aplican las reducciones, similar al orden de evaluación, puede ser:

• Impaciente: se reduce desde dentro hacia fuera. Esto permite algunos bucles infinitos.
• Perezoso: se reduce desde lo externo hacia dentro. El orden perezoso siempre termina.

Teoremas de Church-Rosser

Confluencia

$\forall \lambda \text{-expresioˊn}M/M\stackrel{\ast }{\to }P\wedge M\stackrel{\ast }{\to }Q⟹\exists \lambda \text{-expresioˊn}E/P\stackrel{\ast }{\to }E\wedge Q\stackrel{\ast }{\to }E$

flowchart LR;
1[M] --$$*$$--> 2[P]
1 --$$*$$--> 3[Q]
2 --$$*$$--> 4[E]
3 --$$*$$--> 4

Si $M$ admite forma normal $E$, esta es única salvo que se aplique una $\alpha$-reducción (un renombramiento).

Terminación

$\text{si }M\stackrel{\ast }{\to }P\wedge P\text{ en forma normal}⟹\exists M\stackrel{\ast }{\to }P\text{ en orden normal}$

El orden perezoso siempre termina.