Semántica (lenguajes de programación)

En la teoría de los lenguajes de programación , la semántica es el estudio lógico 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 relacionada con la semántica de las demostraciones matemáticas y, a menudo, se solapa con ella .

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

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, la definición semántica de un lenguaje de programación se basa en una definición sintáctica . Esta debe especificar cuáles de las frases de un programa sintácticamente correcto representan comandos y qué condiciones deben imponerse a la interpretación en el entorno 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 denominada 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 ]}

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 .

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

• La semántica denotacional ^{[ 6 ]} implica que cada frase del lenguaje se interpreta como una denotación , es decir, un significado conceptual que puede pensarse de forma abstracta. Estas denotaciones suelen ser objetos matemáticos que habitan un espacio matemático, pero no es un requisito que así sea. Por necesidad práctica, las denotaciones se describen mediante 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 suele traducir el lenguaje a la teoría de dominios . Las descripciones semánticas denotacionales también pueden servir como traducciones compositivas de un lenguaje de programación al metalenguaje denotacional y utilizarse como base para el diseño de 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 se corresponde vagamente con 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 propio lenguaje;
• La semántica axiomática [ ^{8 ]} otorga significado a las frases describiendo los axiomas que les son aplicables. 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 precisamente lo que se puede demostrar sobre ella mediante 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 del formalismo matemático de apoyo.

Algunas variantes 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 (macrosemántica y microsemántica) y predefiniendo tres entidades semánticas (acciones, datos y generadores) 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 los 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. 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 las gramáticas regulares o libres de contexto concondiciones sensibles al contexto ;
• La semántica categórica (o "funtorial") ^{[ 11 ]} utiliza la teoría de categorías como formalismo matemático central. Generalmente se demuestra que la semántica categórica se corresponde con alguna semántica axiomática que proporciona una presentación sintáctica de las estructuras categóricas. Además, la semántica denotacional suele ser una instancia 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 computaciones concurrentes. Históricamente, los formalismos concurrentes importantes han incluido el modelo de actor y los cálculos de procesos ;
• La semántica de juegos ^{[ 14 ]} utiliza una metáfora inspirada en la teoría de juegos ;
• La semántica de transformadores de predicados , ^{[ 15 ]} desarrollada por Edsger W. Dijkstra , describe el significado de un fragmento de programa como la función que transforma una postcondición en la precondición necesaria para establecerla.

Por diversas 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. Dicha demostración prueba que es "correcto" razonar sobre una estrategia de interpretación (operacional) particular utilizando un sistema de prueba (axiomático) particular .
• Para demostrar que la semántica operacional sobre una máquina de alto nivel se relaciona mediante una simulación con la semántica sobre una máquina de bajo nivel, donde la máquina abstracta de bajo nivel contiene más operaciones primitivas que la definición de un lenguaje dado en la máquina abstracta de alto nivel, dicha demostración prueba 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 .

• 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

Libros de texto

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