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 significado computacional a cadenas válidas en la sintaxis de un lenguaje de programación . Está estrechamente relacionado y, a menudo, se cruza con la semántica de las demostraciones matemáticas .

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 cálculo .

Historia

En 1967, Robert W. Floyd publicó el artículo Asignación de significados a 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, la 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 cercana a cada comando.

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

En la década de 1970 surgieron los términos semántica operativa 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 verificación de modelos .

Enfoques

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

• Semántica denotacional , ^[6] mediante la cual cada frase del 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 una teoría de 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 operativa , ^[7] mediante la cual la ejecución del lenguaje se describe directamente (en lugar de mediante traducción). La semántica operativa 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 operativa puede definir una máquina abstracta (como la máquina SECD ) y dar significado a frases describiendo las transiciones que inducen en los estados de la máquina. Alternativamente, como ocurre con el cálculo lambda puro , la semántica operativa se puede definir mediante transformaciones sintácticas en frases del propio lenguaje;
• Semántica axiomática , ^[8] mediante la cual se da significado a frases describiendo los axiomas que se les aplican. 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 él en alguna lógica. El ejemplo canónico de 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 de apoyar el formalismo matemático. ^{[ cita necesaria ]}

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 productores) 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 semántica denotacional y semántica operativa ;
• Las gramáticas de atributos ^[10] definen sistemas que calculan sistemáticamente " metadatos " (llamados atributos ) para los distintos casos de la sintaxis del lenguaje . Las gramáticas de atributos pueden entenderse como una semántica denotacional en la que el idioma de destino es simplemente el idioma original enriquecido con anotaciones de atributos. Además 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 gramáticas regulares oconcondiciones sensibles al contexto ;
• La semántica categórica (o "functorial") ^[11] utiliza la teoría de categorías como núcleo del formalismo matemático. Generalmente se ha demostrado que la semántica categórica corresponde a alguna semántica axiomática que proporciona una presentación sintáctica de las estructuras categóricas. Además, la semántica denotacional es a menudo instancias de una semántica categórica general; ^[12]
• 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, uno podría desear describir las relaciones entre diferentes semánticas formales. Por ejemplo:

• Demostrar que una semántica operativa particular para una lengua satisface las fórmulas lógicas de una semántica axiomática para esa lengua. Tal prueba demuestra que es "sólido" razonar sobre una estrategia de interpretación (operacional) particular utilizando un sistema de prueba (axiomático) particular .
• Demostrar que la semántica operativa en una máquina de alto nivel está relacionada mediante una simulación con la semántica en una máquina de bajo nivel, donde la máquina abstracta de bajo nivel contiene operaciones más primitivas que la definición de máquina abstracta de alto nivel de un lenguaje determinado. 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 necesaria ]}

Ver 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, José A. (1975). "Semántica de la computación". Teoría de Categorías Aplicada a la Computación y el Control . Apuntes de conferencias sobre informática. vol. 25. Saltador . 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 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 Estadounidense. 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, Massachusetts: MIT Press. pag. xv. ISBN 978-0-262-23169-5.
6. Schmidt, David A. (1986). Semántica denotacional: una metodología para el desarrollo del lenguaje . Editores William C. Brown. ISBN 9780205104505.
7. Plotkin, Gordon D. (1981). Un enfoque estructural de la semántica operativa (Reporte). Informe Técnico DAIMI FN-19. Departamento de Informática, Universidad de Aarhus .
8. Goguen, Joseph A .; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). "Semántica de á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, Martín; Lorho, Bernard (1988). "Gramáticas de atributos: definiciones, sistemas y bibliografía . Apuntes de conferencias sobre informática 323. Springer-Verlag . ISBN 9780387500560.
11. Lawvere, F. William (1963). "Semántica funcional de teorías algebraicas". Actas de la Academia Nacional de Ciencias de los Estados Unidos de América . 50 (5): 869–872. Código bibliográfico : 1963PNAS...50..869L. doi : 10.1073/pnas.50.5.869 . PMC 221940 . PMID  16591125. 
12. Andrzej Tarlecki; Rod M. Burstall ; José A. Goguen (1991). "Algunas herramientas algebraicas fundamentales para la semántica de la computación: Parte 3. Categorías indexadas". Informática Teórica . 91 (2): 239–264. doi : 10.1016/0304-3975(91)90085-G .
13. Loco, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). "El problema de la semántica de concurrencia de los lenguajes de programación" (PDF) . Actas del Simposio europeo sobre lenguajes y sistemas de programación . Saltador . págs. 283–307. doi : 10.1007/978-3-662-46669-8_12 .
14. Abramsky, Sansón (2009). "Semántica de la interacción: una introducción a la semántica de los juegos". En Andrew M. Pitts; P. Dybjer (eds.). Semántica y Lógica de la Computación. Prensa de la Universidad de Cambridge. págs. 1–32. doi :10.1017/CBO9780511526619.002. ISBN 9780521580571.
15. Dijkstra, Edsger W. (1975). "Comandos cautelosos, indeterminación y derivación formal de programas". Comunicaciones de la ACM . 18 (8): 453–457. doi : 10.1145/360933.360975 . S2CID  1679242.

Otras lecturas

Libros de texto

• Floyd, Robert W. (1967). "Asignación de significados a 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 Estadounidense. 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 operativa estructural . 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.
• Günter, Carl (1992). Semántica de los lenguajes de programación . Prensa del MIT. ISBN 0-262-07143-6.
• Nielson, recursos humanos; Nielson, Flemming (1992). Semántica con aplicaciones: una introducción formal (PDF) . Wiley. ISBN 978-0-471-92980-2. Archivado 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 . Prensa del MIT. ISBN 0-262-73103-7.
• Mitchell, John C. (1995). Fundamentos de los lenguajes de programación (posdata) .
• Sloneger, 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 los lenguajes de programación . Prensa de la Universidad de Cambridge. ISBN 0-521-59414-6.
• Harper, Robert (2006). Fundamentos prácticos de los lenguajes de programación (PDF) . Archivado desde el original (PDF) el 27 de junio de 2007.(Borrador de trabajo)
• Nielson, recursos humanos; Nielson, Flemming (2007). Semántica con aplicaciones: un aperitivo. Saltador. ISBN 978-1-84628-692-6.
• Tocón, Aaron (2014). Fundamentos del lenguaje 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 lectura

• 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.