Semántica formal para clausuras léxicas

El lambda cálculo es una herramienta asombrosa. En pocas líneas puedes definir un modelo de computación. Esta simplicidad permite transmitir ideas de manera formal con relativa facilidad. Por esa razón estuve pensando cómo explicar la clausura léxica de manera matemática.

El lambda cálculo con semántica natural

Empezaré por el lambda cálculo con semántica natural (también llamada operacional de paso grande). La sintaxis del lambda cálculo es muy sencilla. [$$t::=x\mid tt\mid \lambda x.t$$] Este tipo de definiciones sintácticas se leen así:

[$t::=$]	Un término (o expresión) es
[$x$]	o bien una variable
[$tt$]	o bien una aplicación de un término sobre otro
[$\lambda x.t$]	o bien una función que toma una variable y devuelve un valor calculado por un término. Esto es a lo que se llama una abstracción lambda o función anónima.

Nota: La aplicación se asocia por la izquierda. Entonces, en vez de escribir [$(((t_1 t_2) t_3) t_4)$] escribimos [$t_1 t_2 t_3 t_4$]. 

Lo que es la semántica es también muy fácil de expresar: un término se convierte en un valor mediante una relación binaria [$t\Downarrow v$]. Los valores [$v$] sólo son un tipo especial de término que se denominan formas normales (nosotros vamos a usar WNF). [$$v::= \lambda x.t \mid x v_1 \cdots v_n$$]  Estas formas normales no se pueden reducir más con las reglas de evaluación con las que vamos a expresar la semántica. Estas reglas son las siguientes:
   

Regla E-VAR[$$x\Downarrow x$$]	Regla E-ABS[$$\lambda x.t \Downarrow \lambda x.t $$]
Regla E-APVAL[$$\frac{\begin{array}{c}t_1 \Downarrow x v_1 \cdots v_k\\t_2 \Downarrow v \end{array}}{t_1 t_2 \Downarrow x v_1 \cdots v_k v}$$]	Regla E-APABS [$$\frac{\begin{array}{c}t_1 \Downarrow \lambda x.t\\t_2 \Downarrow v \\ [x\leftarrow v]t\Downarrow  v'\end{array}}{t_1 t_2 \Downarrow v'}$$]

Como se comprobará, las reglas E-VAR y E-ABS no son complicadas ya que tanto las variables como las abstracciones son valores. El núcleo de todo está en las aplicaciones.
Tanto la regla E-APVAL como la regla E-APABS tienen una forma que recuerda a las fracciones. Esta es una notación usual en lógica para especificar reglas de inferencia e indica que si lo de arriba, que es el antecedente, se cumple, entonces lo de abajo, el consecuente, se debe cumplir.

La regla E-APVAL toma dos términos aplicados el [$t_2$] al [$t_1$]. Si resulta que [$t_1$] tras evaluar tiene un valor que no es una abstracción, lo único que podemos hacer es poner el valor de [$t_2$] detrás de la forma normal, haciéndola un poco más larga. Esto tiene algo más de sentido si, por ejemplo, usamos una variable que se llame [$lista$] y evaluemos algo como [$(lista\ 1\ 7) (2+3)$]. El resultado es la propia [$lista\ 1\ 7$] con un añadido que es el valor de [$2+3$]. Es decir, que [$  (lista\ 1\ 7) (2+3) \Downarrow lista\ 1\ 7\ 5$].

La regla E-APABS también toma dos términos aplicados. Esta vez tiene que ocurrir que [$t_1$] se evalúa a una función [$\lambda x.t$]. Entonces, hay que aplicar el resultado de [$t_2$] que es [$v$] a la función. La forma de hacerlo es sustituir todas las apariciones de [$x$] en [$t$] por [$v$] y calcular el valor que nos da esto. La sustitución la hemos escrito como [$[x\leftarrow v]$].

Entonces, si queremos calcular el doble de 1+3, sería evaluar [$(\lambda x.x+x)(1+3)$]. Usando la regla E-APABS vemos que, efectivamente, [$t_1=  \lambda x.x+x$] y que [$t_1 \Downarrow   \lambda x.x+x $] gracias a la regla E-ABS. Entonces, [$t=x+x$]. Por otra parte, [$t_2=1+3$] y [$t_2 \Downarrow 4$]. Finalmente, la sustitución a realizar es [$[x\leftarrow  4]t = 4+4$]. La evaluación es [$4+4\Downarrow 8$] por lo que [$v'=8$] y podemos decir que ocho es el doble de cuatro: [$$(\lambda x.x+x)(1+3)\Downarrow 8$$]

Nota: ¿Cómo es que estamos usando sumas y números si no los hemos definido? Realmente, sí que lo están. El lambda cálculo permite codificar los números (y muchas más cosas) como funciones. Esta es la llamada codificación de Church.



El lambda cálculo sin sustituciones

El lambda cálculo es Turing completo. Esto quiere decir que cualquier función calculable se puede calcular en él. Esto, por otra parte, no significa que sea eficiente computacionalmente. De hecho, la sustitución es una operación muy costosa: hay que recorrer todo el término en el que queremos sustituir y comparar las variables y manipular grandes trozos de expresión. Las reglas exactas son estas:

[$$[x\leftarrow t]x=t$$]	[$$\frac{x\ne x'}{[x\leftarrow t]x'=x'}$$]
[$$[x\leftarrow t](t_1 t_2)=(  [x\leftarrow t] t_1 ) (   [x\leftarrow t]  t_2 )$$]	[$$[x\leftarrow t]\lambda x.t' =  \lambda x. t' $$]

La última regla está más abajo y es la más divertida porque tiene que evitar capturar las variables. Para hacer esto debe explorar además del término donde se sustituye el término a sustituir. Más coste.
[$$\frac{\begin{array}{c}x\ne x'\\x'\notin fv(t)\end{array}}{[x\leftarrow t]\lambda x'.t' =  \lambda x'. [x\leftarrow t] t' }$$] Todos los creadores de compiladores e intérpretes buscan los métodos más curiosos para evitar la sustitución. Uno de estos métodos es la evaluación por entornos, aunque hay más como las máquinas G, los supercombinadores, etc.

Nosotros vamos a usar la evaluación por entornos que es más simple. La idea es sencilla: no sustituimos, sólo apuntamos lo que hay que sustituir. Lo apuntamos en un entorno que es una colección de vinculaciones de ese tipo. [$$ E::= \emptyset \mid E, x=v $$] Añadimos el entorno a nuestra relación de evaluación de esta manera [$$ E \vdash t \Downarrow v$$] Se podría leer "bajo el entorno [$E$] el término [$t$] se evalúa a [$v$]".

La idea es sencilla, ahora hay que establecer las reglas de evaluación. Un primer intento podría ser éste:

   

Regla E-VAR[$$\frac{x=v \in E}{E\vdash x\Downarrow v}$$]	Regla E-ABS[$$E\vdash\lambda x.t \Downarrow \lambda x.t $$]
Regla E-APVAL[$$\frac{\begin{array}{c}E \vdash t_1 \Downarrow x v_1 \cdots v_k\\ E \vdash t_2 \Downarrow v \end{array}}{E \vdash t_1 t_2 \Downarrow x v_1 \cdots v_k v}$$]	Regla E-APABS [$$\frac{\begin{array}{c} E \vdash t_1 \Downarrow \lambda x.t\\ E \vdash t_2 \Downarrow v \\   E,x=v \vdash t\Downarrow  v'\end{array}}{ E \vdash t_1 t_2 \Downarrow v'}$$]

El truco está en la nueva regla E-VAR que mira en el entorno el valor de la variable encontrada y en la regla E-APABS que introduce en el entorno la vinculación.

Desafortunadamente estas reglas no funcionan.

El problema se observa en la siguiente evaluación [$$\emptyset \vdash (\lambda y.\lambda x.y) 3 \Downarrow v'$$] La regla a aplicar sería E-APABS que me diría que [$$ y=3 \vdash \lambda x.y \Downarrow v'$$] La regla E-ABS terminaría la evaluación incorrectamente [$$ y=3 \vdash \lambda x.y \Downarrow \lambda x.y$$] en vez de la correcta [$\lambda x.3$]. Hay que evitar que se pierda el entorno en la regla E-ABS. Al perder el entorno la expresión [$\lambda x.y$] queda abierta con la variable [$y$] libre. La solución es cerrarla con una clausura. La clausura será léxica porque hemos ido descendiendo por las estructuras sintácticas arrastrando los entornos hasta aquí.

Incluyamos entonces un nuevo término a nuestra sintaxis: las clausuras léxicas. Que son la combinación de una abstracción lambda y un entorno. [$$ t::= x\mid tt \mid \lambda x.t \mid \lambda^E x.t $$] Ahora los valores son [$$ v::= \lambda^E x.t \mid x v_1 \cdots v_k$$] y las reglas de evaluación correctas serían
   

Regla E-VAR[$$\frac{x=v \in E}{E\vdash x\Downarrow v}$$]	Regla E-ABS[$$E\vdash\lambda x.t \Downarrow \lambda^E x.t $$]
Regla E-APVAL[$$\frac{\begin{array}{c}E \vdash t_1 \Downarrow x v_1 \cdots v_k\\ E \vdash t_2 \Downarrow v \end{array}}{E \vdash t_1 t_2 \Downarrow x v_1 \cdots v_k v}$$]	Regla E-APABS [$$\frac{\begin{array}{c} E \vdash t_1 \Downarrow \lambda^{E'} x.t\\ E \vdash t_2 \Downarrow v \\   E',x=v \vdash t\Downarrow  v'\end{array}}{ E \vdash t_1 t_2 \Downarrow v'}$$]

He cambiado la regla E-ABS convirtiendo la abstracción (que es código) en la clausura léxica (que es un valor) y la regla E-APABS que ahora usa el entorno de la clausura en vez del entorno de llamada.

Si evaluamos otra vez   [$$\emptyset \vdash (\lambda y.\lambda x.y) 3 \Downarrow v'$$] obtenemos que [$ v'=\lambda^{y=3}x.y$]. Lo cual me dice que hay una sustitución pendiente de [$y$] por el valor [$3$]. Esta sustitución se hará cuando se aplique la función. No se perderá.

Nota: Hay un pequeñísimo detalle a tener en cuenta en estas nuevas reglas. Si queremos hacer una lista como hicimos antes [$lista\ 1\ (1+1)$] no podremos evaluarla. Eso es así porque la variable [$lista$] no está en el entorno y no podremos aplicar la regla E-VAR. Una solución a esto es añadir un entorno inicial donde [$lista=lista$] de manera que [$ lista=lista \vdash lista\ 1\ (1+1) \Downarrow   lista\ 1\ 2$]. Esto nos debe llevar a pensar que hay dos tipos de variables las de código ([$lista$][$=lista$]) y las de valor ([$lista=$][$lista$]). Haciendo que las variables de valor tengan también entorno ([$x^E$]) abrimos la puerta a las macros higiénicas.