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$$] |
| [$$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) $$] |
| [$$\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}$$] |
| [$$(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 }$$] |
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) } $$] |
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}$$] |
| [$$ \frac{m\Leftarrow x\in M\;\;\;\;\;\; x\leftarrow m'\in_M E}{M\triangleright E \vdash m \downarrow m' \triangleright M} $$] |
| [$$ \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' } $$] |
| [$$ \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' } $$] |
- 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$].
- 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.
- 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}$].
- 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 $]
- 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.
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.
0 comentarios:
Publicar un comentario