Historia de la gestión de símbolos

PARTE I: COMPILADOR Y VINCULADOR

Hoy en día damos por hecho muchas cosas que han costado muchos años descubrir, usar y pulir. Una de ellas es la gestión de los símbolos. Allá por los años cincuenta, si alguien quería hacer un programa debía escribir el código fuente y, como en estos años los compiladores eran muy simples, directamente te generaban el código ejecutable.

Usualmente el código fuente estaba en tarjetas perforadas y el ejecutable se quedaba en memoria, donde se ejecutaba.

Luego, conforme pasaban los años, los programas se iban haciendo más y más grandes. Recompilar todo cada vez era tedioso y para reutilizar un trozo de código hay que volverlo a escribir. La solución es partir los programas. El problema es que este compilador tan simple no me permite partir los programas.

La solución fue usar dos pasos a la hora de compilar. El primer paso es la compilación a un código intermedio que se denomina código objeto. El código objeto es como el código ejecutable, pero tiene marcas de dónde está cada objeto del código (lo que técnicamente se denomina un símbolo exportado). De ahí el nombre "código objeto". Luego, un segundo paso es el vinculador (o enlazador) que lee esas marcas del código objeto y como si fuera un puzle va componiendo el programa ejecutable final y completo.

Esto causa un problema porque... ¿cómo sabe el código fuente de la parte 1 lo que hay en el código fuente de la parte 2 si puede que incluso hayan sido programados por gente completamente distinta?


PARTE II: SÍMBOLOS Y SÍMBOLOS EXTERNOS

A finales de los sesenta apareción un lenguaje que aún hoy es de los más usados. El lenguaje C. Una de las virtudes del C es que soluciona el problema antes mencionado. La solución que se usa en C es permitir usar objetos sin definirlos. Esto se realiza mediante lo que se denomina la declaración del símbolo. La declaración da toda la información necesaria para usar el símbolo, pero no dice qué es. No lo define.

Lo más usual es declararlos y definirlos que es lo que pongo aquí como ejemplo:

int a=0;

double hipotenusa(double x, double y)
{
   return sqrt(x*x+y*y);
}

El código objeto generado por este código fuente de ejemplo tiene lo que técnicamente se denomina dos símbolos: El símbolo "a" y el símbolo "hipotenusa". Ambos están definidos, es decir, que hay un trozo de ese código objeto que se asigna al símbolo "a" y otro trozo de ese código objeto que se asigna al símbolo "hipotenusa". El trozo del símbolo "a" está a cero. El trozo del símbolo "hipotenusa" tiene el código ejecutable de la función hipotenusa.

El contenido del código objeto sería algo como

Símbolo	Objeto asignado
a	0
hipotenusa	{return sqrt(x*x+y*y);}

Para declarar sin definir los símbolos en C se usa lo siguiente:

extern int a;

double hipotenusa(double x, double y);

El código objeto generado por este código fuente de ejemplo tiene dos símbolos: "a" e "hipotenusa". Ninguno está definido, es decir, que este código objeto sólo tiene una lista de los símbolos sin asignarle ningún objeto. Los símbolos sin objeto asignado tienen que obtenerse del exterior cuando el vinculador recomponga el puzle. Son los llamados símbolos externos, porque se definen en algún otro lugar externo al código fuente donde los declaramos.

Símbolo	Objeto asignado
a	externo
hipotenusa	externo

PARTE III: USANDO SÍMBOLOS EXTERNOS

Ahora ya sabemos cómo declarar y definir una función en código fuente y cómo usarla desde otro código fuente. Bastará declararla sin definirla.

programa_parte1.c

/* Declaramos y definimos */
void mifuncion(void)
{
   puts("Esta función está programa_parte1.c");
}

programa_parte2.c

/* Declaramos pero no definimos (prototipo) */
void mifuncion(void);

void main(void)
{
   puts("Esta función está en programa_parte2.c");
   mifuncion(); /* Se usa mifuncion() con haberla sólo declarado */
}

Primero compilamos

Según el compilador la extensión del código objeto será .o   .obj   .coff, etc. Los códigos objetos generados serán algo así como muestran las siguientes tablas.

programa_parte1.obj

Símbolo	Objeto asignado
mifuncion	{puts("Esta función está programa_parte1.c");}

programa_parte2.obj

Símbolo	Objeto asignado
mifuncion	externo
main	{ puts("Esta función está en programa_parte2.c"); mifuncion(); }

Ahora pasamos el vinculador o enlazador.

El vinculador es lo suficientemente inteligente como para ver que el símbolo "mifuncion" está definido en la parte 1 y es un símbolo externo en la parte 2 donde se usa. Entonces, compone ambas partes haciendo que cuando la función main() llame a mifuncion() lo haga correctamente. Finalmente el símbolo "main" es especial y lo usa como punto de entrada del ejecutable.


PARTE IV: LOS FICHEROS DE INCLUSIÓN

Ahora sólo queda un detalle menor. ¿Vamos a tener que repetir

void mifuncion(void);

cada vez que queramos usar la función mifuncion()? ¿Qué pasará si lo que tengo en el código objeto no es una función sino una biblioteca de cincuenta, cien o mil funciones? ¿Voy a tener que escribir todas las que quiera usar una y otra vez en cada fichero fuente que escriba?

La solución es poner todas las declaraciones en un fichero de cabecera (.h del inglés header). E incluir el fichero con tooodas las definiciones. Esto nos ahorra el escribir cada vez todas las definiciones.

Este uso de los ficheros de inclusión es común en lenguajes como el C y el C++.


PARTE V: LOS MÓDULOS

Realmente, usar un fichero de inclusión es una tontería: ¡ya tenemos los símbolos en el código objeto! ¿No podríamos decir en el código fuente "toma los símbolos de este código objeto"? La respuesta es sí. Existen muchos lenguajes que lo hacen. Entre ellos Java y ActionScript3. A esta acción de extraer símbolos de un código objeto y usarlos en otro código fuente se denomina "importar símbolos". Al código objeto que exporta los símbolos de esta manera se le denomina módulo o paquete.

Existen un par de salvedades a este sistema. En primer lugar, el orden de compilación es importante. Debemos compilar los códigos fuentes de manera que cuando usemos un símbolo, el código objeto que lo contiene haya sido generado previamente. Esto significa que no podemos tener ciclos en el uso de referencia aunque algunos sistemas mezclan el compilador y el vinculador en un único paso para permitir estos ciclos. En segundo lugar, es importante cómo llamamos a los ficheros de código objeto y dónde los ubicamos en el sistema de fichero.

Esto último hace que sea necesaria una jerarquía en los nombres de los módulos, usualmente separados por puntos. Así, un símbolo del sistema de módulos de Java se escribe así "java.lang.NullPointerException" y significa algo como en el directorio "java", en el subdirectorio "lang", el fichero "NullPointerException". Este tipo de nombre de símbolos compuestos de varias partes se llaman nombres completamente cualificados.

Es usual en estos sistemas de módulos que cada fichero sólo pueda definir un símbolo. Aquél que coincide con el nombre del fichero. Hay aquí una rigidez. ¿Podríamos separar los nombres de los ficheros de los nombres de los símbolos?

PARTE VI: LOS ESPACIOS DE NOMBRE

Cuando usamos un nombre cualificado como  "java.lang.NullPointerException" hemos pensado que "java" es un directorio, pero desde el punto de vista del programador no es más que un nombre que contiene otros nombres, entre ellos "lang". Asimismo "lang" contiene "NullPointerException". Por esta razón, es común llamar a "java" y a "java.lang" un espacio de nombres (namespace en inglés). En el caso de Java (y de AS3) los espacios de nombres están relacionados con los directorios.


Sin embargo, en C# y C++ no es así y pueden definirse espacios de nombres en el código fuente. Eso significa que los códigos objetos exportan los símbolos con sus nombres cualificados y el vinculador tiene que ser un poco más inteligente.

Modifiquemos el programa anterior para incluir un espacio de nombre llamado "miespacio" usando C++ y añadiré otra "mifuncion" en "otroespacio". El C++ es exótico porque usa :: para separar los nombres cualificados en vez del punto.

programa_parte1.cpp

/* Declaramos y definimos */
namespace miespacio
{
  void mifuncion(void)
  {
     puts("Esta función está programa_parte1.c y en miespacio");
  }
}

namespace otroespacio
{
  void mifuncion(void)
  {
     puts("Esta función está programa_parte1.c pero en otroespacio");
  }
}

programa_parte2.c

/* Declaramos pero no definimos (prototipo) dentro de miespacio*/
namespace miespacio { void mifuncion(void); }

void main(void)
{
   puts("Esta función está en programa_parte2.c");
   miespacio::mifuncion(); /* Se usa miespacio::mifuncion() pero no otroespacio::mifuncion() */
}

Si ahora miramos los códigos objeto encontramos los siguientes símbolos.

programa_parte1.obj    

Símbolo	Objeto asignado
miespacio::mifuncion	{puts("Esta función está programa_parte1.c y en miespacio");}
otroespacio::mifuncion	{puts("Esta función está programa_parte1.c pero en otroespacio");}

programa_parte2.obj

Símbolo	Objeto asignado
miespacio::mifuncion	externo
main	{ puts("Esta función está en programa_parte2.c"); miespacio::mifuncion(); }

De esta manera no hay relación entre la ubicación del módulo en el sistema de ficheros y los espacios de nombre que contiene. Esto es importante porque ahora podemos mover el módulo de lugar dentro del disco y no hay que modificar el código fuente. 

Semántica natural de LISP - parte 2 - LISP imperativo

En la primera parte de esta serie homenaje a John McCarthy vimos una semántica de LISP sin permitir la modificación ni de los valores ni de las vinculaciones. Era un LISP funcional. En esta parte vamos a introducir esa posibilidad. Es por tanto un LISP imperativo.

La memoria y los contextos

En el momento que introducimos cambios, hemos de manejar estados. El estado con el que trabajaremos será la memoria [$M$]. Esta memoria será el conjunto libremente generado por [$$M::= \emptyset \mid M,m\Leftarrow c$$] Los identificadores [$m$] son las direcciones de memoria y los objetos sintácticos [$c$] son las celdas con el contenido de esa dirección. Veremos la sintaxis de las celdas más abajo.

Usaremos también los identificadores [$E$] como sinónimos a [$m$]. No son una nueva categoría, son la misma categoría sintáctica. Simplemente, vamos a usar [$E$] cuando hablemos de posiciones de memoria que guardan entornos. Esto nos hará mucho más legibles las ecuaciones y reglas a continuación.

Si bien recuerda el lector de la primera parte, esta definición de [$M$] es muy similar a la definición de contexto [$C$] que teníamos. Esta vez, nuestro contexto no podrá tener valores porque todo hemos de guardarlo en la memoria para que pueda ser modificado. Así pues, nuestro contexto ahora será [$$C::=\emptyset \mid C,x\leftarrow m$$] Donde [$x$] son los identificadores de variable.

Operaciones sobre memoria y contextos

Debido a la similitud entre la sintaxis de memoria y contexto, vamos a dar sus operaciones a la vez. La primera operación es el dominio que nos indica qué posiciones de memoria o qué identificadores de variable están en uso.

En primer lugar, la memoria vacía o el contexto vacío tienen un dominio vacío.

[$$dom(\emptyset)=\emptyset$$]

[$$dom(\emptyset)=\emptyset$$]

Para continuar, el dominio de la memoria o el contexto más una asignación de memoria o vinculación de variable se calcula recursivamente.

[$$dom(M,m\Leftarrow c)=dom(M)\cup\{m\}$$]

[$$dom(C,x\leftarrow m)=dom(C)\cup\{x\}$$]

La siguiente operación que vamos a especificar es la pertenencia a memoria o a contexto. El caso base es cuando la propia asignación o vinculación está en la parte más externa de la memoria o contexto.

[$$(m\Leftarrow c)\in(M,m\Leftarrow c)$$]

[$$  (x\leftarrow m)\in(M,x\leftarrow m)  $$]

El caso recursivo ocurre cuando no se encuentra en esa posición externa.

[$$\frac{m\ne m'\;\;\;\;\;\;  (m\Leftarrow c)\in M}{(m\Leftarrow c)\in(M,m'\Leftarrow c')}$$]

[$$\frac{x\ne x'\;\;\;\;\;\;(x\leftarrow c)\in C}{(x\leftarrow m)\in(C,x'\leftarrow m')}$$]

Finalmente, y dado que estamos hablando de mutaciones de memoria, tendremos que introducir las operaciones de cambio de memoria y de contexto. Es similar a la pertenencia, pero con una comprobación extra por si la dirección de memoria o variable que queremos modificar no está usada y, por tanto, hay que añadirla. Empecemos por esta regla extra.

[$$\frac{m\notin dom(M)}{M\langle m\Leftarrow c\rangle=M,m\Leftarrow c}$$]

[$$  \frac{x\notin dom(C)}{C\langle x\leftarrow m\rangle=C,x\leftarrow m}$$]

 Cuando lo que queremos cambiar sí está en el dominio, hemos de buscarlo y cambiarlo.

[$$(M,m\Leftarrow c)  \langle m\Leftarrow c'\rangle= (M,m\Leftarrow c') $$]	[$$  (M,x\leftarrow m)   \langle x\leftarrow m'\rangle =   (M,x\leftarrow m')    $$]
[$$\frac{m\ne m'\;\;\;\;\;\;  m' \in dom(M)}{  (M,m\Leftarrow c)\langle m'\Leftarrow c' \rangle =   (M \langle m'\Leftarrow c' \rangle ,m\Leftarrow c)  }$$]	[$$\frac{x\ne x'\;\;\;\;\;\; x'\in dom(C)}{(C,x\leftarrow m)\langle x'\leftarrow m'\rangle =   (C \langle x'\leftarrow m'\rangle ,x\leftarrow m)   }$$]

Celdas y entornos

Las celdas van a contener los valores del LISP funcional. Además, dado que las vinculaciones de variables van a poder ser modificadas, también vamos a introducir en ellas a los contextos. Su sintaxis es la que sigue [$$c::= l \mid x \mid (m.m) \mid \lambda^Emm \mid |p| \mid C $$] Es decir, que una celda podrá ser o bien un literal [$l$], o bien una variable [$x$], o bien un par [$(m.m)$], o bien una clausura [$\lambda^Emm$], o bien un valor predefinido [$|p|$], o bien un contexto [$C$]. Recordemos que la [$E$] no es más que una dirección de memoria como las [$m$].

Dentro de los literales incluimos la lista vacía que escribiremos [$()$]. Una lista de contextos es un entorno. La operación más importante en los entornos es la búsqueda de la vinculación de una variable. Lo haremos buscando en el contexto en posición de cabeza de la lista y luego, si no se encuentra, usando la recursión en el resto de la lista. Bastan dos reglas para realizar este procedimiento. 

[$$\frac{E\Leftarrow(m'.E')\in M\;\;\;\;\;\;m'\Leftarrow C\in M\;\;\;\;\;\;x\leftarrow m\in C}{x\leftarrow m\in_M E}$$]

[$$\frac{  E\Leftarrow(m'.E')\in M\;\;\;\;\;\;m'\Leftarrow C\in M\;\;\;\;\;\;x\leftarrow m\notin C \;\;\;\;\;\;  x \leftarrow m \in_M E' }{ x\leftarrow m\in_M E }$$]

Las dos reglas de arriba son muy similares. Primero, en ambas reglas, se comprueba que la dirección de memoria [$E$] sea un par y que su primer campo [$m'$] apunte a un contexto [$C$]. Luego, si encontramos la variable en [$C$], ahí está (primera regla) y, si no la encontramos, buscamos en el resto de la lista [$E'$] que es el llamado entorno padre (segunda regla).

Otra operación muy simple, y que más que nada es una abreviatura, es la introducción de un nuevo contexto en un entorno.[$$\frac{m' \notin dom(M)\cup\{m\}}{M\triangleright E\Leftarrow C\mid E' \triangleright M,m'\Leftarrow C, E\Leftarrow (m',E')}$$] Para empezar, usaremos [$M\triangleright$] a la izquierda y [$\triangleright M'$] a la derecha de un juicio cuando quiera indicar que la memoria [$M$] se cambia y como resultado obtenemos la memoria [$M'$]. En este caso, leemos el consecuente como "dada la memoria [$M$], obtengo el entorno [$E$] al introducir un nuevo contexto [$C$] en el entorno padre [$E'$] y la memoria con estos cambios es todo lo que hay a la derecha del [$\triangleright$]".

Relaciones auxiliares de evaluación

En la primera parte introdujimos un par de relaciones auxiliares de evaluación: la desestructuración o ajuste de patrones y el envoltorio. Hemos de adaptar ambas a la introducción de la memoria. Ahora hemos de explorar la memoria en vez de explorar valores. Todo esto hace las reglas un poco más largas, pero en el fondo son exactamente las mismas.

El ajuste de patrones sigue teniendo tres reglas: para literales (la llamaremos P-LIT), para variables (P-VAR) y para pares (P-PAIR).
   

[$$\frac{m\Leftarrow l\in M\;\;\;\;\;\;m'\Leftarrow l\in M}{C\{m\mid m'\}_M=C}$$]

[$$\frac{m\Leftarrow x\in M\;\;\;\;\;\; x\notin dom(C)}{C\{m\mid m'\}_M=(C,x\leftarrow m')}$$]

[$$\frac{m\Leftarrow (m_1.m_2)\in M\;\;\;\;\;\;m'\Leftarrow (m'_1.m'_2)\in M}{C\{m\mid m'\}_M=  C\{m_1\mid m'_1\}_M   \{m_2\mid m'_2\}_M   }$$]

El envoltorio sigue teniendo sus dos reglas: para la lista vacía (la llamaremos W-EMPTY) y para el par (W-PAIR). Esta vez se complica un poco más porque hemos de acarrear las memorias de una evaluación a la siguiente. De esta forma los cambios en la primera evaluación afectan a la segunda evaluación. 

[$$\frac{m\Leftarrow ()\in M}{M\triangleright E \vdash m \Downarrow m \triangleright M}$$]

[$$\frac{m\Leftarrow (m_1.m_2)\in M\;\;\;\;\;\; M\triangleright E \vdash m_1 \downarrow m_1' \triangleright M_1 \;\;\;\;\;\;    M_1\triangleright E \vdash m_2 \Downarrow m_2' \triangleright M_2 \;\;\;\;\;\;\; m' \notin dom(M_2)  }{  M\triangleright E \vdash m \Downarrow m' \triangleright M_2,m'\Leftarrow(m'_1.m'_2) } $$]

 En definitiva, lo que hace el envoltorio es evaluar los operandos para obtener los argumentos. En el proceso crea una lista de argumentos.


La evaluación

Ya tenemos todo lo necesario para la evaluación. Es exactamente igual que la evaluación en la versión funcional sólo que acarreando memorias de una evaluación a la siguiente y usando entornos en vez de contextos.

 

[$$\frac{m\Leftarrow l\in M}{M\triangleright E\vdash m\downarrow m \triangleright M}$$]

La primera regla, que sigue siendo E-LIT, mira lo que hay en la dirección de memoria [$m$] y, si es un literal [$l$], devuelve la propia dirección de memoria como su resultado. Eso significa que el resultado de evaluar un literal es él mismo.

[$$  \frac{m\Leftarrow x\in M\;\;\;\;\;\; x\leftarrow m'\in_M E}{M\triangleright E \vdash m \downarrow m' \triangleright M}  $$]

Esta segunda regla, E-VAR, mira lo que hay en la dirección de memoria y, si es una variable [$x$], busca su vinculación [$m'$] en el entorno [$E$] y devuelve esa vinculación. En ninguna de estas dos reglas se modifica la memoria.
 

[$$  \frac{\begin{array}{c}m\Leftarrow(m_1.m_2)\in M\;\;\;\;\;\;M\triangleright E\vdash m_1 \downarrow m'_1 \triangleright M_1 \;\;\;\;\;\; m'_1 \Leftarrow |p|\in M_1 \\  M_1 \triangleright E \vdash |p|m_2 \rightarrow_\delta m'_2 \triangleright M' \end{array}}{  M\triangleright E \vdash m \downarrow m' \triangleright M'  }  $$]

La regla E-PRE, que trata con los valores predefinidos, es algo más compleja. Primero, la regla observa que [$m$] apunta a un par [$(m_1.m_2)$] en la memoria. Eso significa que hay una combinación y hemos de evaluarla. Evalúa el operador [$m_1$] y observa que su resultado [$m'_1$] apunta a un valor predefinido [$|p|$]. Además, hemos modificado la memoria al evaluar el operador y hemos de buscar en [$M_1$]. Una vez que sabemos que es un valor predefinido, delegamos toda evaluación a la relación delta [$\rightarrow_\delta$] que se encarga de los valores predefinidos. La especificaremos más adelante.

[$$ \frac{  \begin{array}{c}m\Leftarrow(m_1.m_2)\in M\;\;\;\;\;\;M\triangleright E\vdash m_1 \downarrow m'_1 \triangleright M_1 \;\;\;\;\;\; m'_1 \Leftarrow \lambda^{E_c}m_f m_b\in M_1 \\ M_1 \triangleright E \vdash m_2 \Downarrow m'_2 \triangleright M_2 \;\;\;\;\;\;  M_2 \triangleright E' \Leftarrow \emptyset\{m_f \mid m'_2 \}_{M_2} \mid E_c \triangleright M_3 \;\;\;\;\;\;  M_3 \triangleright E' \vdash m_b \downarrow m' \triangleright M' \end{array}}{ M\triangleright E \vdash m \downarrow m' \triangleright M' } $$]

 La última regla, E-APP, es la más compleja y usa prácticamente todas las relaciones auxiliares vistas hasta ahora. Explicaremos lo que hace paso a paso:

1. Los tres primeros antecedentes son exactamente iguales que los de la regla E-PRE. Es decir, comprobamos que es un par, evaluamos el primer componente y descubrimos que es, en este caso, una clausura con entorno de clausura en la dirección de memoria [$E_c$] con parámetros formales en la dirección de memoria [$m_f$] y el código a ejecutar en la dirección de memoria [$m_b$].
2. A continuación, evaluamos los operandos para obtener los argumentos. Esto es justamente lo que hace la relación de envoltorio. Es el primer antecedente de la segunda fila.
3. Una vez que tenemos los argumentos, usamos ajuste de patrones para generar un contexto en el cual estén vinculadas las variables de los parámetros formales [$m_f$] a los argumentos [$m'_2$]. Esta parte es [$\emptyset\{m_f\mid m'_2\}_{M_2}$].
4. Luego, ese contexto se introduce en un nuevo entorno [$E'$] usando como entorno padre el [$E_c$] para obtener la memoria [$M_3$]. Es lo que hace [$ M_2 \triangleright E' \Leftarrow \emptyset\{m_f \mid m'_2 \}_{M_2} \mid E_c \triangleright M_3 $]
5. Entonces, tenemos en la dirección de memoria [$E'$] el entorno donde evaluar el cuerpo de la clausura y obtener el resultado [$m'$] junto con la memoria final [$M'$]. Es lo que hace el último antecedente.

Para ver cómo funciona todo esto, haremos un ejemplo de evaluación.

Ejemplo de evaluación

Aunque va a ser un ejemplo muy simple, la memoria va a estar bastante llena. Para no liarnos voy a usar como identificadores de memoria los valores de la semántica funcional entre corchetes. De esta forma entendemos mejor qué hay en la dirección de memoria [$m_4$] si en vez de escribir [$m_4$] escribo [$[\lambda^{C_0}((x.y))x]$].

Entonces, nuestra memoria [$M_0$] va a ser la siguiente.

[$[C_0]$]	[$\Leftarrow$]	[$list\leftarrow [\lambda^{(C_0)}xx], car\leftarrow [\lambda^{(C_0)}((x.y))x] $]
[$ [\lambda^{(C_0)}xx] $]	[$\Leftarrow$]	[$ \lambda^{[(C_0)]}[x][x]$]
[$ [x] $]	[$\Leftarrow$]	[$x$]
[$ [\lambda^{(C_0)}((x.y))x] $]	[$\Leftarrow$]	[$\lambda^{[(C_0)]}[((x.y))][x]$]
[$ [((x.y))] $]	[$\Leftarrow$]	[$([(x.y)].[()])$]
[$ [(x.y)] $]	[$\Leftarrow$]	[$([x].[y])$]
[$ [y] $]	[$\Leftarrow$]	[$y$]
[$ [(car\ (list\ 1\ 2))] $]	[$\Leftarrow$]	[$([car].[((list\ 1\ 2))])$]
[$ [car] $]	[$\Leftarrow$]	[$car$]
[$ [((list\ 1\ 2))] $]	[$\Leftarrow$]	[$([(list\ 1\ 2)].[()])$]
[$ [(list\ 1\ 2)] $]	[$\Leftarrow$]	[$([list].[(1\ 2)])$]
[$ [()] $]	[$\Leftarrow$]	[$()$]
[$ [list] $]	[$\Leftarrow$]	[$list$]
[$ [(1\ 2)] $]	[$\Leftarrow$]	[$([1].[(2)])$]
[$ [1] $]	[$\Leftarrow$]	[$1$]
[$ [(2)] $]	[$\Leftarrow$]	[$([2].[()])$]
[$ [2] $]	[$\Leftarrow$]	[$2$]
[$ [(C_0)] $]	[$\Leftarrow$]	[$([C_0].[()])$]

Ahora vamos a querer evaluar la dirección de memoria [$m=[(car\ (list\ 1\ 2))]$] en el entorno [$E_0=[(C_0)]$] y usando la memoria [$M_0$]. Necesitaremos hallar los interrogantes de [$$ M_0\triangleright E_0 \vdash m \downarrow\ ????\ \triangleright\ ????$$] Deberemos proceder con la regla E-APP en la cual encontramos que [$[(car\ (list\ 1\ 2))]\Leftarrow ([car].[((list\ 1\ 2))])\in M_0$] Entonces, [$m_1=[car]$] y hemos de evaluar [$$ M_0 \triangleright E_0 \vdash m_1 \downarrow\ ????\ \triangleright\ ????$$] Hay que aplicar la regla E-VAR en la cual obtenemos como resultado la dirección de memoria [$[\lambda^{(C_0)}((x.y))(x)]$].

A continuación hemos de realizar el envoltorio. Aparcamos E-APP(car). Ahora, como [$[((list\ 1\ 2))]\Leftarrow ([(list\ 1\ 2).[()]) \in M_0$] es un par, hay que entrar en W-PAIR. Nos dice que evaluemos el primer componente del par que es[$[(list\ 1\ 2)]$]. Tendremos que usar E-APP otra vez.

Aparcamos W-PAIR(car) y E-APP(car) para entrar en E-APP(list). Como [$[(list\ 1\ 2)]\Leftarrow ([list].[(1\ 2)]) \in M_0$], la regla E-APP me dice que evalúe el primer componente del par. En este caso [$[list]$]. Aplicando E-VAR obtenemos que el resultado es la celda [$\lambda^{[(C_0)]}[x][x]$] y tengo que entrar en envoltorio otra vez.

Tenemos en suspenso E-APP(list), W-PAIR(car) y E-APP(car). Y estamos trabajando con W-PAIR para envolver [$[(1\ 2)]\Leftarrow ([1].[(2)])\in M_0$]. Esta regla me dice que evalúe el primer componente que por E-LIT es él mismo [$[1]$] y que vuelva a aplicar el envoltorio sobre el segundo componente [$[(2)]$]. Aparco este W-PAIR(1) y voy con W-PAIR otra vez.

En este punto están en suspenso W-PAIR(1), E-APP(list), W-PAIR(car) y E-APP(car). Seguimos trabajando con la memoria [$M_0$] y hemos de aplicar W-PAIR a [$[(2)]\Leftarrow ([2].[()])\in M_0$]. El resultado es que [$[2]$] se evalúa por E-LIT a él mismo y W-EMPTY me devuelve el propio [$[()]$].

Ahora ocurre una cosa muy importante. La regla W-PAIR modifica la memoria. Añade un par en una nueva dirección. El primer componente del par es el resultado de la evaluación del primer componente, que era [$[2]$] y el segundo, el del envoltorio, que era [$[()]$]. Entonces, mi nueva memoria será [$$M_1=M_0,m_0\Leftarrow ([2].[()])$$] y el resultado de W-PAIR es [$$ M_0 \triangleright E_0 \vdash [(2)] \Downarrow m_0 \triangleright M_1$$] Este cambio de memoria es importante porque ahora recuperamos W-PAIR(1) y usa [$M_1$] en vez de [$M_0$].

Nota: Escribo [$m_0$] en vez de [$[(2)]$] porque [$[(2)]$] ya está usado en [$M_0$] y se confundiría. Tenemos dos celdas con el mismo contenido en memoria.

Retomamos W_PAIR(1) y sigue en suspenso E-APP(list), W-PAIR(car) y E-APP(car). La regla W_PAIR vuelve a modificar la memoria. En este caso [$$M_2=M_1,m_1\Leftarrow ([1].m_0)$$] y lo que hemos demostrado es [$$ M_0 \triangleright E_0 \vdash [(1\ 2)] \Downarrow m_1 \triangleright M_2$$].

Retomamos E-APP(list) y sigue en suspenso W-PAIR(car) y E-APP(car). El siguiente antecedente de la regla E-APP es el que realiza el ajuste de patrones. En este caso hemos de ajustar [$\emptyset\{[x]\mid m_2\}_{M_2}$]. Es sencillo usando la regla P-VAR. El ajuste devuelve el contexto [$C_1=x\leftarrow m_2$].

A continuación, la regla E-APP introduce el nuevo contexto [$C_1$] en la memoria. La nueva memoria es [$$M_3=M_2, [C_1]\Leftarrow C_1, [(C_1 C_0)]\Leftarrow ([C_1].[(C_0)]$$] y el nuevo entorno está en [$[(C_1 C_0)]$]. En este nuevo entorno y con esta nueva memoria evaluamos el cuerpo de la clausura que era [$[x]$]. Usamos para ello la regla E-VAR y encontramos que [$x\leftarrow m_2 \in_{M_3} [(C_1 C_2)]$] por lo que el resultado es [$m_2$] con la propia memoria [$M_3$]. Entonces lo que hemos demostrado hasta ahora es que [$$ M_0 \triangleright E_0 \vdash [(list\ 1\ 2)] \downarrow m_2 \triangleright M_3 $$]

Retomemos W-PAIR(car) y mantengamos en suspenso E-APP(car). La regla W-PAIR, tras evaluar el primer componente del par, envuelve el segundo. Usando la regla W-EMPTY obtenemos [$[()]$] como resultado de este envoltorio. A continuación, modifica la memoria incluyendo un nuevo par en [$m_3$] con ambos resultados. Es decir que [$M_4=M_2,m_3\Leftarrow (m_2.[()])$] y hemos demostrado que [$$ M_0 \triangleright E_0 \vdash [((list\ 1\ 2))] \Downarrow m_3 \triangleright M_4$$]

Retomamos, por fin, E-APP(car). Hemos de realizar primero el ajuste de patrones en el cual obtenemos el contexto [$C_2=x\leftarrow [1],y\leftarrow m_1$]. Luego, incluimos un nuevo entorno en la memoria con ese contexto y con entorno padre el de la clausura. [$$M_5=M_4, [C_2]\Leftarrow C_2, [(C_2 C_0)]\Leftarrow ([C_2].[(C_0)])$$] Y, finalmente, evaluamos el cuerpo de la clausura. Es sencillo porque consta únicamente de una variable y aplicamos E-VAR. Demostramos, por fin, que [$$M_0 \triangleright E_0 \vdash [(car\ (list\ 1\ 2))] \downarrow [1] \triangleright M_5$$]

Valores predefinidos y formas especiales

Especificaremos muy pocas formas predefinidas. La más usual en un lenguaje imperativo es la evaluación en secuencia. Usaremos el valor predefinido [$|begin|$] para esta evaluación. Necesitamos tres reglas. La primera dice que la evaluación en secuencia de la lista vacía es la propia lista vacía.[$$\frac{m\Leftarrow ()\in M}{M\triangleright E \vdash |begin|m \rightarrow_\delta m \triangleright M}$$] La segunda regla indica que si la lista a evaluar en secuencia sólo tiene un elemento, el resultado es la evaluación de ese elemento. [$$\frac{m\Leftarrow (m_1.m_2)\in M \;\;\;\;\;\; m_2\Leftarrow () \in M \;\;\;\;\;\; M \triangleright E \vdash m_1 \downarrow m' \triangleright M'}{M\triangleright E \vdash m \rightarrow_\delta m' \triangleright M'}$$]Finalmente, si hay más de un elemento, evaluamos el primero y evaluamos en secuencia el resto.[$$\frac{m\Leftarrow (m_1.m_2)\in M \;\;\;\;\;\; m_2\Leftarrow () \notin M \;\;\;\;\;\; M \triangleright E \vdash m_1 \downarrow m'_1 \triangleright M_1 \;\;\;\;\;\; M_1 \triangleright E \vdash |begin|m_2 \rightarrow_\delta m' \triangleright M'}{M\triangleright E \vdash m \rightarrow_\delta m' \triangleright M'}$$]

Para definir una vinculación usamos el valor predefinido [$|def!|$].[$$\frac{m\Leftarrow (m_1.m_2) \in M \;\;\;\;\;\; m_1 \Leftarrow x \in M \;\;\;\;\;\; M \triangleright E \vdash |begin|m_2 \rightarrow_\delta m' \triangleright M'}{ M\triangleright E \vdash |def!|m \rightarrow_\delta m' \triangleright M' \langle E \Leftarrow x \leftarrow m'\rangle}$$] La relación auxiliar [$M \langle E \Leftarrow x \leftarrow m\rangle$] es la que realmente modifica la memoria con la nueva definición.[$$\frac{E\Leftarrow (m_1.E_2)\in M \;\;\;\;\;\; m_1 \Leftarrow C \in M}{M \langle E \Leftarrow x \leftarrow m\rangle = M\langle M_1 \Leftarrow C \langle x \leftarrow m \rangle \rangle}$$]

Es posible definir el valor predefinido [$|set!|$] que modifica una vinculación preexistente. La dificultad de esta definición estriba en hacerla recursiva (hacia el entorno padre) si no se halla la variable a modificar en el contexto actual.