Semántica operacional

Semántica
LingüísticoLógico
Análisis Computacional Léxico ( léxico lexicología ) Estadístico Estructural Teoría de prototipos Dinámica de fuerza Problemas lingüísticos no resueltos Teoría de descripciones
Informática
Tipos Acción Algebraico Axiomático Categórico Concurrencia Denotacional Juego Operacional Predicado transformacional Teoría Interpretación abstracta Gráfico semántico abstracto Coincidencia semántica Análisis Latente Aprendizaje automático Aplicaciones Sistema de archivos semántico Web semántica Wiki semántico
Idioma Lingüística
v t mi

La semántica operacional es una categoría de la semántica del lenguaje de programación formal 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 declaraciones 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 los pasos individuales de un cálculo tienen lugar en un sistema basado en computadora; por oposición semántica natural (osemántica de gran paso ) describen 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 operativa 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 de 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 operativa 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 operativa se utilizó por primera vez para definir la semántica de Algol 68 . La siguiente declaración es una cita del informe ALGOL 68 revisado:

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 operativa" en su significado actual se atribuye a Dana Scott ( Plotkin04 ). Lo que sigue es una cita del artículo fundamental de Scott sobre semántica formal, en el que menciona los aspectos "operativos" de la semántica.

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

Enfoques

Gordon Plotkin introdujo la semántica operacional estructural, Robert Hieb y Matthias Felleisen los contextos 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 operativa. Una especificación SOS define el comportamiento de un programa en términos de una (serie de) relaciones 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; Las ilustraciones adecuadas se dan en Plotkin81 y Hennessy90 , y en otros libros de texto. Dejemos que se extiendan sobre los programas del lenguaje y dejemos que se extiendan sobre los estados (por ejemplo, funciones desde ubicaciones de memoria hasta valores). Si tenemos expresiones (ordenadas por ), valores ( ) y ubicaciones ( ), entonces un comando de actualización de memoria tendría 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 estar dada por 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 el estado termina en el estado , entonces el programa en el estado se reducirá al programa en el estado . (Puede pensar en esto como formalizar "Puede ejecutar , y luego ejecutar usando el almacenamiento de memoria resultante). La segunda regla dice que si el programa en estado puede reducir al programa con estado , entonces el programa en estado se reducirá a la programa en estado . (Puede pensar en esto como formalizar el principio para un compilador optimizador: "Se le permite transformar${\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}}$como si fuera independiente, incluso si es sólo 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};C_{2}}$${\displaystyle C_{1}}$${\displaystyle C_{2}}$

Si también tenemos expresiones booleanas sobre el estado, ordenadas por , 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}}}$

Tal definición permite el análisis formal del comportamiento de los programas, permitiendo el estudio de las relaciones entre programas. Las relaciones importantes incluyen preordenes de simulación y bisimulación . Estos 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 una gran popularidad y se ha convertido en un estándar de facto en la definición de semántica operativa. Como señal de é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 Ciencias de la Computación .

Semántica de reducción

La semántica de reducción es una presentación alternativa de la semántica operativa que utiliza los denominados contextos de reducción. El método fue introducido por Robert Hieb y Matthias Felleisen en 1992 como una técnica para formalizar una teoría de ecuaciones para el control y el estado . Por ejemplo, la gramática de un cálculo lambda simple de llamada por valor y sus contextos se puede dar como:

${\displaystyle e=v\;|\;(e\;e)\;|\;x\quad \quad v=\lambda x.e\quad \quad C=\left[\,\right]\;|\;(C\;e)\;|\;(v\;C)}$

Los contextos incluyen un hueco donde se puede insertar un término. La forma de los contextos indica dónde puede ocurrir la reducción (es decir, un término se puede insertar en un término). Para describir una semántica para este lenguaje, se proporcionan axiomas o reglas de reducción:${\displaystyle C}$${\displaystyle \left[\,\right]}$

${\displaystyle (\lambda x.e)\;v\longrightarrow e\,\left[x/v\right]\quad (\mathrm {\beta } )}$

Este único axioma es la regla beta del cálculo lambda. Los contextos de reducción muestran cómo esta regla se compone de términos más complicados. En particular, esta regla puede activarse para la posición del argumento de una aplicación como porque hay un contexto que coincide con el término. En este caso, los contextos descomponen los términos de manera única, de modo que solo sea posible una reducción en cualquier paso dado. Extender el axioma para que coincida con los contextos de reducción proporciona el cierre compatible . Tomando el cierre reflexivo y transitivo de esta relación se obtiene la relación de reducción para este lenguaje.${\displaystyle ((\lambda x.x\;\lambda x.x)\lambda x.(x\;x))}$${\displaystyle ([\,]\;\lambda x.(x\;x))}$

La técnica es útil por la facilidad con la que los contextos de reducción pueden modelar constructos de estado o control (por ejemplo, continuaciones ). Además, la semántica de reducción se ha utilizado para modelar lenguajes orientados a objetos, ^[3] sistemas de contratos y otras características del lenguaje.

Semántica de gran paso

Semántica natural

La semántica operacional estructural de gran paso también se conoce con los nombres de semántica natural , semántica relacional y semántica de evaluación . ^[4] La semántica operativa de gran paso fue introducida bajo el nombre de semántica natural por Gilles Kahn al presentar Mini-ML, un dialecto puro del lenguaje ML .

Uno puede ver las definiciones de gran paso como definiciones de funciones, o más generalmente de relaciones, interpretando cada construcción del lenguaje en un dominio apropiado. Su intuición lo convierte en una opción popular para la especificación semántica en lenguajes de programación, pero tiene algunos inconvenientes que lo hacen inconveniente o imposible de usar en muchas situaciones, como lenguajes con funciones de control intensivo o simultaneidad.

Una semántica de gran paso describe de una manera 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, subdeclaraciones, etc.).

Comparación

Hay una serie de distinciones entre la semántica de pequeños pasos y de grandes pasos que influyen en si una u otra forma 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 los llame "naturales"). Ambos pueden conducir a demostraciones más simples, por ejemplo al probar la preservación de la corrección bajo alguna transformación del programa . ^[5]

La principal desventaja de la semántica de gran paso es que los cálculos no terminantes ( divergentes ) no tienen un árbol de inferencia, lo que hace imposible establecer y probar propiedades sobre dichos cálculos. ^[5]

La semántica de pasos pequeños proporciona un mayor control de los detalles y el orden de evaluación. En el caso de la semántica operacional instrumentada, esto permite que la semántica operacional rastree y que el semántico establezca y pruebe teoremas más precisos sobre el comportamiento en tiempo de ejecución del lenguaje. Estas propiedades hacen que la semántica de pasos pequeños sea más conveniente cuando se prueba la solidez de un sistema de tipos frente a una semántica operativa. ^[5]

Ver 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). "El informe revisado sobre las teorías sintácticas del control secuencial y el estado". Informática Teórica . 103 (2): 235–271. doi : 10.1016 / 0304-3975 (92) 90014-7 .
3. Abadi, M .; Cardelli, L. (8 de septiembre de 2012). Una teoría de los objetos . ISBN 9781441985989.
4. Universidad de Illinois CS422
5. Xavier Leroy . "Semántica operativa coinductiva de gran paso".

• Gilles Kahn . "Semántica natural". Actas del IV Simposio Anual sobre Aspectos Teóricos de la Informática . Springer-Verlag. Londres. 1987.
• Gordon D. Plotkin. Un enfoque estructural de la semántica operativa . (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. Programa. 60-61: 3-15, 2004. ( preimpresión ).
• Dana S. Scott. Esquema de una teoría matemática de la computación, Grupo de Investigación en Programación, Monografía Técnica PRG-2, Universidad de Oxford, 1970.
• Adriaan van Wijngaarden y col. 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 la semántica operativa en Wikimedia Commons