Semántica operacional

La semántica operacional estructural (SOS, también llamada semántica operacional estructurada o semántica de pasos pequeños ) fue introducida por Gordon Plotkin en ( Plotkin81 ) como un medio lógico para definir la semántica operacional. La idea básica detrás de SOS es definir el comportamiento de un programa en términos del comportamiento de sus partes, proporcionando así una visión estructural, es decir, orientada a la sintaxis e inductiva , de la semántica operacional. Una especificación SOS define el comportamiento de un programa en términos de una (o conjunto de) relaciones de transición . Las especificaciones SOS adoptan la forma de un conjunto de reglas de inferencia que definen las transiciones válidas de una pieza compuesta de sintaxis en términos de las transiciones de sus componentes.

Como ejemplo sencillo, consideremos parte de la semántica de un lenguaje de programación simple; en Plotkin81 y Hennessy90 , y otros libros de texto, se ofrecen ilustraciones adecuadas.${\displaystyle C_{1},C_{2}}$abarcar programas del lenguaje y dejar${\displaystyle s}$abarcar estados (por ejemplo, funciones desde ubicaciones de memoria a valores). Si tenemos expresiones (recorridas por${\displaystyle E}$), valores (${\displaystyle V}$) y ubicaciones (${\displaystyle L}$), entonces un comando de actualización de memoria tendría la siguiente semántica:

${\displaystyle {\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}}$

De manera informal, la regla dice que " si la expresión${\displaystyle E}$en el estado${\displaystyle s}$reduce a valor${\displaystyle V}$, luego el programa${\displaystyle L:=E}$actualizará el estado${\displaystyle s}$con la tarea${\displaystyle L=V}$".

La semántica de la secuenciación se puede definir mediante las siguientes tres reglas:

1.${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}}$

2.${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}}$

3.${\displaystyle {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}}$

De manera informal, la primera regla dice que, si el programa${\displaystyle C_{1}}$en el estado${\displaystyle s}$termina en el estado${\displaystyle s'}$, luego el programa${\displaystyle C_{1};C_{2}}$en el estado${\displaystyle s}$se reducirá al programa${\displaystyle C_{2}}$en el estado${\displaystyle s'}$. (Puedes pensar en esto como formalizar "Puedes correr"${\displaystyle C_{1}}$y luego correr${\displaystyle C_{2}}$ utilizando el almacenamiento de memoria resultante.) La segunda regla dice que si el programa${\displaystyle C_{1}}$en el estado${\displaystyle s}$puede reducirse al programa${\displaystyle C_{1}'}$con el estado${\displaystyle s'}$, luego el programa${\displaystyle C_{1};C_{2}}$en el estado${\displaystyle s}$se reducirá al programa${\displaystyle C_{1}';C_{2}}$en el estado${\displaystyle s'}$. (Puedes pensar en esto como la formalización del principio para un compilador optimizador: "Se te permite transformar${\displaystyle C_{1}}$como si fuera independiente, incluso si es solo la primera parte de un programa." La semántica es estructural, porque el significado del programa secuencial${\displaystyle C_{1};C_{2}}$, se define por el significado de${\displaystyle C_{1}}$y el significado de${\displaystyle C_{2}}$.

Si también tenemos expresiones booleanas sobre el estado, abarcadas por${\displaystyle B}$, entonces podemos definir la semántica del comando while : ${\displaystyle {\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}}$

Esta definición permite un análisis formal del comportamiento de los programas, posibilitando el estudio de las relaciones entre ellos. Entre las relaciones importantes se incluyen los preórdenes de simulación y la bisimulación . Estas son especialmente útiles en el contexto de la teoría de la concurrencia .

Gracias a su aspecto intuitivo y su estructura fácil de seguir, SOS ha ganado gran popularidad y se ha convertido en un estándar de facto en la definición de la semántica operacional. Como muestra de su éxito, el informe original (el llamado informe de Aarhus) sobre SOS ( Plotkin81 ) ha atraído más de 1000 citas según CiteSeer., lo que lo convierte en uno de los informes técnicos más citados en Ciencias de la Computación .

La semántica de reducción es una presentación alternativa de la semántica operacional. Sus ideas clave fueron aplicadas por primera vez a variantes puramente funcionales de llamada por nombre y llamada por valor del cálculo lambda por Gordon Plotkin en 1975 ^{[ 3 ]} y generalizadas a lenguajes funcionales de orden superior con características imperativas por Matthias Felleisen en su disertación de 1987. ^{[ 4 ]} El método fue desarrollado posteriormente por Matthias Felleisen y Robert Hieb en 1992 en una teoría completamente ecuacional para el control y el estado . ^{[ 2 ]} La frase "semántica de reducción" fue acuñada por primera vez por Felleisen y Daniel P. Friedman en un artículo de PARLE de 1987. ^{[ 5 ]}

La semántica de reducción se define como un conjunto de reglas de reducción , cada una de las cuales especifica un único paso de reducción potencial. Por ejemplo, la siguiente regla de reducción establece que una instrucción de asignación puede reducirse si se encuentra inmediatamente junto a la declaración de su variable:

${\displaystyle \mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e}$

Para que una instrucción de asignación llegue a tal posición, se "asciende" a través de aplicaciones de funciones y el lado derecho de las instrucciones de asignación hasta que alcanza el punto adecuado. Dado que se interpone${\displaystyle \mathbf {let} }$Las expresiones pueden declarar variables distintas, el cálculo también exige una regla de extrusión para${\displaystyle \mathbf {let} }$expresiones. La mayoría de los usos publicados de la semántica de reducción definen tales “reglas de burbuja” con la conveniencia de los contextos de evaluación. Por ejemplo, la gramática de los contextos de evaluación en un lenguaje simple de llamada por valor se puede dar como

${\displaystyle E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e}$

dónde${\displaystyle e}$denota expresiones arbitrarias y${\displaystyle v}$denota valores totalmente reducidos. Cada contexto de evaluación incluye exactamente un hueco.${\displaystyle [\,]}$en el que se inserta un término de forma que lo capture. La forma del contexto indica, mediante este orificio, dónde puede producirse la reducción. Para describir el “burbujeo” con la ayuda de contextos de evaluación, basta un único axioma:

${\displaystyle E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}}$

Esta regla de reducción única es la regla de elevación del cálculo lambda de Felleisen y Hieb para sentencias de asignación. Los contextos de evaluación restringen esta regla a ciertos términos, pero es aplicable libremente a cualquier término, incluso bajo expresiones lambda.

Siguiendo a Plotkin, demostrar la utilidad de un cálculo derivado de un conjunto de reglas de reducción requiere (1) un lema de Church-Rosser para la relación de un solo paso, que induce una función de evaluación, y (2) un lema de estandarización de Curry-Feys para el cierre transitivo-reflexivo de la relación de un solo paso, que reemplaza la búsqueda no determinista en la función de evaluación por una búsqueda determinista de extremo izquierdo/externo. Felleisen demostró que las extensiones imperativas de este cálculo satisfacen estos teoremas. Como consecuencia de estos teoremas, la teoría ecuacional —el cierre simétrico-transitivo-reflexivo— constituye un principio de razonamiento sólido para estos lenguajes. Sin embargo, en la práctica, la mayoría de las aplicaciones de la semántica de reducción prescinden del cálculo y utilizan únicamente la reducción estándar (y el evaluador que se puede derivar de ella).

La semántica de reducción es particularmente útil dada la facilidad con la que los contextos de evaluación pueden modelar estados o construcciones de control inusuales (por ejemplo, continuaciones de primera clase ). Además, la semántica de reducción se ha utilizado para modelar lenguajes orientados a objetos , ^{[ 6 ]} sistemas de contratos , excepciones, futuros, llamadas por necesidad y muchas otras características del lenguaje. Matthias Felleisen, Robert Bruce Findler y Matthew Flatt ofrecen un tratamiento completo y moderno de la semántica de reducción que analiza en detalle varias de estas aplicaciones en Semantics Engineering with PLT Redex . ^{[ 7 ]}

La semántica operacional estructural de pasos grandes también se conoce con los nombres de semántica natural , semántica relacional y semántica de evaluación . ^{[ 8 ]} La semántica operacional de pasos grandes fue introducida con el nombre de semántica natural por Gilles Kahn al presentar Mini-ML, un dialecto puro de ML .

Las definiciones de pasos grandes pueden considerarse definiciones de funciones o, más generalmente, de relaciones, interpretando cada construcción del lenguaje en un dominio apropiado. Su intuición las convierte en una opción popular para la especificación semántica en lenguajes de programación, pero presentan algunos inconvenientes que las hacen poco prácticas o imposibles de usar en muchas situaciones, como en lenguajes con características de control intensivo o concurrencia. ^{[ 9 ]}

La semántica de grandes pasos describe, mediante la estrategia de divide y vencerás, cómo se pueden obtener los resultados de la evaluación final de las construcciones del lenguaje combinando los resultados de la evaluación de sus contrapartes sintácticas (subexpresiones, subinstrucciones, etc.).