Semántica (informática)

Estudio matemático del significado de los lenguajes de programación.

En la teoría de los lenguajes de programación , la semántica es el estudio matemático riguroso del significado de los lenguajes de programación . ^[1] La semántica asigna un significado computacional a cadenas válidas en la sintaxis de un lenguaje de programación . Está estrechamente relacionada con la semántica de las demostraciones matemáticas y a menudo se cruza con ella .

La semántica describe los procesos que sigue una computadora al ejecutar un programa en ese lenguaje específico. Esto se puede hacer describiendo la relación entre la entrada y la salida de un programa, o dando una explicación de cómo se ejecutará el programa en una determinada plataforma , creando así un modelo de computación .

Historia

En 1967, Robert W. Floyd publicó el artículo Asignación de significados a los programas ; su principal objetivo era "un estándar riguroso para las pruebas sobre programas informáticos, incluidas las pruebas de corrección , equivalencia y terminación". ^{[2] [3]} Floyd escribió además: ^[2]

En nuestro enfoque, una definición semántica de un lenguaje de programación se basa en una definición sintáctica . Debe especificar cuáles de las frases de un programa sintácticamente correcto representan comandos y qué condiciones deben imponerse a una interpretación en las proximidades de cada comando.

En 1969, Tony Hoare publicó un artículo sobre la lógica de Hoare basada en las ideas de Floyd, ahora a veces llamadas colectivamente semántica axiomática . ^{[4] [5]}

En la década de 1970 surgieron los términos semántica operacional y semántica denotacional ^{. [5]}

Descripción general

El campo de la semántica formal abarca todo lo siguiente:

• La definición de modelos semánticos
• Las relaciones entre diferentes modelos semánticos
• Las relaciones entre diferentes enfoques del significado
• La relación entre la computación y las estructuras matemáticas subyacentes de campos como la lógica , la teoría de conjuntos , la teoría de modelos , la teoría de categorías , etc.

Tiene estrechos vínculos con otras áreas de la informática , como el diseño de lenguajes de programación , la teoría de tipos , los compiladores e intérpretes , la verificación de programas y la comprobación de modelos .

Aproches

Existen muchos enfoques de la semántica formal; estos pertenecen a tres clases principales:

• Semántica denotacional , ^[6] por la cual cada frase en el lenguaje se interpreta como una denotación , es decir, un significado conceptual que puede pensarse de manera abstracta. Tales denotaciones son a menudo objetos matemáticos que habitan un espacio matemático, pero no es un requisito que deban serlo. Como necesidad práctica, las denotaciones se describen utilizando alguna forma de notación matemática, que a su vez puede formalizarse como un metalenguaje denotacional. Por ejemplo, la semántica denotacional de los lenguajes funcionales a menudo traduce el lenguaje a la teoría del dominio . Las descripciones semánticas denotacionales también pueden servir como traducciones compositivas de un lenguaje de programación al metalenguaje denotacional y usarse como base para diseñar compiladores .
• Semántica operacional , ^[7] mediante la cual la ejecución del lenguaje se describe directamente (en lugar de por traducción). La semántica operacional corresponde vagamente a la interpretación , aunque nuevamente el "lenguaje de implementación" del intérprete es generalmente un formalismo matemático. La semántica operacional puede definir una máquina abstracta (como la máquina SECD ) y dar significado a las frases al describir las transiciones que inducen en los estados de la máquina. Alternativamente, como con el cálculo lambda puro , la semántica operacional puede definirse mediante transformaciones sintácticas en frases del lenguaje mismo;
• Semántica axiomática ^[8] ,mediante la cual se da significado a las frases describiendo los axiomas que se aplican a ellas. La semántica axiomática no hace distinción entre el significado de una frase y las fórmulas lógicas que la describen; su significado es exactamente lo que se puede probar sobre ella en alguna lógica. El ejemplo canónico de la semántica axiomática es la lógica de Hoare .

Aparte de la elección entre enfoques denotacionales, operacionales o axiomáticos, la mayoría de las variaciones en los sistemas semánticos formales surgen de la elección del formalismo matemático de apoyo. ^{[ cita requerida ]}

Variaciones

Algunas variaciones de la semántica formal incluyen las siguientes:

• La semántica de acción ^[9] es un enfoque que intenta modularizar la semántica denotacional, dividiendo el proceso de formalización en dos capas (macro y microsemántica) y predefiniendo tres entidades semánticas (acciones, datos y rendimientos) para simplificar la especificación;
• La semántica algebraica ^[8] es una forma de semántica axiomática basada en leyes algebraicas para describir y razonar sobre la semántica de programas de manera formal . También admite la semántica denotacional y la semántica operacional ;
• Las gramáticas de atributos ^[10] definen sistemas que calculan sistemáticamente " metadatos " (llamados atributos ) para los diversos casos de la sintaxis del lenguaje . Las gramáticas de atributos pueden entenderse como una semántica denotacional donde el lenguaje de destino es simplemente el lenguaje original enriquecido con anotaciones de atributos. Aparte de la semántica formal, las gramáticas de atributos también se han utilizado para la generación de código en compiladores y para aumentar las gramáticas regulares o libres de contexto concondiciones sensibles al contexto ;
• La semántica categórica (o "funcional") ^[11] utiliza la teoría de categorías como formalismo matemático central. Se suele demostrar que la semántica categórica corresponde a una semántica axiomática que ofrece una presentación sintáctica de las estructuras categóricas. Además, la semántica denotacional suele ser un ejemplo de una semántica categórica general; ^[12]
• La semántica de concurrencia ^[13] es un término general para cualquier semántica formal que describa cálculos concurrentes. Los formalismos concurrentes históricamente importantes han incluido el modelo de actor y los cálculos de proceso ;
• La semántica de juegos ^[14] utiliza una metáfora inspirada en la teoría de juegos ;
• La semántica del transformador de predicados , ^[15] desarrollada por Edsger W. Dijkstra , describe el significado de un fragmento de programa como la función que transforma una poscondición en la precondición necesaria para establecerla.

Describiendo relaciones

Por diversas razones, es posible que se desee describir las relaciones entre diferentes semánticas formales. Por ejemplo:

• Demostrar que una semántica operacional particular para un lenguaje satisface las fórmulas lógicas de una semántica axiomática para ese lenguaje. Tal prueba demuestra que es "correcto" razonar sobre una estrategia de interpretación (operacional) particular utilizando un sistema de prueba (axiomático) particular .
• Demostrar que la semántica operacional en una máquina de alto nivel está relacionada mediante una simulación con la semántica en una máquina de bajo nivel, en la que la máquina abstracta de bajo nivel contiene más operaciones primitivas que la definición de la máquina abstracta de alto nivel de un lenguaje dado. Tal prueba demuestra que la máquina de bajo nivel "implementa fielmente" la máquina de alto nivel.

También es posible relacionar múltiples semánticas a través de abstracciones mediante la teoría de la interpretación abstracta . ^{[ cita requerida ]}

Véase también

• Semántica computacional
• Semántica formal (lógica)
• Semántica formal (lingüística)
• Ontología
• Ontología (ciencia de la información)
• Equivalencia semántica
• Tecnología semántica

Referencias

1. Goguen, Joseph A. (1975). "Semántica de la computación". Teoría de categorías aplicada a la computación y el control . Apuntes de clase sobre informática. Vol. 25. Springer . Págs. 151-163. doi :10.1007/3-540-07142-3_75. ISBN. 978-3-540-07142-6.
2. Floyd, Robert W. (1967). "Asignación de significados a los programas" (PDF) . En Schwartz, JT (ed.). Aspectos matemáticos de la informática. Actas del Simposio sobre matemáticas aplicadas. Vol. 19. Sociedad Matemática Americana. págs. 19–32. ISBN 0821867288.
3. Knuth, Donald E. "Resolución conmemorativa: Robert W. Floyd (1936–2001)" (PDF) . Memoriales de la facultad de la Universidad de Stanford . Sociedad Histórica de Stanford.
4. Hoare, CAR (octubre de 1969). "Una base axiomática para la programación informática". Comunicaciones de la ACM . 12 (10): 576–580. doi : 10.1145/363235.363259 . S2CID  207726175.
5. Winskel, Glynn (1993). La semántica formal de los lenguajes de programación: una introducción. Cambridge, Mass.: MIT Press. p. xv. ISBN 978-0-262-23169-5.
6. Schmidt, David A. (1986). Semántica denotacional: una metodología para el desarrollo del lenguaje . William C. Brown Publishers. ISBN 9780205104505.
7. Plotkin, Gordon D. (1981). Un enfoque estructural de la semántica operacional (Informe). Informe técnico DAIMI FN-19. Departamento de Ciencias de la Computación, Universidad de Aarhus .
8. Goguen, Joseph A. ; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). "Semántica del álgebra inicial y álgebras continuas". Revista de la ACM . 24 (1): 68–95. doi : 10.1145/321992.321997 . S2CID  11060837.
9. Mosses, Peter D. (1996). Teoría y práctica de la semántica de la acción (informe). Informe BRICS RS9653. Universidad de Aarhus .
10. Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988). "Gramáticas de atributos: definiciones, sistemas y bibliografía" . Apuntes de clase sobre informática 323. Springer-Verlag . ISBN. 9780387500560.
11. Lawvere, F. William (1963). "Semántica funcional de las teorías algebraicas". Actas de la Academia Nacional de Ciencias de los Estados Unidos de América . 50 (5): 869–872. Bibcode :1963PNAS...50..869L. doi : 10.1073/pnas.50.5.869 . PMC 221940 . PMID  16591125. 
12. Andrzej Tarlecki; Rod M. Burstall ; Joseph A. Goguen (1991). "Algunas herramientas algebraicas fundamentales para la semántica de la computación: Parte 3. Categorías indexadas". Ciencias de la computación teórica . 91 (2): 239–264. doi : 10.1016/0304-3975(91)90085-G .
13. Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). "El problema de la semántica de concurrencia de lenguajes de programación" (PDF) . Actas del Simposio Europeo sobre Lenguajes y Sistemas de Programación . Springer . págs. 283–307. doi : 10.1007/978-3-662-46669-8_12 .
14. Abramsky, Samson (2009). "Semántica de la interacción: una introducción a la semántica de juegos". En Andrew M. Pitts; P. Dybjer (eds.). Semántica y lógica de la computación. Cambridge University Press. págs. 1–32. doi :10.1017/CBO9780511526619.002. ISBN 9780521580571.
15. Dijkstra, Edsger W. (1975). "Órdenes protegidas, no determinación y derivación formal de programas". Comunicaciones de la ACM . 18 (8): 453–457. doi : 10.1145/360933.360975 . S2CID  1679242.

Lectura adicional

Libros de texto

• Floyd, Robert W. (1967). "Asignación de significados a los programas" (PDF) . En Schwartz, JT (ed.). Aspectos matemáticos de la informática. Actas del Simposio sobre matemáticas aplicadas. Vol. 19. Sociedad Matemática Americana. Págs. 19–32. ISBN. 0821867288.
• Hennessy, M. (1990). La semántica de los lenguajes de programación: una introducción elemental utilizando la semántica estructural operacional . Wiley. ISBN 978-0-471-92772-3.
• Tennent, Robert D. (1991). Semántica de lenguajes de programación. Prentice Hall. ISBN 978-0-13-805599-8.
• Gunter, Carl (1992). Semántica de lenguajes de programación . MIT Press. ISBN 0-262-07143-6.
• Nielson, HR; Nielson, Flemming (1992). Semántica con aplicaciones: una introducción formal (PDF) . Wiley. ISBN 978-0-471-92980-2Archivado desde el original (PDF) el 17 de abril de 2012. Consultado el 27 de mayo de 2011 .
• Winskel, Glynn (1993). La semántica formal de los lenguajes de programación: una introducción . MIT Press. ISBN 0-262-73103-7.
• Mitchell, John C. (1995). Fundamentos de lenguajes de programación (Postscript) .
• Slonneger, Kenneth; Kurtz, Barry L. (1995). Sintaxis formal y semántica de lenguajes de programación. Addison-Wesley. ISBN 0-201-65697-3.
• Reynolds, John C. (1998). Teorías de lenguajes de programación . Cambridge University Press. ISBN 0-521-59414-6.
• Harper, Robert (2006). Fundamentos prácticos para lenguajes de programación (PDF) . Archivado desde el original (PDF) el 27 de junio de 2007.(Borrador de trabajo)
• Nielson, HR; Nielson, Flemming (2007). Semántica con aplicaciones: un aperitivo. Springer. ISBN 978-1-84628-692-6.
• Stump, Aaron (2014). Fundamentos de lenguajes de programación . Wiley. ISBN 978-1-118-00747-1.
• Krishnamurthi, Shriram (2012). "Lenguajes de programación: aplicación e interpretación" (2.ª ed.).

Notas de la conferencia

• Winskel, Glynn. "Semántica denotacional" (PDF) . Universidad de Cambridge.

Enlaces externos

• Aaby, Anthony (2004). Introducción a los lenguajes de programación. Archivado desde el original el 19 de junio de 2015.Semántica.