Nivel 1 · El cálculo lambda

Sustitución y α-conversión

La operación central del cálculo lambda — aplicar una función a un argumento — se reducirá en la página siguiente a sustituir un término en otro. Esta página define esa operación con total precisión, porque es exactamente el punto donde la intuición «reemplaza $x$ por $N$ » falla si no se tiene cuidado: una variable libre puede quedar capturada por un ligador. Todo el material sigue a Nederpelt y Geuvers (2014) .

El nombre de una variable ligada no importa

Las funciones $\lambda x.\, x$ y $\lambda y.\, y$ son la misma función identidad escrita con distinto nombre de variable. La relación que lo formaliza se construye en dos pasos: primero el renombramiento de una sola variable de enlace, después su clausura.

Definición 7.15 (Renombramiento; M^{x→y})

Sea $M^{x \to y}$ el resultado de reemplazar toda ocurrencia libre de $x$ en $M$ por $y$ . El renombramiento de la variable de enlace $x$ , $\lambda x.\, M =_\alpha \lambda y.\, M^{x \to y},$ está permitido bajo dos condiciones:

$y \notin FV(M)$ — la nueva variable no aparece libre en $M$ , y
$y$ no es variable de enlace en $M$ .

Las dos condiciones no son pedantería. Si $y \in FV(M)$ , el renombre capturaría esa $y$ libre (pasaría a estar ligada, cambiando el significado). Si $y$ ya liga dentro de $M$ , se produce un conflicto de sombreado (shadowing): el nuevo ligador externo chocaría con el interno.

Definición 7.16 (α-equivalencia)

La relación $=_\alpha$ es la menor relación que contiene el renombramiento de la Definición 7.15 y es:

compatible: si $M =_\alpha N$ , entonces $ML =_\alpha NL$ , $LM =_\alpha LN$ y $\lambda z.\, M =_\alpha \lambda z.\, N$ ;
reflexiva, simétrica y transitiva (una relación de equivalencia).

Ejemplo 7.18 (Un renombre válido y dos inválidos)

Sea $M \equiv \lambda x.\, x(\lambda z.\, x\,y)$ , aplicado a $z$ .

$(\lambda x.\, x(\lambda z.\, x\,y))\,z =_\alpha (\lambda u.\, u(\lambda z.\, u\,y))\,z$ — válido: $u \notin FV$ del cuerpo y $u$ no es enlace.
Renombrar $x \mapsto y$ es inválido: $y$ está libre en el cuerpo y quedaría capturada.
Renombrar $x \mapsto z$ en un solo paso es inválido: $z$ ya es variable de enlace en el cuerpo (el $\lambda z$ interior). La conversión a $(\lambda z.\, z(\lambda x.\, z\,y))\,z$ es verdadera, pero exige pasos intermedios que primero liberen el nombre $z$ .

Definición 7.17 (Captura de variables)

Una variable libre queda capturada cuando una operación textual la coloca bajo un ligador $\lambda$ que la ata. Una operación correcta sobre términos lambda debe evitar la captura.

La sustitución, cláusula por cláusula

Definición 7.20 (Sustitución)

Sea $M[x := N]$ el término que resulta de sustituir $N$ por todas las ocurrencias libres de $x$ en $M$ . Se define por recursión sobre $M$ :

Variables:
- (1a) $x[x := N] \equiv N$ ;
- (1b) $y[x := N] \equiv y$ , si $x \not\equiv y$ .
Aplicación: $(P\, Q)[x := N] \equiv (P[x := N])\,(Q[x := N])$ .
Abstracción: $(\lambda y.\, P)[x := N] \equiv \lambda z.\, (P^{y \to z}[x := N])$ , donde $\lambda z.\, P^{y \to z}$ es una variante $\alpha$ de $\lambda y.\, P$ tal que $z \notin FV(N) \cup \{x\}$ .

Nota 7.21 (Observaciones sobre la cláusula (3))

La condición $z \notin FV(N)$ impide la captura: las variables libres de $N$ no deben quedar atadas por el ligador. La condición $z \not\equiv x$ impide que el renombre convierta ocurrencias ligadas en objetivos de la sustitución.
Cuando $y \not\equiv x$ y $y \notin FV(N)$ , no hace falta renombrar: $(\lambda y.\, P)[x := N] \equiv \lambda y.\, (P[x := N])$ .
Cuando $y \equiv x$ , la $x$ no ocurre libre en el cuerpo y la sustitución no hace nada: $(\lambda x.\, P)[x := N] \equiv \lambda x.\, P$ .

Ejemplo 7.22 (Dónde muerde la captura)

Compárense: $(\lambda y.\, x)[x := y] \quad\text{y}\quad (\lambda w.\, x)[x := y].$ En la segunda, la cláusula (3) sin renombre da $\lambda w.\, y$ : una función constante que devuelve la $y$ libre. En la primera, aplicar la cláusula (3) sin renombrar daría $\lambda y.\, y$ (¡la identidad!), capturando la $y$ . La cláusula obliga a elegir $z$ fresco: $(\lambda y.\, x)[x := y] \equiv \lambda z.\, y,$ que es $\alpha$ -equivalente a $\lambda w.\, y$ , como debe ser: los dos términos de partida eran $\alpha$ -equivalentes.

Pruébalo tú mismo

El reductor aplica la Definición 7.20 tal cual: cuando la cláusula (3) exige renombrar, la advertencia α aparece con su justificación. Carga el segundo preset, $(\lambda x.\, \lambda y.\, x\,y)\,y$ , y observa el renombre forzado.

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.

El lema que hace todo componible

Lema 7.23 (Lema de Sustitución)

Sean $x \not\equiv y$ y $x \notin FV(L)$ . Entonces: $M[x := N][y := L] \equiv M[y := L][x := N[y := L]].$

Demostración.

Por inducción sobre la estructura de $M$ ; los casos de variable y aplicación son directos, y el caso de abstracción usa que los renombres de la cláusula (3) pueden elegirse frescos para ambos lados. Los detalles están en Nederpelt y Geuvers (2014) , Lema 1.6.5. Las dos hipótesis son esenciales: sin $x \notin FV(L)$ , el lado derecho re-sustituiría dentro de $L$ ocurrencias de $x$ que el izquierdo jamás toca.

Nota (Convención de identificación módulo α)

De aquí en adelante los términos $\alpha$ -equivalentes se identifican: se escribe $\equiv$ también para la identidad módulo $\alpha$ , como $\lambda x.\, x \equiv \lambda y.\, y$ . Esta convención es distinta de la convención de Barendregt (elegir nombres de variables ligadas distintos entre sí y distintos de las libres); juntas hacen que la cláusula (3) casi nunca necesite renombrar en la práctica.