Semántica (informática)

No confundir con la semántica computacional .

The field concerned with the rigorous mathematical study of the meaning of programming languages

Este artículo incluye una lista de referencias generales , pero permanece en gran parte sin verificar porque carece de suficientes citas en línea correspondientes . Ayude a mejorar este artículo introduciendo citas más precisas. ( Agosto de 2020 ) ( Obtenga información sobre cómo y cuándo eliminar este mensaje de plantilla )

En la teoría de los lenguajes de programación , la semántica es el campo que se ocupa del estudio matemático riguroso del significado de los lenguajes de programación . Lo hace evaluando el significado de cadenas sintácticamente válidas definidas por un lenguaje de programación específico, mostrando el cálculo involucrado. En el caso de que la evaluación sea de cadenas sintácticamente inválidas, el resultado sería no computación. La semántica describe los procesos que sigue una computadora al ejecutar un programa en ese lenguaje específico. Esto se puede mostrar describiendo la relación entre la entrada y la salida de un programa, o una explicación de cómo se ejecutará el programa en una determinada plataforma., creando así un modelo de cálculo .

La semántica formal, por ejemplo, ayuda a escribir compiladores , comprender mejor lo que hace un programa y probar , por ejemplo, que la siguiente ifdeclaración

si  1  ==  1  entonces S1 si no S2

tiene el mismo efecto que S1solo.

Resumen

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

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

• Semántica denotacional , según la cual cada frase del lenguaje se interpreta como una denotación , es decir, un significado conceptual que se puede pensar 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 una 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 en 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 operacional , por la cual la ejecución del lenguaje se describe directamente (en lugar de por traducción). La semántica operacional se corresponde libremente con 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 al describir las transiciones que inducen en los estados de la máquina. Alternativamente, al igual que con el cálculo lambda puro, la semántica operativa se puede definir mediante transformaciones sintácticas en frases del lenguaje mismo;
• Semántica axiomática , mediante la cual se da significado a las frases describiendo los axiomas que se aplican a ellas. La semántica axiomática no distingue 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 .

Las distinciones entre las tres amplias clases de enfoques a veces pueden ser vagas, pero todos los enfoques conocidos de la semántica formal utilizan las técnicas anteriores o alguna combinación de las mismas.

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.

Variaciones

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

• La semántica de acción es un enfoque que intenta modularizar la semántica denotacional, dividiendo el proceso de formalización en dos capas (macro y micro semántica) y predefiniendo tres entidades semánticas (acciones, datos y rendidores) para simplificar la especificación;
• La semántica algebraica es una forma de semántica axiomática basada enleyes algebraicas para describir y razonar sobre la semántica del programa de unamanera formal ;
• Las gramáticas de atributos definen sistemas que calculan sistemáticamente " metadatos " (llamados atributos ) para los diversos casos de 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. 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") utiliza la teoría de categorías como formalismo matemático central. Se suele demostrar que una semántica categórica corresponde a alguna semántica axiomática que da una presentación sintáctica de las estructuras categóricas. Además, la semántica denotacional son a menudo instancias de una semántica categórica general;
• La semántica de concurrencia es un término general para cualquier semántica formal que describa cálculos concurrentes. Formalismos concurrentes históricamente importantes han incluido el modelo Actor y los cálculos de procesos ;
• La semántica de juegos utiliza una metáfora inspirada en la teoría de juegos .
• La semántica del transformador de predicados , desarrollada por Edsger W. Dijkstra , describe el significado de un fragmento de programa como la función que transforma una poscondición en la condición previa necesaria para establecerla.

Describiendo relaciones

Por una variedad de razones, uno podría desear 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 "sólido" razonar sobre una estrategia de interpretación particular (operativa) utilizando un sistema de prueba particular (axiomático) .
• Demostrar que la semántica operativa sobre una máquina de alto nivel está relacionada mediante una simulación con la semántica sobre una máquina de bajo nivel, por lo que la máquina abstracta de bajo nivel contiene más operaciones primitivas que la definición de 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 semánticas múltiples a través de abstracciones a través de la teoría de la interpretación abstracta .

Historia

Esta sección necesita expansión . Puede ayudar agregando más . ( Agosto de 2013 )

A Robert W. Floyd se le atribuye la fundación del campo de la semántica del lenguaje de programación en Floyd (1967) . ^[1]

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

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 de Matemáticas Aplicadas. 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 operacional 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.
• 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-2.
• 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 los lenguajes de programación (Posdata) .
• 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 los lenguajes de programación . Prensa de la Universidad de Cambridge. 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 . Saltador. ISBN 978-1-84628-692-6.
• Stump, 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.