Nivel 1 · El cálculo lambda

Confluencia: Church–Rosser

Un término puede tener múltiples rutas de reducción. Esto sería un problema potencial para cualquier sistema de cálculo: si se toman dos caminos diferentes, ¿podría llegarse a dos resultados finales distintos e incompatibles? Si la respuesta fuera sí, el cálculo lambda sería impredecible y poco confiable como modelo de computación. Afortunadamente, la respuesta es no, debido a la siguiente propiedad.

El teorema

Teorema 7.37 (Church-Rosser o Confluencia)

Si un término $M$ se β-reduce en cero o más pasos a $N_1$ y también a $N_2$ , entonces existe un término común $L$ al que tanto $N_1$ como $N_2$ pueden reducirse. Formalmente:

\text{si } M \twoheadrightarrow_\beta N_1 \text{ y } M \twoheadrightarrow_\beta N_2, \text{ entonces existe un } L \text{ tal que } N_1 \twoheadrightarrow_\beta L \text{ y } N_2 \twoheadrightarrow_\beta L.

Esta propiedad se conoce como la propiedad del diamante, porque el enunciado se dibuja como un rombo. En el vértice superior está $M$ ; los dos lados superiores son las dos reducciones dadas por hipótesis, que divergen hacia $N_1$ y $N_2$ ; los dos lados inferiores son las reducciones cuya existencia garantiza el teorema, que vuelven a converger en $L$ :

\begin{array}{ccccc} & & M & & \\ & \swarrow & & \searrow & \\ N_1 & & & & N_2 \\ & \searrow & & \swarrow & \\ & & L & & \end{array}

Las cuatro flechas del diagrama representan reducciones en cero o más pasos, $\twoheadrightarrow_\beta$ ; en la tesis, las dos inferiores se dibujan punteadas para señalar que son las que el teorema construye.

Nota 7.38 (Dónde está la demostración completa)

La demostración de este teorema se puede encontrar en Barendregt (1984) , Teorema 3.2.8; allí la demostración se basa en la Definición 3.2.3 y los Lemas 3.2.4 y 3.2.6.

El esbozo de Tait y Martin-Löf

La demostración directa del Teorema de Church-Rosser es notablemente compleja. La estrategia moderna y más intuitiva, debida a Tait y Martin-Löf, consiste en introducir una relación de reducción auxiliar, más fuerte, llamada reducción paralela, denotada por $\Rightarrow$ . Para un tratamiento exhaustivo del cálculo lambda y sus propiedades, la obra de Barendregt (1984) sigue siendo la referencia más completa. El esbozo consta de tres pasos.

Paso 1: definir la reducción paralela

La relación $M \Rightarrow N$ formaliza la idea de reducir simultáneamente cero o más redexes. Se define inductivamente sobre la estructura de los términos.

Definición 7.39 (Reducción paralela, ⇒)

La relación $M \Rightarrow N$ se define por las siguientes reglas:

(Variable) $x \Rightarrow x$ .
(Abstracción) Si $M \Rightarrow M'$ , entonces $(\lambda x .\, M) \Rightarrow (\lambda x .\, M')$ .
(Aplicación) Si $M \Rightarrow M'$ y $N \Rightarrow N'$ , entonces $(M N) \Rightarrow (M' N')$ .
(Contracción paralela) Si $M \Rightarrow M'$ y $N \Rightarrow N'$ , el redex principal también puede contraerse: $(\lambda x .\, M)\, N \Rightarrow M'[x := N']$ .

De las cláusulas 1 a 3 se sigue, por inducción estructural, que $M \Rightarrow M$ para todo $M$ ; la cláusula 4 permite además contraer un redex mientras, en paralelo, se reducen su cuerpo y su argumento.

Paso 2: los lemas fundamentales para ⇒

Esta nueva relación tiene propiedades muy convenientes, que se enuncian aquí sin demostración; las pruebas pueden consultarse en Barendregt (1984) .

Lema 7.40 (Lema de sustitución para ⇒)

Si $M \Rightarrow M'$ y $N \Rightarrow N'$ , entonces $M[x := N] \Rightarrow M'[x := N']$ .

Lema 7.41 (Lema del diamante para ⇒)

La relación $\Rightarrow$ satisface la propiedad del diamante. Es decir, si $M \Rightarrow N_1$ y $M \Rightarrow N_2$ , entonces existe un término $L$ tal que $N_1 \Rightarrow L$ y $N_2 \Rightarrow L$ .

Paso 3: conclusión

La demostración finaliza conectando $\Rightarrow$ con la reducción β estándar, mostrando que sus clausuras transitivas son equivalentes. Un resultado general de la teoría de reescritura afirma que si una relación ( $\Rightarrow$ ) satisface la propiedad del diamante, su clausura transitiva ( $\twoheadrightarrow_\beta$ ) también la satisface, probando así la confluencia.

Ejemplo 7.42 (Ilustración de la confluencia)

Considérese de nuevo el término $M \equiv (\lambda x .\, (\lambda y .\, y\, x)\, z)\, v$ . Este término tiene dos redexes, lo que da lugar a dos rutas de reducción iniciales:

Ruta 1 (reduciendo el redex externo $(\lambda x .\, \dots)\, v$ ): $M \rightarrow_\beta (\lambda y .\, y\, v)\, z =: N_1.$
Ruta 2 (reduciendo el redex interno $(\lambda y .\, \dots)\, z$ ): $M \rightarrow_\beta (\lambda x .\, z\, x)\, v =: N_2.$

El Teorema de Church-Rosser asegura que $N_1$ y $N_2$ deben converger. Efectivamente, ambos se reducen a un término común $L$ :

a partir de $N_1$ : $(\lambda y .\, y\, v)\, z \rightarrow_\beta z\, v$ ;
a partir de $N_2$ : $(\lambda x .\, z\, x)\, v \rightarrow_\beta z\, v$ .

De la reducción a la conversión

Una primera consecuencia del Teorema de Church-Rosser extiende la confluencia de la reducción a la conversión $=_\beta$ (Definición 7.28). Es este puente el que se necesita para la unicidad de las formas normales, pues «forma normal de $M$ » se definió mediante $M =_\beta N$ , no mediante $M \twoheadrightarrow_\beta N$ (Definición 7.33).

Corolario 7.43 (Church–Rosser para la conversión)

Si $M =_\beta N$ , entonces existe un término $L$ tal que $M \twoheadrightarrow_\beta L$ y $N \twoheadrightarrow_\beta L$ .

Demostración.

Por inducción sobre la longitud de la cadena de conversión $M \equiv M_0 \leftrightarrow_\beta M_1 \leftrightarrow_\beta \cdots \leftrightarrow_\beta M_k \equiv N$ . Si $k = 0$ , basta $L \equiv M$ . Para el paso inductivo, la hipótesis de inducción da $L'$ con $M \twoheadrightarrow_\beta L'$ y $M_{k-1} \twoheadrightarrow_\beta L'$ . Si $M_k \rightarrow_\beta M_{k-1}$ , entonces $M_k \twoheadrightarrow_\beta L'$ y se toma $L \equiv L'$ . Si $M_{k-1} \rightarrow_\beta M_k$ , el Teorema 7.37 aplicado a $M_{k-1}$ (que se reduce a $L'$ y a $M_k$ ) da un $L$ con $L' \twoheadrightarrow_\beta L$ y $M_k \twoheadrightarrow_\beta L$ ; componiendo, $M \twoheadrightarrow_\beta L' \twoheadrightarrow_\beta L$ .

Corolario 7.44 (Unicidad de la forma normal)

Un λ-término tiene como máximo una forma normal β.

Demostración.

Sean $N_1, N_2$ formas normales β de $M$ , es decir, $M =_\beta N_1$ y $M =_\beta N_2$ con $N_1, N_2 \in \beta\text{-fn}$ . Por simetría y transitividad, $N_1 =_\beta N_2$ , y por el Corolario 7.43 existe un término $L$ tal que $N_1 \twoheadrightarrow_\beta L \quad\text{y}\quad N_2 \twoheadrightarrow_\beta L.$ Como una forma normal carece de redexes, solo se reduce (en cero pasos) a sí misma:

N_1 \twoheadrightarrow_\beta L \implies N_1 \equiv L, \qquad N_2 \twoheadrightarrow_\beta L \implies N_2 \equiv L.

De $N_1 \equiv L \equiv N_2$ se concluye $N_1 \equiv N_2$ . Por lo tanto, un λ-término tiene como máximo una forma normal β.

La unicidad justifica el artículo definido: cuando un término es normalizable puede hablarse de la forma normal, el resultado del cómputo, independiente del orden en que se contraigan los redexes. Con la sintaxis, la sustitución, la reducción y la confluencia en su lugar, el cálculo lambda no tipado está completo como modelo de computación. La última página del módulo examina qué le falta para servir de fundamento a la lógica y a las matemáticas: los tipos.