Las reglas del lambda cálculo

El lambda cálculo consta de varias reglas. He puesto aquí las que he encontrado, pero no pretendo ser exhaustivo. Si alguien conoce alguna regla más, estaría encantado de incluirla en la lista.

La regla beta

El lambda cálculo se basa en una regla fundamental: la regla beta.

Esta regla dice que si quiero calcular f(3) y tengo definida f(x), lo que hay que hacer es sustituir x por 3.

[$$ (\lambda x.e)v \rightarrow \left[ x \mapsto v \right] e $$]

La regla alfa

Sin embargo, esto significa que realmente la x puede ser renombrada y si defino f(x) usando la y, tengo la definición equivalente f(y). Esto es cierto, siempre que no tenga usada la y para otra cosa, claro. En la jerga se dice que la y no es libre. Las variables libres de una expresión se capturan con la función "fv".

[$$ \frac {y\not \in fv(e)}{\lambda x.e \rightarrow \lambda y.\left[ x \mapsto y\right] e} $$]

La regla alfa es realmente una equivalencia porque puedo usarla para cambiar la x por la y (u otra variable) y luego usarla de nuevo para volver a la x. Por esa razón se la suele llamar la alfa-equivalencia.

La alfa-equivalencia ocurre siempre que tenemos variables ligadas y captura, junto a la definición de sustitución, ese hecho.

La regla eta

Los estudiosos del lambda cálculo se dieron cuenta de que había ciertas funciones que no podían reducirse con la regla beta, pero que "obviamente" podían reducirse. Era el caso de funciones como f(x)=g(x). Si son iguales, cambia una por otra sea lo que sea x. Como la reducción beta sólo puede cambiar la x por otra cosa, se imponía una nueva regla que dio en llamarse la regla eta.

[$$ \lambda x. (e x) \to e $$]

Esta simple e inocente regla introduce bastantes problemas cuando introducimos otros elementos que no sean funciones. Tantos problemas que los lenguajes de programación actuales no la implementan. Por ejemplo, si e lanzase una excepción, el antecedente de la regla eta no lo haría, mientras que el consecuente sí.

La regla delta

Hemos hablado de lanzar excepciones, pero ¿cómo introducimos esos nuevos valores en el sistema? Las reglas vistas hasta ahora sólo pueden actuar sobre funciones anónimas. Por esa razón se introducen reglas a la carta. Todas estas reglas se agrupan en una única regla, la regla delta, que hace de puente entre las definiciones de los elementos a gusto de usuario y el lambda cálculo.

[$$ \frac{e \rightarrow_\delta e'}{e \rightarrow e'} $$]

La hipótesis de la regla delta es que una expresión e puede reducirse de forma externa a otra expresión e'. En este caso, una expresión e se reduce en el lambda cálculo a la expresión e'.

La regla mu

Finalmente puede ocurrir que queramos introducir valores predefinidos para ciertas variables en nuestra computación. Se incluye entonces un enterno global y se añade la regla mu para poder usar esos valores definidos.

[$$
\frac{x\in dom(\Gamma),\: \Gamma(x)=e}{x\rightarrow e}
$$]

Esta regla sólo se puede usar si la variable no está ligada