Semántica operacional

Categoría de semántica de lenguajes de programación formal

La semántica operacional es una categoría de la semántica formal de los lenguajes de programación en la que ciertas propiedades deseadas de un programa , como la corrección, la seguridad o la protección, se verifican mediante la construcción de pruebas a partir de afirmaciones lógicas sobre su ejecución y procedimientos, en lugar de adjuntar significados matemáticos a sus términos ( semántica denotacional ). La semántica operacional se clasifica en dos categorías: la semántica operacional estructural (o semántica de pequeños pasos ) describe formalmente cómo tienen lugar los pasos individuales de un cálculo en un sistema informático; por oposición, la semántica natural (o semántica de grandes pasos ) describe cómo se obtienen los resultados generales de las ejecuciones. Otros enfoques para proporcionar una semántica formal de los lenguajes de programación incluyen la semántica axiomática y la semántica denotacional .

La semántica operacional de un lenguaje de programación describe cómo se interpreta un programa válido como secuencias de pasos computacionales. Estas secuencias son entonces el significado del programa. En el contexto de la programación funcional , el paso final en una secuencia de terminación devuelve el valor del programa. (En general, puede haber muchos valores de retorno para un solo programa, porque el programa podría ser no determinista , e incluso para un programa determinista puede haber muchas secuencias de cálculo ya que la semántica puede no especificar exactamente qué secuencia de operaciones llega a ese valor).

Quizás la primera encarnación formal de la semántica operacional fue el uso del cálculo lambda para definir la semántica de Lisp . ^[1] Las máquinas abstractas en la tradición de la máquina SECD también están estrechamente relacionadas.

Historia

El concepto de semántica operacional se utilizó por primera vez para definir la semántica de Algol 68. La siguiente declaración es una cita del informe revisado de ALGOL 68:

El significado de un programa en el lenguaje estricto se explica en términos de una computadora hipotética que realiza el conjunto de acciones que constituyen la elaboración de ese programa. (Algol68, Sección 2)

El primer uso del término "semántica operacional" en su significado actual se atribuye a Dana Scott (Plotkin04). Lo que sigue es una cita del artículo seminal de Scott sobre semántica formal, en el que menciona los aspectos "operacionales" de la semántica.

Está muy bien aspirar a un enfoque más "abstracto" y "más limpio" de la semántica, pero si el plan ha de ser bueno, no se pueden ignorar por completo los aspectos operativos. (Scott70)

Aproches

Gordon Plotkin introdujo la semántica operacional estructural, Matthias Felleisen y Robert Hieb la semántica de reducción, ^[2] y Gilles Kahn la semántica natural.

Semántica de pequeños pasos

Semántica operacional estructural

La semántica operacional estructural (SOS, también llamada semántica operacional estructurada o semántica de pequeños pasos ) 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 , sobre la semántica operacional. Una especificación SOS define el comportamiento de un programa en términos de una (conjunto de) relación (es) de transición. Las especificaciones SOS toman 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.

Para un ejemplo simple, consideramos parte de la semántica de un lenguaje de programación simple; se dan ilustraciones adecuadas en Plotkin81 y Hennessy90, y otros libros de texto. Sea range sobre programas del lenguaje, y sea range sobre estados (por ejemplo, funciones desde ubicaciones de memoria hasta valores). Si tenemos expresiones (sobre las que se ha aplicado un rango de ), valores ( ) y ubicaciones ( ), entonces un comando de actualización de memoria tendría la semántica: ${\displaystyle C_{1},C_{2}}$ ${\displaystyle s}$ ${\displaystyle E}$ ${\displaystyle V}$ ${\displaystyle L}$

${\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 en estado se reduce a valor , entonces el programa actualizará el estado con la asignación ". ${\displaystyle E}$ ${\displaystyle s}$ ${\displaystyle V}$ ${\displaystyle L:=E}$ ${\displaystyle s}$ ${\displaystyle L=V}$

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

${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad \quad {\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 }}\quad \quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}}$

De manera informal, la primera regla dice que, si el programa en estado termina en estado , entonces el programa en estado se reducirá al programa en estado . (Puede pensar en esto como la formalización de "Puede ejecutar , y luego ejecutar usando el almacén de memoria resultante). La segunda regla dice que si el programa en estado puede reducirse al programa con estado , entonces el programa en estado se reducirá al programa en estado . (Puede pensar en esto como la formalización del principio para un compilador optimizador: "Se le permite transformar 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 , se define por el significado de y el significado de . ${\displaystyle C_{1}}$ ${\displaystyle s}$ ${\displaystyle s'}$ ${\displaystyle C_{1};C_{2}}$ ${\displaystyle s}$ ${\displaystyle C_{2}}$ ${\displaystyle s'}$ ${\displaystyle C_{1}}$ ${\displaystyle C_{2}}$ ${\displaystyle C_{1}}$ ${\displaystyle s}$ ${\displaystyle C_{1}'}$ ${\displaystyle s'}$ ${\displaystyle C_{1};C_{2}}$ ${\displaystyle s}$ ${\displaystyle C_{1}';C_{2}}$ ${\displaystyle s'}$ ${\displaystyle C_{1}}$ ${\displaystyle C_{1};C_{2}}$ ${\displaystyle C_{1}}$ ${\displaystyle C_{2}}$

Si también tenemos expresiones booleanas sobre el estado, con un rango de , entonces podemos definir la semántica del comando while : ${\displaystyle B}$ ${\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 el análisis formal del comportamiento de los programas, lo que permite el estudio de las relaciones entre programas. Entre las relaciones importantes se encuentran los preordenes 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 a su estructura fácil de seguir, SOS ha ganado una gran popularidad y se ha convertido en un estándar de facto para definir la semántica operacional. Como muestra de su éxito, el informe original (el llamado informe Aarhus) sobre SOS (Plotkin81) ha atraído más de 1000 citas según CiteSeer [1], lo que lo convierte en uno de los informes técnicos más citados en informática .

Semántica de reducció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 las 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 elaborado más a fondo 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" en sí fue acuñada por primera vez por Felleisen y Daniel P. Friedman en un artículo de PARLE 1987. ^[5]

La semántica de reducción se presenta 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 declaración de asignación se puede reducir si se encuentra inmediatamente al lado de su declaración de 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 sentencia de asignación llegue a esa posición, se la “hace subir” a través de aplicaciones de funciones y del lado derecho de las sentencias de asignación hasta que alcanza el punto adecuado. Dado que las expresiones intermedias pueden declarar variables distintas, el cálculo también exige una regla de extrusión para las expresiones. La mayoría de los usos publicados de la semántica de reducción definen esas “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 \mathbf {let} }$ ${\displaystyle \mathbf {let} }$

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

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

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

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

Siguiendo a Plotkin, demostrar la utilidad de un cálculo derivado de un conjunto de reglas de reducción exige (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 con una búsqueda determinista de extremo izquierdo/externo. Felleisen demostró que las extensiones imperativas de este cálculo satisfacen estos teoremas. Las consecuencias de estos teoremas son que la teoría ecuacional (el cierre simétrico-transitivo-reflexivo) es 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 profundidad varias de estas aplicaciones en Semantics Engineering with PLT Redex . ^[7]

Semántica de grandes pasos

Semántica natural

La semántica operacional estructural de grandes pasos 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 grandes pasos fue introducida con el nombre de semántica natural por Gilles Kahn al presentar Mini-ML, un dialecto puro de ML .

Las definiciones de gran paso se pueden considerar como definiciones de funciones o, más generalmente, de relaciones, interpretando cada construcción del lenguaje en un dominio apropiado. Su intuitividad hace que sea una opción popular para la especificación semántica en lenguajes de programación, pero tiene algunas desventajas que hacen que sea inconveniente o imposible de usar en muchas situaciones, como lenguajes con características de control intensivo o concurrencia. ^[9]

Una semántica de gran paso describe de manera divide y vencerás cómo se pueden obtener los resultados finales de la evaluación de construcciones del lenguaje combinando los resultados de la evaluación de sus contrapartes sintácticas (subexpresiones, subenunciados, etc.).

Comparación

Hay una serie de distinciones entre la semántica de pasos pequeños y la de pasos grandes que influyen en si una u otra constituye una base más adecuada para especificar la semántica de un lenguaje de programación.

La semántica de grandes pasos tiene la ventaja de ser a menudo más simple (necesita menos reglas de inferencia) y a menudo corresponde directamente a una implementación eficiente de un intérprete para el lenguaje (de ahí que Kahn las llame "naturales"). Ambas pueden conducir a pruebas más simples, por ejemplo, al probar la preservación de la corrección bajo alguna transformación del programa . ^[10]

La principal desventaja de la semántica de grandes pasos es que los cálculos no terminantes ( divergentes ) no tienen un árbol de inferencia, lo que hace imposible enunciar y demostrar propiedades sobre dichos cálculos. ^[10]

La semántica de pasos pequeños proporciona un mayor control sobre los detalles y el orden de evaluación. En el caso de la semántica operacional instrumentada, esto permite que la semántica operacional siga el rastro y que el semanticista formule y demuestre teoremas más precisos sobre el comportamiento del lenguaje en tiempo de ejecución. Estas propiedades hacen que la semántica de pasos pequeños sea más conveniente para demostrar la solidez de los tipos de un sistema de tipos frente a una semántica operacional. ^[10]

Véase también

• Semántica algebraica
• Semántica axiomática
• Semántica denotacional
• Semántica formal de los lenguajes de programación

Referencias

1. McCarthy, John . «Funciones recursivas de expresiones simbólicas y su cálculo por máquina, parte I». Archivado desde el original el 4 de octubre de 2013. Consultado el 13 de octubre de 2006 .
2. Felleisen, M.; Hieb, R. (1992). "Informe revisado sobre las teorías sintácticas del control secuencial y el estado". Ciencias de la computación teórica . 103 (2): 235–271. doi :10.1016/0304-3975(92)90014-7.
3. Plotkin, Gordon (1975). «Call-by-name, call-by-value and the λ-calculus» (PDF) . Theoretical Computer Science . 1 (2): 125–159. doi : 10.1016/0304-3975(75)90017-1 . Consultado el 22 de julio de 2021 .
4. Felleisen, Matthias (1987). Los cálculos de conversión Lambda-v-CS: una teoría sintáctica del control y el estado en lenguajes de programación imperativos de orden superior (PDF) (PhD). Universidad de Indiana . Consultado el 22 de julio de 2021 .
5. Felleisen, Matthias; Friedman, Daniel P. (1987). "Una semántica de reducción para lenguajes imperativos de orden superior". Actas de la Conferencia Internacional sobre Arquitecturas y Lenguajes Paralelos en Europa. Vol. 1. Springer-Verlag. págs. 206–223. doi :10.1007/3-540-17945-3_12.
6. Abadi, M.; Cardelli, L. (8 de septiembre de 2012). Una teoría de los objetos. ISBN 9781441985989.
7. Felleisen, Matthias; Findler, Robert Bruce; Flatt, Matthew (2009). Ingeniería semántica con PLT Redex. The MIT Press. ISBN 978-0-262-06275-6.
8. Universidad de Illinois CS422
9. Nipkow, Tobias; Klein, Gerwin (2014). Semántica concreta (PDF) . págs. 101–102. doi : 10.1007/978-3-319-10542-0 . Consultado el 13 de marzo de 2024 .
10. Xavier Leroy . "Semántica operacional coinductiva de grandes pasos".

Lectura adicional

• Gilles Kahn . "Semántica natural". Actas del 4º Simposio anual sobre aspectos teóricos de la informática . Springer-Verlag. Londres. 1987.
• Gordon D. Plotkin. Un enfoque estructural de la semántica operacional. (1981) Tech. Rep. DAIMI FN-19, Departamento de Ciencias de la Computación, Universidad de Aarhus, Aarhus, Dinamarca. (Reimpreso con correcciones en J. Log. Algebr. Program. 60-61: 17-139 (2004), preimpresión).
• Gordon D. Plotkin. Los orígenes de la semántica operacional estructural. J. Log. Algebr. Program. 60-61:3-15, 2004. (preimpresión).
• Dana S. Scott. Outline of a Mathematical Theory of Computation, Programming Research Group, Monografía técnica PRG-2, Universidad de Oxford, 1970.
• Adriaan van Wijngaarden et al. Informe revisado sobre el lenguaje algorítmico ALGOL 68 . IFIP. 1968. ([2] ^{[ enlace muerto permanente ]} )
• Matthew Hennessy . Semántica de lenguajes de programación. Wiley, 1990. Disponible en línea.

Enlaces externos

• Medios relacionados con Semántica operacional en Wikimedia Commons