Semántica de lenguajes de programación

En la Teoría de lenguajes de programación, la semántica es el campo que tiene que ver con el estudio riguroso desde un punto de vista matemático del significado de los lenguajes de programación. Esto se hace evaluando el significado de cadenas sintácticamente legales definidas por un lenguaje de programación específico, mostrando el proceso computacional involucrado. En el caso de que la evaluación fuera de cadenas sintácticamente ilegales, el resultado sería no-cómputo. La semántica describe el proceso que una computadora sigue 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 el programa se ejecutará en cierta plataforma, y consecuentemente creando un modelo de computación.

Semánticas formales ayudan, por ejemplo, a escribir compiladores, a tener un mejor entendimiento de lo que un programa está haciendo y a hacer determinadas pruebas, como demostrar que el siguiente código

if 1 == 1 then S1 else S2

tiene el mismo efecto que S1 por sí solo.

Vistazo general

El campo de las semánticas formales abarca todo lo que sigue:

• Definición de modelos semánticos
• Relaciones entre diferentes modelos semánticos
• Relaciones entre los distintos enfoques de significado
• Relación entre computación y las estructuras matemáticas subyacentes de varios campos como la lógica, teoría de conjuntos, teoría de modelos, teoría de categorías, etc.

También tiene vínculos cercanos con otras áreas de la ciencia de la computación como el diseño de lenguajes de programación, teoría de tipos, intérpretes y compiladores, verificación de programas y modelos.

Descripción

Hay muchos enfoques a las semánticas formales, las cuales pertenecen a tres categorías principales:

• Semántica denotacional, por medio de las cuales cada frase en el lenguaje es interpretada como una denotación. Tales denotaciones a menudo son objetos matemáticos que habitan espacios matemáticos, pero no es un requerimiento que éstas deban serlo. Como una necesidad práctica, las denotaciones se describen usando alguna forma de notación matemática, la cual en turno puede ser formalizada como un metalenguaje denotativo. Por ejemplo, las semánticas denotacionales de lenguajes funcionales muchas veces traducen el lenguaje en teoría de dominio. Las descripciones semánticas denotacionales también pueden servir como traducciones de composición de un lenguaje de programación en el metalenguaje denotativo y se utiliza como base para el diseño de compiladores.

• Semántica operacional, donde la ejecución del lenguaje se describe directamente (en vez de hacerse mediante el uso de una traducción). Las semánticas operacionales tienen que ver con la interpretación, aunque nuevamente el “lenguaje de implementación” del intérprete es de forma general un formalismo matemático. Las semánticas operacionales pueden definir una máquina abstracta (como la máquina SECD), y dan significado a las frases describiendo las transiciones que ellas inducen en los estados de la máquina. De forma alternativa, como con el cálculo lambda puro, las semánticas operacionales pueden ser definidas vía transformaciones sintácticas sobre frases del lenguaje en sí mismo.
• Semántica axiomática, a través de la cual se le da significado a las frases describiendo los axiomas lógicos que se aplican a ellas. Las semánticas axiomáticas no hacen distinción entre un significado de una frase y las fórmulas lógicas que la describen, su significado es exactamente lo que se puede probar de ella en alguna lógica. El ejemplo canónico de semánticas axiomáticas es la lógica de Hoare.

Las diferencias entre estas tres amplias clases de aproximaciones puede que a veces sean difusas, pero todas las aproximaciones conocidas a las semánticas formales usan las técnicas de arriba, o alguna combinación de ellas.

Aparte de la elección entre aproximación denotacional, operacional o axiomática, la mayoría de las variaciones en los sistemas de semántica formal vienen de la elección de la base en el formalismo matemático.

Variaciones

Algunas variaciones de las semánticas formales incluyen las siguientes:

• Semánticas de acción: Es una aproximación que trata de modularizar semánticas denotacionales, separando el proceso de formalización en dos capas (macro y micorsemánticas) y predefiniendo tres entidades semánticas (acciones, datos y productores) para simplificar la especificación.
• Semánticas algebraicas: Es una forma de semántica axiomática basada en leyes algebraicas para describir y sacar conclusiones acerca de programas semánticos en una forma formal.
• Gramáticas atributadas: Definen sistemas que sistemáticamente computan metadatos (llamados atributos) para los múltiples casos de las sintaxis del lenguaje. Las gramáticas atributadas se pueden ver como semánticas denotacionales donde el lenguaje objetivo es simplemente el lenguaje original enriquecido con anotaciones atributadas. Aparte de las semánticas formales, las gramáticas atributadas también han sido usadas para generación de código en compiladores, y para aumentar gramáticas regulares o libres del contexto con condiciones dependientes del contexto.
• Semánticas categóricas: Usan teoría de categoría como el núcleo del formalismo matemático.
• Semánticas concurrentes: Es un término comodín que contiene cualquier semántica formal que describa procesos computacionales concurrentes. Históricamente, importantes formalismos concurrentes han incluido el modelo de actor y el procesamiento de álgebras.
• Semántica de Juegos: Utilizan una metáfora inspirada en la teoría de juegos.
• Semánticas de predicado transformador: Desarrolladas por Edsger W. Dijkstra, describen el significado de un fragmento de un programa como la función que transforma una post-condición a la precondición necesaria para establecerla.

Describiendo las relaciones

Por una variedad de razones, uno pudiera querer describir las relaciones entre diferentes semánticas formales. Por ejemplo:

• Para probar que una semántica operacional particular para un lenguaje satisface las fórmulas lógicas de una semántica axiomática para ese lenguaje. Esta prueba demuestra que es lógico ver una estrategia de interpretación (operacional) usando un sistema de pruebas (axiomático).

• Para probar que una semántica operacional sobre una máquina de alto nivel se relaciona con una bisimulación con las semánticas 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 máquina abstracta de alto nivel de un lenguaje dado. Esta prueba demuestra que la máquina de bajo nivel “implementa completamente” la máquina de alto nivel.

También es posible relacionar múltiples semánticas a través de abstracciones utilizando la teoría de interpretación abstracta.

Enlaces externos

Aaby, Anthony (2004). Introducción a los lenguajes de programación. Semantics.

• Datos: Q1437428