Semántica de lenguajes de programación
From Wikipedia, the free encyclopedia
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.
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.
