Nivel 1 · El cálculo lambda

β-reducción

La reducción β es la base de la evaluación de funciones en el cálculo lambda . Por ejemplo, la expresión $(\lambda x .\, x)\, y$ representa la aplicación de la función identidad $\lambda x .\, x$ al argumento $y$ ; intuitivamente, la función debería devolver el argumento sin cambios. La reducción β formaliza ese paso: se toma el cuerpo de la función (en este caso, $x$ ) y se sustituye la variable ligada por el argumento, usando exactamente la Definición 7.20: $(\lambda x .\, x)\, y \rightarrow_\beta x[x := y] \equiv y.$ Este mecanismo consiste, esencialmente, en aplicar una función y obtener un resultado. Todo el material sigue a Nederpelt y Geuvers (2014) .

Un paso de cómputo

Definición 7.24 (β-reducción de un paso, →β)

La relación $\rightarrow_\beta$ se define por:

Base: $(\lambda x .\, M)\, N \rightarrow_\beta M[x := N]$ .
Compatibilidad: si $M \rightarrow_\beta N$ , entonces $M L \rightarrow_\beta N L$ , $L M \rightarrow_\beta L N$ y $\lambda x .\, M \rightarrow_\beta \lambda x .\, N$ .

Las cláusulas de compatibilidad son las que permiten reducir dentro de un término: un paso de reducción puede aplicarse a cualquier subtérmino con la forma adecuada, no solo al término completo. El siguiente vocabulario da nombre a esas piezas.

Definición 7.25 (Redex y contráctum)

Un término $(\lambda x .\, M) N$ se denomina redex (expresión reducible) y el término $M[x := N]$ se llama su contráctum. La reducción β en un paso, denotada $\rightarrow_\beta$ , consiste en reemplazar un redex por su contráctum.

Ejemplo 7.26 (Un paso, dos rutas y un bucle)

$(\lambda x .\, x(x\, y))\, N \rightarrow_\beta N(N\, y)$ .
En el término $(\lambda x .\, (\lambda y .\, y\, x)\, z)\, v$ hay dos redexes:
- Redex 1: el término completo. $(\lambda x .\, (\lambda y .\, y\, x)\, z)\, v \rightarrow_\beta (\lambda y .\, y\, v)\, z.$
- Redex 2: el subtérmino $(\lambda y .\, y\, x)\, z$ . $(\lambda x .\, (\lambda y .\, y\, x)\, z)\, v \rightarrow_\beta (\lambda x .\, z\, x)\, v.$
Ambos términos resultantes pueden reducirse a un reducto común $z\, v$ :
$(\lambda y .\, y\, v)\, z \rightarrow_\beta z\, v, \qquad (\lambda x .\, z\, x)\, v \rightarrow_\beta z\, v.$
$(\lambda x .\, x\, x)(\lambda x .\, x\, x) \rightarrow_\beta (\lambda x .\, x\, x)(\lambda x .\, x\, x)$ . Este es un caso de reducción infinita, donde la sustitución del argumento en el cuerpo del redex produce el mismo término.

Cero o más pasos

Definición 7.27 (Reducción β en cero o más pasos, ↠β)

Sea $M \twoheadrightarrow_\beta N$ si existen $n \geq 0$ y términos $M_0, M_1, \dots, M_n$ tales que

M_0 \equiv M, \qquad M_n \equiv N, \qquad \text{y} \qquad M_i \rightarrow_\beta M_{i+1} \ \text{ para todo } 0 \leq i < n.

Por lo tanto, si $M \twoheadrightarrow_\beta N$ , existe una cadena de reducciones β de un solo paso que comienza en $M$ y termina en $N$ :

M \equiv M_0 \rightarrow_\beta M_1 \rightarrow_\beta \cdots \rightarrow_\beta M_{n-1} \rightarrow_\beta M_n \equiv N.

El caso $n = 0$ está permitido: todo término se reduce a sí mismo en cero pasos, de modo que $\twoheadrightarrow_\beta$ es reflexiva; concatenando cadenas se comprueba que también es transitiva.

La igualdad β

La reducción tiene una dirección: va del redex al contráctum. Para hablar de términos que computan lo mismo se necesita la relación simétrica generada por la reducción.

Definición 7.28 (Conversión β, igualdad β; =β)

Dos términos $M$ y $N$ son β-convertibles o β-iguales, denotado $M =_\beta N$ , si existe una secuencia de términos $M_0, \dots, M_n$ (con $n \ge 0$ ) tal que $M_0 \equiv M$ , $M_n \equiv N$ y, para todo $i$ con $0 \le i < n$ : $M_i \rightarrow_\beta M_{i+1} \quad \lor \quad M_{i+1} \rightarrow_\beta M_i,$ donde $\lor$ es la disyunción inclusiva: la condición se satisface si $M_i$ se reduce a $M_{i+1}$ , si $M_{i+1}$ se reduce a $M_i$ , o si ambas relaciones se cumplen.

Nota 7.29 (La abreviatura ↔β)

La condición $M_i \rightarrow_\beta M_{i+1} \lor M_{i+1} \rightarrow_\beta M_i$ se abrevia con $M_i \leftrightarrow_\beta M_{i+1}$ . La igualdad $=_\beta$ es entonces la clausura reflexiva y transitiva de $\leftrightarrow_\beta$ , que en la literatura se escribe también $\leftrightarrow_\beta^*$ . En una cadena de conversión los pasos pueden apuntar en direcciones distintas: $=_\beta$ conecta términos «cuesta arriba» y «cuesta abajo» de la reducción.

Ejemplo 7.30 (Dos rutas, una sola meta)

Para demostrar la β-igualdad entre los términos del conjunto

\{\, (\lambda x .\, (\lambda y .\, y\, x)\, z)\, v,\ (\lambda y .\, y\, v)\, z,\ (\lambda x .\, z\, x)\, v,\ z\, v \,\},

basta con mostrar que todos se reducen a la misma forma normal $z\, v$ . El término inicial tiene dos caminos de reducción posibles:

(\lambda x .\, (\lambda y .\, y\, x)\, z)\, v \begin{cases} \rightarrow_\beta (\lambda y .\, y\, v)\, z \rightarrow_\beta z\, v, \\[4pt] \rightarrow_\beta (\lambda x .\, z\, x)\, v \rightarrow_\beta z\, v. \end{cases}

Dado que todos los términos convergen a $z\, v$ (es decir, $M \twoheadrightarrow_\beta z\, v$ para cada uno), son todos β-iguales entre sí. Por ejemplo, $(\lambda y .\, y\, v)\, z =_\beta (\lambda x .\, z\, x)\, v$ porque ambos tienen un reducto en común, aunque ninguno de los dos se reduce al otro.

Pruébalo tú mismo

El reductor ejecuta la Definición 7.24 paso a paso: resalta cada redex disponible, y al contraerlo aplica la sustitución de la Definición 7.20. Escribe el término (\x. (\y. y x) z) v y verifica que las dos rutas del Ejemplo 7.26 desembocan en $z\, v$ ; el preset $\Omega$ muestra el bucle infinito del tercer punto.

Reductor β interactivo

La sustitución sigue la Definición del texto: (λy. P)[x := N] ≡ λz. (P^{y→z}[x := N]) con z ∉ FV(N) ∪ {x}; el renombre se muestra cuando ocurre.

Que las dos rutas del ejemplo converjan no es un accidente: es un teorema, y de los importantes. Antes de llegar a él, la página siguiente estudia qué significa que un cómputo termine, y muestra que no todos lo hacen.