Nivel 1 · El cálculo lambda

Sintaxis: términos y variables libres

En la matemática usual una función es un conjunto de pares ordenados: un objeto derivado de la teoría de conjuntos. El cálculo lambda , inventado por Church en los años treinta, invierte esa jerarquía: la función es el objeto primitivo, y todo lo demás (números, valores de verdad, estructuras de datos) se codifica con funciones. El objetivo original de Church era fundacional: precisar qué funciones son «computables» mediante un algoritmo, pregunta que respondió en Church (1936) . En lugar de decenas de instrucciones, todo el sistema se resume en tres reglas de formación y una regla de cómputo. Esta página presenta las tres reglas de formación; el material sigue a Nederpelt y Geuvers (2014) .

Las tres reglas que generan todo

Definición 7.1 (El conjunto Λ de los λ-términos)

El conjunto $\Lambda$ de todos los λ-términos se define inductivamente con tres reglas:

Cualquier variable $u \in V$ , donde $V = \{x, y, z, \dots\}$ , es un λ-término. Son los átomos del lenguaje.
Si $M, N \in \Lambda$ , entonces $(M N) \in \Lambda$ (aplicación: el proceso de aplicar una función a un argumento).
Si $u \in V$ y $M \in \Lambda$ , entonces $(\lambda u .\, M) \in \Lambda$ (abstracción: el proceso que permite crear nuevas funciones).

Alternativamente, en notación gramatical BNF: $\Lambda = V \ \mid\ (\Lambda\, \Lambda) \ \mid\ (\lambda V .\, \Lambda),$ donde cada alternativa especifica cómo construir λ-términos a través de variables, aplicaciones y abstracciones.

Nota 7.2 (Convenciones de notación)

Las variables de $V$ se denotan $x, y, z, \dots$
Los λ-términos de $\Lambda$ se denotan $L, M, N, P, Q, R, \dots$
Identidad sintáctica ( $\equiv$ ): dos λ-términos son idénticos si sus estructuras son iguales. Por ejemplo, $x \equiv x$ pero $x \not\equiv y$ ; también $(x\,z) \equiv (x\,z)$ , pero $(x\,z) \not\equiv (x\,y)$ .

La abstracción $\lambda x.\, M$ se lee «la función que a cada $x$ le asigna $M$ »; la aplicación $M N$ se lee « $M$ evaluada en $N$ ». Nótese que la sintaxis permite aplicar cualquier término a cualquier término: nada impide escribir $x\,x$ . Esa libertad tendrá consecuencias importantes más adelante en el módulo.

Nota 7.9 (Convenciones para ahorrar paréntesis)

Para mejorar la legibilidad:

Se pueden omitir los paréntesis más externos: $M N$ significa $(M N)$ y $\lambda x .\, M$ significa $(\lambda x .\, M)$ .
La aplicación es asociativa a la izquierda: $M N L$ se interpreta como $((M N) L)$ .
La abstracción tiene mayor precedencia que la aplicación: $\lambda x .\, M N$ significa $\lambda x .\, (M N)$ .
Abstracciones combinadas: $\lambda x y .\, M$ significa $\lambda x .\, (\lambda y .\, M)$ .

Subtérminos: las partes de un término

Un λ-término complejo está construido a partir de otros más simples. Para analizar y manipular estas expresiones se necesita referirse a las partes que lo forman; a estas partes se les llama subtérminos.

Definición 7.3 (Conjunto de subtérminos, Sub)

Dado un λ-término $P \in \Lambda$ , el conjunto de sus subtérminos, denotado $\operatorname{Sub}(P)$ , se define por inducción sobre la estructura de $P$ , donde $x \in V$ y $M, N \in \Lambda$ :

Variable: $\operatorname{Sub}(x) = \{x\}$ .
Aplicación: $\operatorname{Sub}(M N) = \operatorname{Sub}(M) \cup \operatorname{Sub}(N) \cup \{M N\}$ .
Abstracción: $\operatorname{Sub}(\lambda x .\, M) = \operatorname{Sub}(M) \cup \{\lambda x .\, M\}$ .

Un λ-término $L$ es un subtérmino de $M$ si $L \in \operatorname{Sub}(M)$ .

Nota 7.5 (Demostraciones por inducción estructural)

La técnica de demostración natural sobre conjuntos definidos recursivamente, como $\Lambda$ , es la inducción estructural. La prueba sigue la estructura de la definición inductiva del conjunto y consta de dos partes:

Caso base: se demuestra que la propiedad se cumple para los elementos atómicos (los que no se construyen a partir de otros), como las variables.
Paso inductivo: se demuestra que si la propiedad se cumple para los componentes más simples, también se cumple para los elementos compuestos construidos a partir de ellos: se asume la propiedad para $M$ y $N$ (la hipótesis de inducción) y se prueba para $(M N)$ y $(\lambda x .\, M)$ .

Lema 7.6 (Reflexividad y transitividad de Sub)

Para todos los λ-términos $M$ se tiene:

Reflexividad: $M \in \operatorname{Sub}(M)$ .
Transitividad: si $L \in \operatorname{Sub}(M)$ y $M \in \operatorname{Sub}(N)$ , entonces $L \in \operatorname{Sub}(N)$ .

Demostración.

(1) Reflexividad. Se prueba para cada caso de la inducción estructural:

\begin{cases} M = x \implies x \in \operatorname{Sub}(x), \\ M = (P\, Q) \implies (P\, Q) \in \operatorname{Sub}((P\, Q)), \\ M = (\lambda x .\, P) \implies (\lambda x .\, P) \in \operatorname{Sub}((\lambda x .\, P)), \end{cases}

pues en las tres cláusulas de la Definición 7.3 el propio término pertenece al conjunto. Por lo tanto, $M \in \operatorname{Sub}(M)$ para cualquier $M$ .

(2) Transitividad. Por inducción estructural sobre $N$ .

Caso de variable: sea $N = x$ . Entonces $\operatorname{Sub}(N) = \{x\}$ , de modo que $M \in \operatorname{Sub}(N)$ fuerza $M = x$ , y a su vez $L \in \operatorname{Sub}(M) = \{x\}$ fuerza $L = x$ . Por lo tanto, $L \in \operatorname{Sub}(N)$ .
Caso de aplicación: sea $N \equiv (P\, Q)$ , con $\operatorname{Sub}(N) = \operatorname{Sub}(P) \cup \operatorname{Sub}(Q) \cup \{(P\, Q)\}$ . De $M \in \operatorname{Sub}(N)$ se tienen tres casos. Si $M \in \operatorname{Sub}(P)$ , la hipótesis de inducción sobre $P$ da $L \in \operatorname{Sub}(P) \subseteq \operatorname{Sub}(N)$ . Si $M \in \operatorname{Sub}(Q)$ , la hipótesis de inducción sobre $Q$ da $L \in \operatorname{Sub}(Q) \subseteq \operatorname{Sub}(N)$ . Si $M \equiv (P\, Q)$ , entonces $M \equiv N$ y $L \in \operatorname{Sub}(M)$ es directamente $L \in \operatorname{Sub}(N)$ .
Caso de abstracción: sea $N \equiv (\lambda x .\, P)$ , con $\operatorname{Sub}(N) = \operatorname{Sub}(P) \cup \{(\lambda x .\, P)\}$ . De $M \in \operatorname{Sub}(N)$ se tienen dos casos. Si $M \in \operatorname{Sub}(P)$ , la hipótesis de inducción sobre $P$ da $L \in \operatorname{Sub}(P) \subseteq \operatorname{Sub}(N)$ . Si $M \equiv (\lambda x .\, P)$ , entonces $M \equiv N$ y la conclusión es inmediata.

En todos los casos $L \in \operatorname{Sub}(N)$ .

Ejemplo 7.7 (Subtérminos)

Los subtérminos de $(x\, z)$ son $(x\, z), x, z$ .
El conjunto de subtérminos de $(\lambda x .\, (x\, x))$ es $\{(\lambda x .\, (x\, x)),\ (x\, x),\ x\}$ .
Para $((\lambda x .\, (x\, x))\, (\lambda x .\, (x\, x)))$ , el conjunto es $\{((\lambda x .\, (x\, x))\, (\lambda x .\, (x\, x))),\ (\lambda x .\, (x\, x)),\ (x\, x),\ x\}.$ Obsérvese que, aunque $\operatorname{Sub}(P)$ es un conjunto, un mismo subtérmino puede tener varias ocurrencias en $P$ : aquí $(\lambda x .\, (x\, x))$ ocurre dos veces y $x$ cuatro veces.

Definición 7.8 (Subtérmino propio)

Un subtérmino propio de un λ-término $M$ es cualquier subtérmino $L$ de $M$ tal que $L \not\equiv M$ .

Ocurrencias libres, ligadas y de enlace

Las ocurrencias de variables en un λ-término se dividen en tres categorías. La situación es análoga a la de la variable de integración en $\int_0^1 f(x)\, dx$ o la variable cuantificada en $\forall x\, P(x)$ : la $x$ ahí es un nombre interno, «ligado», mientras que un parámetro que viene del contexto exterior es «libre». En el cálculo lambda, el símbolo $\lambda$ es quien crea esta clasificación:

Las ocurrencias de enlace son las que están inmediatamente después de un símbolo $\lambda$ .
Las demás ocurrencias son libres o ligadas según estén o no dentro del alcance de una abstracción $\lambda$ $λ$ que las ate:
- una variable $x$ es inicialmente libre cuando es usada sola;
- en una abstracción $(\lambda x .\, M)$ , todas las ocurrencias libres de $x$ en $M$ se vuelven ligadas; por esta razón la $x$ inmediatamente después de $\lambda$ se denomina variable de enlace.

Esto lleva a la siguiente definición recursiva.

Definición 7.10 (Conjunto de variables libres, FV)

Dado un λ-término $M$ , el conjunto de variables libres $FV(M)$ se define recursivamente:

(Variable) $FV(x) = \{x\}$ .
(Aplicación) $FV(M N) = FV(M) \cup FV(N)$ .
(Abstracción) $FV(\lambda x .\, M) = FV(M) \setminus \{x\}$ .

Ejemplo 7.11 (Cálculo de FV, cláusula por cláusula)

Mostrar que $FV(\lambda x .\, x\, y) = \{y\}$ :

\begin{aligned} FV(\lambda x .\, x\, y) &= FV(x\, y) \setminus \{x\} && \text{(regla de Abstracción)} \\ &= (FV(x) \cup FV(y)) \setminus \{x\} && \text{(regla de Aplicación en } x\, y\text{)} \\ &= (\{x\} \cup \{y\}) \setminus \{x\} && \text{(regla de Variable en } x \text{ y } y\text{)} \\ &= \{x, y\} \setminus \{x\} = \{y\}. \end{aligned}

Mostrar que $FV(x(\lambda x .\, x\, y)) = \{x, y\}$ :

\begin{aligned} FV\bigl(x(\lambda x.\, x\,y)\bigr) &= FV(x) \cup FV(\lambda x.\, x\,y) && \text{(regla de Aplicación)} \\ &= \{x\} \cup \bigl(FV(x\,y) \setminus \{x\}\bigr) && \text{(regla de Abstracción)} \\ &= \{x\} \cup \bigl((\{x\} \cup \{y\}) \setminus \{x\}\bigr) && \text{(reglas de Aplicación y Variable)} \\ &= \{x\} \cup \{y\} = \{x, y\}. \end{aligned}

Nota 7.12 (FV recoge nombres, no ocurrencias)

La definición de $FV$ recoge todas las variables que son libres en algún lugar del término. Otras ocurrencias de esas mismas variables pueden estar ligadas.
En el término $x(\lambda x .\, x\, y)$ tanto $x$ como $y$ ocurren libres. Sin embargo, solo la primera ocurrencia de $x$ es libre: la ocurrencia después del $\lambda$ es de enlace y la última ocurrencia de $x$ es ligada.

Ejemplo 7.13 (Identificación de ocurrencias)

Considérese $M \equiv (\lambda x .\, x\, y)\, (\lambda z .\, z)$ . Cada ocurrencia de variable se clasifica así:

Ocurrencias de enlace (inmediatamente después de un $\lambda$ ; su función es crear un enlace): la $x$ de $\lambda x$ y la $z$ de $\lambda z$ .
Ocurrencias ligadas (dentro del alcance de una ocurrencia de enlace correspondiente): la $x$ del cuerpo $(x\, y)$ , ligada por $\lambda x$ ; y la $z$ del cuerpo $(z)$ , ligada por $\lambda z$ .
Ocurrencia libre (sin ocurrencia de enlace correspondiente que la alcance): la $y$ , ya que no hay ningún $\lambda y$ en el término.

Términos cerrados

Definición 7.14 (Términos lambda cerrados, Λ⁰)

Considérense las siguientes definiciones:

Un λ-término $M$ es cerrado si $FV(M) = \varnothing$ .
Un λ-término cerrado también se llama combinador.
El conjunto de todos los λ-términos cerrados se denota por $\Lambda^0$ .

Un término cerrado no depende de ningún contexto exterior: es una función autocontenida, como la identidad $\lambda x.\, x$ o la constante $\lambda x y.\, x$ . La siguiente página aborda la operación que da vida a estos términos: la sustitución (Definición 7.20), y con ella el delicado asunto de renombrar variables ligadas sin cambiar el significado.