Semántica operativa

Categoría de semántica del lenguaje de programación formal.

La semántica operativa es una categoría de semántica de 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 operativa se clasifica en dos categorías: la semántica operativa 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 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 al 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 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 aspirar a un enfoque más "abstracto" y "más limpio" de la semántica, pero si el plan quiere ser bueno, los aspectos operativos no pueden ignorarse por completo. (Scott70)

Enfoques

Gordon Plotkin introdujo la semántica operativa estructural, Matthias Felleisen y Robert Hieb la semántica reductora, ^[2] y Gilles Kahn la semántica natural.

Semántica de pequeños pasos

Semántica operativa estructural

La semántica operativa estructural (SOS, también llamada semántica operativa 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 operativa. 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 operativa. Una especificación SOS define el comportamiento de un programa en términos de (un conjunto 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 sencillo, consideremos parte de la semántica de un lenguaje de programación simple; Se dan ilustraciones adecuadas en Plotkin81 y Hennessy90, y en otros libros de texto. Deje abarcar los programas del lenguaje y deje abarcar los estados (por ejemplo, funciones desde ubicaciones de memoria hasta valores). Si tenemos expresiones (intervalos entre ), 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))}}}$

Informalmente, 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 venir 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 estado termina en estado , entonces el programa en estado se reducirá al programa en estado . (Puede pensar en esto como formalizar "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á a programa en estado . (Puede pensar en esto como una formalización del principio de un compilador optimizador: "Se le permite transformarse como si fuera independiente, incluso si es solo la primera parte de un programa"). estructural, porque el significado del programa secuencial , está definido 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}}}$

Tal definición permite un análisis formal del comportamiento de los programas, permitiendo el estudio de las relaciones entre programas. Las relaciones importantes incluyen pedidos anticipados de simulación y bisimulación . Estos son especialmente útiles en el contexto de la teoría de la concurrencia .

Gracias a su apariencia intuitiva y 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 semántica operativa. Como señal de éxito, el informe original (el llamado informe Aarhus) sobre SOS (Plotkin81) ha atraído más de 1.000 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 operativa. 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} Matthias Felleisen las generalizó a lenguajes funcionales de orden superior con características imperativas en su disertación de 1987. ^[4] El método fue elaborado aún más por Matthias Felleisen y Robert Hieb en 1992 hasta convertirlo en una teoría totalmente ecuacional para el control y el estado . ^[2] La propia 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 proporciona 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 ubica 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 colocar una declaración de asignación en esa posición, se "hace burbujear" a través de aplicaciones de funciones y el lado derecho de las declaraciones de asignación hasta que llegue al 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 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 \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 inserta un término de manera capturante. La forma del contexto indica con este agujero dónde puede ocurrir la reducción. Para describir el “burbujeo” con la ayuda de contextos de evaluación, basta un solo 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 única es la regla de elevación del cálculo lambda de Felleisen y Hieb para declaraciones de asignación. Los contextos de evaluación restringen esta regla a ciertos términos, pero es libremente aplicable en cualquier término, incluso bajo lambdas.

Siguiendo a Plotkin, mostrar 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 la 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 más a la izquierda/más externa. Felleisen demostró que las extensiones imperativas de este cálculo satisfacen estos teoremas. Las consecuencias de estos teoremas son que la teoría ecuacional (la clausura simétrica-transitiva-reflexiva) 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 puede derivarse 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 en Ingeniería Semántica de PLT Redex ofrecen un tratamiento moderno y completo de la semántica de reducción que analiza en detalle varias de estas aplicaciones . ^[7]

Semántica de grandes pasos

Semántica natural

La semántica operativa 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] Gilles Kahn introdujo la semántica operativa de gran paso bajo el nombre de semántica natural al presentar Mini-ML, un dialecto puro de ML .

Se pueden ver las definiciones de grandes pasos como definiciones de funciones, o más generalmente de relaciones, que interpretan 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 hacen que su uso sea inconveniente o imposible en muchas situaciones, como lenguajes con funciones de control intensivo o concurrencia. ^[9]

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

Comparación

Hay una serie de distinciones entre la semántica de pasos pequeños y grandes 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 las llame "naturales"). Ambas pueden conducir a pruebas más simples, por ejemplo. al demostrar 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 probar propiedades sobre dichos cálculos. ^[10]

La semántica de pequeños pasos brinda más control sobre los detalles y el orden de la evaluación. En el caso de la semántica operativa instrumentada, esto permite que la semántica operativa realice un seguimiento y que el semántico enuncie y pruebe teoremas más precisos sobre el comportamiento del lenguaje en tiempo de ejecución. Estas propiedades hacen que la semántica de pequeños pasos sea más conveniente al probar la solidez del tipo de un sistema de tipos frente a una semántica operativa. ^[10]

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 estado y el control secuencial". Informática Teórica . 103 (2): 235–271. doi :10.1016/0304-3975(92)90014-7.
3. Plotkin, Gordon (1975). "Llamada por nombre, llamada por valor y cálculo λ" (PDF) . Informática Teórica . 1 (2): 125-159. doi : 10.1016/0304-3975(75)90017-1 . Consultado el 22 de julio de 2021 .
4. Felleisen, Matías (1987). Los cálculos de la conversión Lambda-v-CS: una teoría sintáctica de control y estado en lenguajes de programación imperativos de orden superior (PDF) (Doctor). Universidad de Indiana . Consultado el 22 de julio de 2021 .
5. Felleisen, Matías; Friedman, Daniel P. (1987). "Una semántica de reducción para lenguajes imperativos de orden superior". Actas de Arquitecturas y Lenguajes Paralelos de Europa . Congreso Internacional de 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, Matías; Findler, Robert Bruce; Flatt, Mateo (2009). Ingeniería Semántica con PLT Redex. La prensa del MIT. ISBN 978-0-262-06275-6.
8. Universidad de Illinois CS422
9. Nipkow, Tobías; 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 operativa coinductiva de grandes pasos".

Otras lecturas

• Gilles Kahn . "Semántica natural". Actas del cuarto 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) Tecnología. Representante 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 operativa estructural. J. Registro. Álgebra. 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 et al. Informe revisado sobre el lenguaje algorítmico ALGOL 68 . IFIP. 1968. ([2] ^{[ enlace muerto permanente ]} )
• Mateo 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