La semántica natural o semántica de paso grande no es más que una relación que a cada programa [$t$] en un contexto [$C$] le proporciona un valor [$v$]. Escribiremos esta relación así [$$C \vdash t \downarrow v$$] y se lee "[$t$] se evalúa a [$v$] bajo el contexto [$C$]". Aunque antes debemos especificar claramente cuáles son las estructuras sintácticas que forman [$t$], [$C$] y [$v$].
Sintaxis
La sintaxis de los programas son términos [$t$] que son a su vez, o bien una variable [$x$], o bien un literal [$l$], o bien un par de términos [$(t.t)$]. Esto se escribe así: [$$t ::= x \mid l \mid ( t . t )$$] Dentro de los literales incluimos la lista vacía [$()$] que permite, junto con el par, formar listas. Una lista [$(1 2 3)$] es realmente [$(1.(2.(3.())))$]. Es decir, el primer componente del par es el término que está en la cabeza de la lista y el segundo componente es otra lista que representa al resto de los términos. Es común llamar a estos componentes "head" y "tail" (cabeza y cola en inglés) o "car" y "cdr". Estos dos últimos nombres tienen una historia más larga.
Los literales son símbolos como [$1, 53, "hola",$] etc. que tienen un valor en sí mismos. Las variables son símbolos como [$x, y, z,$] etc. que requieren un contexto para saber el valor que representan.
La sintaxis de los valores [$v$] es o bien un término [$t$], o bien una clausura [$\lambda ^C t t$], o bien una forma predefinida [$|p|$]. [$$v::=t\mid \lambda^C tt \mid |p|$$] Escribiremos las formas predefinidas entre barras para distinguirlas de las variables y literales, aunque el símbolo que sea [$p$] puede coincidir con ellos.
Los contextos no son más que una colección de vinculaciones de valores a variables.[$$ C::= \emptyset \mid C,x\leftarrow v$$] Construímos los contextos con el contexto vacío [$\emptyset$] al que le vamos agregando vinculaciones de la forma [$x\leftarrow v$]. Aunque la forma correcta de escribir un contexto sea [$\emptyset, x \leftarrow 5, y \leftarrow 8$], omitiremos el [$\emptyset$].
Operaciones sobre contextos
Vamos a necesitar un par de operaciones para trabajar con los contextos. Son muy simples. La primera es el dominio del contexto [$dom\ C$] que nos dice qué variables se han usado en un contexto. [$$ dom\ \emptyset = \emptyset $$][$$ dom(C,x\leftarrow v)=dom(C)\cup\{x\}$$]
La segunda operación busca una variable en un contexto. Lo escribiremos como una relación de pertenencia [$x\leftarrow v \in C$] para simplificar la lectura. [$$x\leftarrow v\in C,x\leftarrow v$$][$$\frac{x\ne x'\;\;\;\;\;\;x\leftarrow v\in C}{x\leftarrow v\in C,x'\leftarrow v'}$$]La primera línea es una regla tan obvia que lo mismo es difícil de entender: [$x\leftarrow v$] pertenece a [$C,x\leftarrow v$]. La segunda regla dice que [$x\leftarrow v$] pertenece a [$C,x'\leftarrow v'$] si [$x$] es distinta a [$x'$] y [$x\leftarrow v$] pertenece a [$C$]. Si llega un momento que [$C=\emptyset$], no podremos usar ninguna de las dos reglas (y por tanto [$x\leftarrow v$] no pertenecerá).
Ajuste de patrones
Llegará un momento en la evaluación en el cual tendremos que relacionar argumentos con parámetros. La forma más inteligente de hacerlo es usando el ajuste de patrones, también llamado asignación desestructurante. El ajuste de patrones que vamos a ver aquí es muy simple: toma un término y un valor, devolviendo las vinculaciones que deberían tener las variables del término para que se ajuste al valor proporcionado. Por ejemplo. Si quiero ajustar [$x$] y [$3$], lo escribiré así [$\{x\mid 3\}$] y el resultado será que la variable [$x$] ha de vincularse al valor [$3$]. Esta vinculación es la que hemos escrito [$x\leftarrow 3$] en los contextos. Como no tenemos contexto al que añadir la vinculación, lo incluiremos en nuestro ajsute de patrones. El resultado es que el ajuste de patrones es una relación [$C\{t\mid v\}=C$]. El ejemplo de arriba se podría completar entonces con [$$z\leftarrow 8\;\{x\mid 3\}=z\leftarrow 8,x\leftarrow 3$$]Más ejemplos serían [$$z\leftarrow 8\;\{(x\; y)\mid (3\;7)\}= z\leftarrow 8,x\leftarrow 3,y\leftarrow 7$$][$$\emptyset\{(x y. z)\mid(1 \; (2 \; 3) \; 4 \; 5 \; 6)\}=x\leftarrow 1,y\leftarrow(2\;3), z\leftarrow(4 \;5 \; 6)$$][$$x\leftarrow 5\{x\mid 5\}=???$$] En el último ejemplo no es posible calcular el ajuste de patrones porque [$x$] ya está definida. ¡Incluso si le vamos a dar el mismo valor! De esta manera cada contexto sólo tendrá una única aparición de cada variable.
Las reglas del ajuste de patrones son muy sencillas. En primer lugar, la regla D-LIT dice que los literales han de coincidir.[$$C\{l\mid l\}=C$$] La regla D-VAR modifica el contexto vinculando la variable, que no está definida previamente, al valor.[$$\frac{x\notin C}{C\{x\mid v\}=C,x\leftarrow v}$$] Finalmente, la regla D-PAIR es meramente estructural.[$$C\{(t_1.t_2)\mid(v_1.v_2)\}=C\{t_1\mid v_1\}\{t_2\mid v_2\}$$]
La evaluación
Llega la hora de dar la relación de evaluación [$C \vdash t \downarrow v$] que antes mencionábamos. Son cuatro reglas. La primera, que llamaremos E-LIT, es para saber el valor de un literal. Es muy sencillo porque es él mismo. [$$C \vdash l \downarrow l$$] La segunda (E-VAR) es para saber el valor de una variable. Necesitamos consultar el contexto.[$$\frac{x\leftarrow v \in C}{C \vdash x\downarrow v}$$] La tercera la usaremos para pares cuya cabeza se evalúe a un valor por predefinido. La llamaremos E-PRE. [$$\frac{C\vdash t_0 \downarrow |p| \;\;\;\;\;\; C\vdash (|p| t_1 \cdots t_n) \rightarrow_\delta v}{C\vdash (t_0 t_1 \cdots t_n)\downarrow v}$$] Aquí hemos usado una relación auxiliar [$C\vdash v\rightarrow_\delta v$] en la que introduciremos la semántica de los valores predefinidos (ver más abajo). Finalmente, la regla E-APP, formaliza el uso de una clausura.[$$\frac{C\vdash t_0 \downarrow \lambda^{C'}t't'' \;\;\;\;\;\; C\vdash (t_1 \cdots t_n) \Downarrow (v_1 \cdots v_n) \;\;\;\;\;\; C' \{ t' \mid (v_1 \cdots v_n) \}\vdash t''\downarrow v}{C\vdash (t_0 t_1 \cdots t_n) \downarrow v}$$] Hemos usado el ajuste de patrones en el último antecedente (a la derecha del todo.) También hemos usado una relación auxiliar [$ C\vdash (t_1 \cdots t_n) \Downarrow (v_1 \cdots v_n) $] que llamaremos de "envoltorio" que lo único que hace es evaluar una lista de términos, término a término, para obtener una lista de valores.
Las reglas de esta relación auxiliar de envoltorio son muy simples. Primero, la lista vacía se envuelve a sí misma. [$$C\vdash () \Downarrow ()$$] Y segundo, un par evalúa su cabeza y envuelve el resto. [$$\frac{C\vdash t_1 \downarrow v_1 \;\;\;\;\;\; C\vdash t_2 \Downarrow v_2}{C \vdash (t_1.t_2) \Downarrow (v_1.v_2)}$$] En general podemos ver la relación de envoltorio como una abreviatura de
[$$C\vdash t_1 \downarrow v_1 \;\;\;\;\;\; C\vdash t_2 \downarrow v_2 \;\;\;\;\;\; \cdots \;\;\;\;\;\; C\vdash t_n \downarrow v_n $$] que escribimos [$$ C\vdash (t_1t_2\cdots t_n) \Downarrow (v_1v_2\cdots v_n)$$]
Formas predefinidas
Las formas predefinidas nos pueden servir para trabajar con los literales. Por ejemplo, la suma se puede formalizar así (llamaremos a esta regla P-ADD): [$$\frac{C\vdash (t_1 \cdots t_n)\Downarrow (N_1 \cdots N_n) }{ C\vdash (|+| t_1 \cdots t_n)\rightarrow_\delta \sum_{k=1}^n{N_k} }$$] Donde los [$N$] mayúsculas han de ser literales de número como el [$3$] o el [$75.82$].
Entre todas las formas es especialmente importante la que genera clausuras. Llamaremos a este valor predefinido[$|\lambda|$] y se define con la regla P-LAMBDA [$$C\vdash (|\lambda| t_1 t_2) \rightarrow_\delta \lambda^Ct_1 t_2 $$] Con esta forma especial podemos definir funciones.
Ejemplos de evaluación
Si usamos un contexto inicial [$$C_0 = lambda \leftarrow |\lambda|, +\leftarrow |+|$$] tenemos suficiente potencia expresiva para calcular el doble de [$3$] (realmente, con lambda y usando la codificación de Church, tenemos la potencia expresiva de un modelo computacional Turing completo). Me he tomado algunas libertades para simplificar la derivación (no he usado la abreviatura del envoltorio y le he dado nombres a los contextos). El resultado es el que sigue (clic para ampliar):
En el contexto inicial podemos incluir más definiciones. Algunas funciones típicas son:[$$car\leftarrow \lambda^{C_0}((x.y))x$$][$$cdr\leftarrow\lambda^{C_0}((x.y))y$$][$$list\leftarrow\lambda^{C_0}xx$$][$$cons\leftarrow\lambda^{C_0}(x y)(x.y)$$] Con este nuevo contexto inicial podemos calcular el segundo elemento de la lista [$(1 2 3)$]. La derivación (omitiendo ya nombres de reglas) es la que sigue:
Hasta aquí por hoy. En la siguiente parte de esta serie permitiremos mutaciones en la vinculación de las variables.
0 comentarios:
Publicar un comentario