Semántica (computación)

En la teoría de los lenguajes de programación, la semántica es el campo relacionado con el 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 tal caso, si la evaluación fuera de cadenas sintácticamente inválidas, el resultado sería la no computación. La semántica describe los procesos que sigue una computadora cuando ejecuta 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 computación.

Visión de conjunto

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 los 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, en la que 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 necesidad práctica, las denotaciones se describen utilizando algún tipo 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 operativa, mediante la cual la ejecución del lenguaje se describe directamente (en lugar de por 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 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 operativa se puede definir a través de 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 al respecto 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 denotativos, operativos 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.

Variaciones

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

• La semántica de acción es un enfoque que trata de 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 es una forma de semántica axiomática basada en leyes algebraicas para describir y razonar sobre la semántica del programa de manera formal. También es compatible con la semántica denotacional y la semántica operativa;
• Las gramáticas de atributos 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 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 las gramáticas regulares o sin contexto con condiciones sensibles al contexto;
• La semántica categórica (o "functorial") utiliza la teoría de categorías como el formalismo matemático central. Por lo general, se demuestra 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 es 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. Los formalismos concurrentes históricamente importantes han incluido el modelo de actor y los cálculos de proceso;
• La semántica de juegos utiliza una metáfora inspirada en la teoría de juegos;
• La semántica de transformadores de predicados, desarrollada por Edsger W. Dijkstra, describe el significado de un fragmento de programa como la función que transforma una condición posterior 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 (operacional) particular utilizando un sistema de prueba (axiomático) particular.
• 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, 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 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 a través de la teoría de la interpretación abstracta.

Historia

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