Nivel 1 · El cálculo lambda

Formas normales y no terminación

La β-reducción es el motor de todo el sistema: ejecutar un cómputo en el cálculo lambda es reducir redexes. Pero esa idea plantea preguntas fundamentales, las mismas que valen para cualquier programa de software:

¿Cuándo termina un cálculo? ¿Existe un estado final donde ya no se puede hacer más trabajo?
¿Terminan todos los cálculos? ¿O es posible que algunos entren en bucles infinitos?
Si un cálculo puede realizarse de diferentes maneras (eligiendo qué parte reducir primero), ¿se llegará siempre al mismo resultado?

Las respuestas se encuentran en la teoría de la normalización y la confluencia, siguiendo a Nederpelt y Geuvers (2014) . Esta página responde las dos primeras preguntas; la tercera es el tema de la página siguiente.

El estado final: forma normal

Definición 7.33 (Forma normal β)

Considérese:

Un término $M$ está en forma normal β (o es una β-fn) si no contiene ningún redex. Es decir, no se le pueden aplicar más pasos de reducción β.
Un término $M$ tiene una forma normal β (o es β-normalizable) si existe un término $N$ en forma normal β tal que $M =_\beta N$ . Dicho $N$ se denomina una forma normal β de $M$ .

Nota (Una sutileza: tener forma normal se define con =β)

Los dos sentidos de la definición no son intercambiables. «Estar en» forma normal es una propiedad sintáctica del término; «tener» forma normal se define mediante la conversión $M =_\beta N$ (Definición 7.28), no mediante la reducción $M \twoheadrightarrow_\beta N$ . A priori esto es más débil: una cadena de conversión puede zigzaguear, y nada en la definición garantiza que $M$ pueda reducirse hasta $N$ . Que sí puede (y que la forma normal es única) se demostrará en la página siguiente como consecuencia del Teorema de Church-Rosser (Corolario 7.43 y Corolario 7.44).

Para analizar el proceso de reducción es útil definir formalmente las secuencias de pasos.

Definición 7.34 (Ruta de reducción)

Una ruta de reducción (o camino de reducción) a partir de un término $M$ es una secuencia (finita o infinita) de términos $M_0, M_1, M_2, \dots$ tal que $M_0 \equiv M$ y $M_i \rightarrow_\beta M_{i+1}$ para cada par de términos consecutivos de la secuencia (para todo $0 \le i < n$ si la secuencia es finita con último término $M_n$ ; para todo $i \geq 0$ si es infinita).

La existencia de múltiples redexes en un término implica que puede haber múltiples rutas de reducción. Esto lleva a dos propiedades de terminación importantes.

Definición 7.35 (Normalización débil y fuerte)

Se define:

Un término $M$ es débilmente normalizable si existe al menos una ruta de reducción finita que lleva a una forma normal β.
Un término $M$ es fuertemente normalizable si toda ruta de reducción que comienza en $M$ es finita. Esto implica que no existen rutas de reducción infinitas a partir de $M$ .

Fuertemente normalizable implica débilmente normalizable, pero el recíproco falla, como muestra el tercer punto del siguiente ejemplo. El protagonista es el término $\Omega := (\lambda x .\, x\, x)(\lambda x .\, x\, x),$ la autoaplicación aplicada a sí misma.

Ejemplo 7.36 (Comportamiento de reducción)

Considérense los siguientes ejemplos, que ilustran los conceptos:

Término fuertemente normalizable: el término $(\lambda x .\, (\lambda y .\, y\, x)\, z)\, v$ es fuertemente normalizable. Todas las rutas de reducción posibles terminan en la forma normal $z\, v$ .
Término no normalizable: el término $\Omega$ no es ni siquiera débilmente normalizable. Su única ruta de reducción es un ciclo infinito: $\Omega \rightarrow_\beta \Omega \rightarrow_\beta \dots$
Término débilmente pero no fuertemente normalizable: considérese $M \equiv (\lambda y .\, z)\, \Omega$ $M \equiv (λ y . z) Ω$ . Este término tiene dos redexes: el redex externo (el término completo) y el redex interno ( $\Omega$ $Ω$ ).
- Ruta 1 (finita): si se reduce el redex externo, el cálculo termina inmediatamente: $(\lambda y .\, z)\, \Omega \rightarrow_\beta z.$ Como existe una ruta que lleva a la forma normal $z$ , el término es débilmente normalizable.
- Ruta 2 (infinita): si se elige reducir siempre el redex interno $\Omega$ , el cálculo no termina nunca: $(\lambda y .\, z)\, \Omega \rightarrow_\beta (\lambda y .\, z)\, \Omega \rightarrow_\beta \dots$ La existencia de esta ruta infinita significa que el término no es fuertemente normalizable.

Por qué Ω solo se reduce a sí mismo

La afirmación del punto 2 merece verificarse en detalle. Los subtérminos de $\Omega$ son $x$ , $x\, x$ , $\lambda x .\, x\, x$ y el propio $\Omega$ ; de ellos, el único con la forma $(\lambda x .\, M) N$ de un redex es $\Omega$ completo, con $M \equiv x\, x$ y $N \equiv \lambda x .\, x\, x$ . Contraerlo aplica la sustitución de la Definición 7.20:

\begin{aligned} (\lambda x .\, x\, x)(\lambda x .\, x\, x) &\rightarrow_\beta (x\, x)[x := \lambda x .\, x\, x] && \text{(base de la } \beta\text{-reducción)} \\ &\equiv (x[x := \lambda x .\, x\, x])\,(x[x := \lambda x .\, x\, x]) && \text{(cláusula 2, aplicación)} \\ &\equiv (\lambda x .\, x\, x)(\lambda x .\, x\, x) \equiv \Omega && \text{(cláusula 1a, variable)}. \end{aligned}

El único paso de reducción disponible desde $\Omega$ devuelve exactamente $\Omega$ : toda ruta de reducción a partir de $\Omega$ es $\Omega \rightarrow_\beta \Omega \rightarrow_\beta \dots$ , y como $\Omega$ contiene un redex, nunca está en forma normal. Además $\Omega$ no tiene forma normal: por la Definición 7.28 esto exigiría un $N$ en forma normal con $\Omega =_\beta N$ , y el Corolario 7.43 de la página siguiente daría entonces un reducto común de $\Omega$ y $N$ ; pero el único reducto de $\Omega$ es $\Omega$ , que no está en forma normal, y el único reducto de $N$ es $N$ .

Nota (Vista previa: el orden de evaluación importa)

El punto 3 del Ejemplo 7.36 enseña algo práctico: ante varios redexes, la elección puede decidir entre terminar o no. Un ejemplo clásico con combinadores: sean $K \equiv \lambda x y .\, x$ e $I \equiv \lambda x .\, x$ . El término $K\, I\, \Omega$ tiene una ruta finita si se contrae primero el redex más externo,

K\, I\, \Omega \equiv ((\lambda x y .\, x)\, I)\, \Omega \rightarrow_\beta (\lambda y .\, I)\, \Omega \rightarrow_\beta I,

pero también una ruta infinita si se insiste en reducir $\Omega$ . La estrategia que contrae siempre el redex más a la izquierda y más externo es normalizante: alcanza la forma normal siempre que exista una. Este resultado (el teorema de normalización) no se demuestra en la tesis; véase Barendregt (1984) .

Queda pendiente la tercera pregunta del inicio: un término puede tener múltiples rutas de reducción, y si dos de ellas terminan, ¿pueden desembocar en resultados distintos e incompatibles? La respuesta, en la página siguiente, es el teorema central del cálculo lambda.