Semántica denotacional

En informática, la semántica denotacional (inicialmente conocida como semántica matemática o semántica de Scott-Strachey) es un enfoque para formalizar los significados de lenguajes de programación mediante la construcción de objetos matemáticos (llamados denotaciones) que describen los significados de las expresiones de los lenguajes. Otros enfoques que proporcionan la semántica formal de los lenguajes de programación incluyen la semántica axiomática y la semántica operativa.

En términos generales, la semántica denotacional se ocupa de encontrar objetos matemáticos llamados dominios que representen lo que hacen los programas. Por ejemplo, los programas (o frases de programa) pueden estar representados por funciones parciales o por juegos entre el entorno y el sistema.

Un principio importante de la semántica denotacional es que la semántica debe ser composicional: la denotación de una frase de programa debe construirse a partir de las denotaciones de sus subfrases.

Desarrollo histórico

La semántica denotacional se originó en el trabajo de Christopher Strachey y Dana Scott publicado a principios de la década de 1970. Tal como la desarrollaron originalmente Strachey y Scott, la semántica denotacional proporcionó el significado de un programa de computadora como una función que mapeaba la entrada en la salida. Para dar significado a los programas definidos recursivamente, Scott propuso trabajar con funciones continuas entre dominios, específicamente órdenes parciales completas. Como se describe a continuación, se ha continuado investigando la semántica denotacional adecuada para aspectos de los lenguajes de programación como la secuencialidad, la concurrencia, el no determinismo y el estado local.

La semántica denotacional se ha desarrollado para lenguajes de programación modernos que usan capacidades como concurrencia y excepciones, por ejemplo, ML concurrente, CSP y Haskell. La semántica de estos idiomas es compositiva en el sentido de que el significado de una frase depende de los significados de sus subfrases. Por ejemplo, el significado de la expresión aplicativa f(E1,E2) se define en términos de la semántica de sus subfrases f, E1 y E2. En un lenguaje de programación moderno, E1 y E2 pueden evaluarse simultáneamente y la ejecución de uno de ellos puede afectar al otro al interactuar a través de objetos compartidos, lo que hace que sus significados se definan en términos de cada uno. Además, E1 o E2 pueden generar una excepción que podría terminar la ejecución del otro. Las siguientes secciones describen casos especiales de la semántica de estos lenguajes de programación modernos.

Significados de los programas recursivos

La semántica denotacional se atribuye a una frase de programa como una función de un entorno (que contiene los valores actuales de sus variables libres) a su denotación. Por ejemplo, la frase n*m produce una denotación cuando se proporciona con un entorno que tiene enlace para sus dos variables libres: n y m. Si en el entorno n tiene el valor 3 y < code class="mw-highlight mw-highlight-lang-text mw-content-ltr" id="" style="" dir="ltr">m tiene el valor 5, entonces la denotación es 15.

Una función se puede representar como un conjunto de pares ordenados de argumentos y valores de resultado correspondientes. Por ejemplo, el conjunto {(0,1), (4,3)} denota una función con el resultado 1 para el argumento 0, el resultado 3 para el argumento 4 y sin definir en caso contrario.

Considere, por ejemplo, la función factorial, que podría definirse recursivamente como:

int factorial()int n) {} si ()n == 0) entonces retorno 1; más retorno n * factorial()n-1); }

Para proporcionar un significado para esta definición recursiva, la denotación se construye como límite de aproximaciones, donde cada aproximación limita el número de llamadas a factorial. Al principio, comenzamos sin llamadas - por lo tanto nada se define. En la siguiente aproximación, podemos añadir el par ordenado (0,1), porque esto no requiere volver a llamar factorial. Del mismo modo podemos añadir (1,1), (2,2), etc., añadiendo un par cada aproximación sucesiva porque computación factorial(n) Requisitos n+1 llamadas. En el límite obtenemos una función total desde ${displaystyle mathbb {N}$ a ${displaystyle mathbb {N}$ definido en todas partes en su dominio.

Formalmente modelamos cada aproximación como una función parcial ${displaystyle mathbb {N} rightharpoonup mathbb {N}$. Nuestra aproximación entonces se aplica repetidamente una función "hacer una función factorial parcial más definida" ${displaystyle F:(mathbb {N} rightharpoonup mathbb {N})to (mathbb {N} rightharpoonup mathbb {N})}$, comenzando por la función vacía (conjunto vacío). F podría definirse en código como sigue (utilizando Map para ${displaystyle mathbb {N} rightharpoonup mathbb {N}$):

int factorial_norecursivo()Mapa.int,int■ factorial_less_definido, int n){} si ()n == 0) entonces retorno 1; más si ()fprev = Lookup()factorial_less_definido, n-1) entonces retorno n * fprev; más retorno NOT_DEFINED;}Mapa.int,int■ F()Mapa.int,int■ factorial_less_definido){}  Mapa.int,int■ new_factorial = Mapa.vacío(); para()int n dentro Todos.int■()) {} si()f = factorial_norecursivo()factorial_less_definido, n) ! NOT_DEFINED) new_factorial.#()n,f); } retorno new_factorial;}

Entonces podemos introducir la notación Fⁿ para indicar F aplicada n veces.

• F⁰({}) es la función parcial totalmente indefinida, representada como el conjunto {};
• F¹({}) es la función parcial representada como el conjunto {(0,1)}: se define en 0, a ser 1, e indefinido en otro lugar;
• F⁵({}) es la función parcial representada como el conjunto {(0,1), (1,1), (2,2), (3,6), (4,24)}: se define para los argumentos 0,1,2,3,4.

Este proceso iterativo construye una secuencia de funciones parciales de ${displaystyle mathbb {N}$ a ${displaystyle mathbb {N}$. Las funciones parciales forman un orden parcial completo de cadena utilizando ⊆ como el pedido. Además, este proceso iterativo de mejores aproximaciones de la función factorial forma un mapeo expansivo (también llamado progresivo) porque cada ${displaystyle F^{i}leq F^{i+1}$ usando ⊆ como el pedido. Así que por un teorema de punto fijo (específicamente Bourbaki-Witt teorem), existe un punto fijo para este proceso iterativo.

En este caso, el punto fijo es el límite superior mínimo de esta cadena, que es el factorial, que se puede expresar como la unión

${displaystyle bigcup _{iin mathbb {N}F^{i}({}).}$

El punto fijo que encontramos es el punto menos fijo de F, porque nuestra iteración comenzó con el elemento más pequeño del dominio (el conjunto vacío). Para probar esto necesitamos un teorema de punto fijo más complejo como el teorema de Knaster-Tarski.

Semántica denotacional de programas no deterministas

El concepto de dominios de potencia se ha desarrollado para dar una semántica denotacional a los programas secuenciales no deterministas. Escribiendo P para un constructor de dominio de potencia, el dominio P(D) es el dominio de cálculos no deterministas de tipo indicado por D.

Existen dificultades con la equidad y la falta de límites en los modelos de no determinismo basados en la teoría del dominio.

Semántica denotacional de concurrencia

Muchos investigadores han argumentado que los modelos teóricos de dominio dados anteriormente no son suficientes para el caso más general de computación concurrente. Por este motivo se han introducido varios modelos nuevos. A principios de la década de 1980, la gente comenzó a usar el estilo de la semántica denotacional para dar semántica a los lenguajes concurrentes. Los ejemplos incluyen el trabajo de Will Clinger con el actor modelo; el trabajo de Glynn Winskel con estructuras de eventos y redes de Petri; y el trabajo de Francez, Hoare, Lehmann y de Roever (1979) sobre semántica de trazas para CSP. Todas estas líneas de investigación siguen bajo investigación (ver, por ejemplo, los diversos modelos denotacionales para CSP).

Recientemente, Winskel y otros han propuesto la categoría de profunctores como una teoría de dominio para la concurrencia.

Semántica denotacional de estado

El estado (como un montón) y las características imperativas simples se pueden modelar directamente en la semántica denotacional descrita anteriormente. Todos los libros de texto a continuación tienen los detalles. La idea clave es considerar un comando como una función parcial en algún dominio de estados. El significado de "x:=3 " es entonces la función que lleva un estado al estado con 3 asignado a x. El operador de secuenciación ";" se denota por la composición de funciones. Luego se utilizan construcciones de punto fijo para dar una semántica a las construcciones de bucle, como "mientras".

Las cosas se vuelven más difíciles en el modelado de programas con variables locales. Un enfoque es no trabajar más con dominios, sino interpretar los tipos como funtores de alguna categoría de mundos a una categoría de dominios. Los programas se denotan entonces por funciones continuas naturales entre estos funtores.

Denotaciones de tipos de datos

Muchos lenguajes de programación permiten a los usuarios definir tipos de datos recursivos. Por ejemplo, el tipo de listas de números se puede especificar mediante

datatype lista = Cons de Nat * lista Silencio Vacío

Esta sección trata solo de estructuras de datos funcionales que no pueden cambiar. Los lenguajes de programación imperativos convencionales normalmente permitirían cambiar los elementos de una lista recursiva de este tipo.

Para otro ejemplo: el tipo de denotaciones del cálculo lambda sin tipo es

datatype D = D de ()D → D)

El problema de resolver ecuaciones de dominio tiene que ver con encontrar dominios que modelen este tipo de tipos de datos. Un enfoque, en términos generales, es considerar la colección de todos los dominios como un dominio en sí mismo y luego resolver la definición recursiva allí. Los libros de texto a continuación dan más detalles.

Los tipos de datos polimórficos son tipos de datos que se definen con un parámetro. Por ejemplo, se define el tipo de α lists por

datatype α lista = Cons de α * α lista Silencio Vacío

Las listas de números naturales, entonces, son del tipo nat list , mientras que las listas de cadenas son de lista de cadenas.

Algunos investigadores han desarrollado modelos teóricos de dominio del polimorfismo. Otros investigadores también han modelado el polimorfismo paramétrico dentro de las teorías de conjuntos constructivos. Los detalles se encuentran en los libros de texto que se enumeran a continuación.

Un área de investigación reciente ha involucrado la semántica denotacional para lenguajes de programación basados en objetos y clases.

Semántica denotacional para programas de complejidad restringida

Siguiendo el desarrollo de lenguajes de programación basados en lógica lineal, se ha dado semántica denotacional a lenguajes para uso lineal (ver, por ejemplo, redes de prueba, espacios de coherencia) y también complejidad de tiempo polinomial.

Semántica denotacional de secuencialidad

El problema de la abstracción total para el lenguaje de programación secuencial PCF fue, durante mucho tiempo, una gran pregunta abierta en la semántica denotacional. La dificultad con PCF es que es un lenguaje muy secuencial. Por ejemplo, no hay forma de definir la función paralela o en PCF. Es por esta razón que el enfoque que usa dominios, como se presentó anteriormente, produce una semántica denotacional que no es completamente abstracta.

Esta pregunta abierta se resolvió principalmente en la década de 1990 con el desarrollo de la semántica del juego y también con técnicas que involucran relaciones lógicas. Para más detalles, consulte la página sobre PCF.

Semántica denotacional como traducción de fuente a fuente

A menudo es útil traducir un lenguaje de programación a otro. Por ejemplo, un lenguaje de programación concurrente podría traducirse a un proceso de cálculo; un lenguaje de programación de alto nivel podría traducirse a código de bytes. (De hecho, la semántica denotacional convencional puede verse como la interpretación de los lenguajes de programación en el lenguaje interno de la categoría de dominios).

En este contexto, las nociones de la semántica denotacional, como la abstracción total, ayudan a satisfacer las preocupaciones de seguridad.

Abstracción

A menudo se considera importante conectar la semántica denotacional con la semántica operativa. Esto es especialmente importante cuando la semántica denotacional es bastante matemática y abstracta, y la semántica operativa es más concreta o más cercana a las intuiciones computacionales. Las siguientes propiedades de una semántica denotacional suelen ser de interés.

1. Independencia sintaxis: Las denotaciones de los programas no deben involucrar la sintaxis del lenguaje fuente.
2. Adecuación (o sonido): Todos los programas observably distinct tienen denotaciones distintas;
3. abstracción completa: Todos los programas observacionalmente equivalentes tienen denotaciones iguales.

Para la semántica en el estilo tradicional, la adecuación y la abstracción total pueden entenderse aproximadamente como el requisito de que "la equivalencia operativa coincida con la igualdad denotacional". Para la semántica denotacional en modelos más intensionales, como el modelo de actor y los cálculos de proceso, existen diferentes nociones de equivalencia dentro de cada modelo, por lo que los conceptos de adecuación y abstracción total son un tema de debate y más difíciles de precisar. Además, la estructura matemática de la semántica operativa y la semántica denotacional puede llegar a ser muy similar.

Las propiedades deseables adicionales que podemos desear mantener entre la semántica operativa y denotacional son:

1. Constructivismo: El constructivismo está preocupado por si los elementos de dominio pueden ser mostrados por métodos constructivos.
2. Independencia de la semántica denotacional y operacional: La semántica denotacional debe formalizarse utilizando estructuras matemáticas que sean independientes de la semántica operacional de un lenguaje de programación; Sin embargo, los conceptos subyacentes pueden estar estrechamente relacionados. Vea la sección sobre Compositionality a continuación.
3. Completa integridad o Definición: Cada morfismo del modelo semántico debe ser la denotación de un programa.

Composicionalidad

Un aspecto importante de la semántica denotacional de los lenguajes de programación es la composicionalidad, mediante la cual la denotación de un programa se construye a partir de las denotaciones de sus partes. Por ejemplo, considere la expresión "7 + 4". La composicionalidad en este caso es proporcionar un significado para "7 + 4" en términos de los significados de "7", "4" y "+".

Una semántica denotacional básica en la teoría del dominio es composicional porque se da de la siguiente manera. Comenzamos considerando fragmentos de programa, es decir, programas con variables libres. Un contexto de escritura asigna un tipo a cada variable libre. Por ejemplo, en la expresión (x + y) podría considerarse en un contexto de escritura (x:nat,y:nat). Ahora damos una semántica denotacional a los fragmentos de programa, usando el siguiente esquema.

1. Comenzamos describiendo el significado de los tipos de nuestro lenguaje: el significado de cada tipo debe ser un dominio. Escribimos 〚τ〛 para el dominio denotando el tipo τ. Por ejemplo, el significado del tipo nat debe ser el dominio de los números naturales: 〚nat〛= ${displaystyle mathbb {N}$⊥.
2. Del significado de los tipos derivamos un significado para escribir contextos. Hemos puesto 〚 x1#1,... xn#nτ = τ1〛×... ×n〛. Por ejemplo, 〚x:nat,Sí.:nat〛= ${displaystyle mathbb {N}$⊥×${displaystyle mathbb {N}$⊥. Como caso especial, el significado del contexto de escritura vacía, sin variables, es el dominio con un elemento, denotado 1.
3. Finalmente, debemos dar un significado a cada programa-fragment-in-typing-context. Supongamos que P es un fragmento de programa de tipo σ, en el contexto de la máquina de escribir, a menudo escrito P:σ. Entonces el significado de este programa en texto debe ser una función continua 〚P:σ〛 эΓ→〚σ〛. Por ejemplo, 〚⊢7:nat〛:1→${displaystyle mathbb {N}$⊥ es la función constantemente "7", mientras 〚x:nat,Sí.:nat⊢x+Sí.:nat〛:${displaystyle mathbb {N}$⊥×${displaystyle mathbb {N}$⊥→${displaystyle mathbb {N}$⊥ es la función que añade dos números.

Ahora, el significado de la expresión compuesta (7+4) se determina mediante la composición de las tres funciones 〚⊢7:nat〛:1→${displaystyle mathbb {N}$⊥, 〚⊢4:nat〛:1→${displaystyle mathbb {N}$⊥, y 〚x:nat,Sí.:nat⊢x+Sí.:nat〛:${displaystyle mathbb {N}$⊥×${displaystyle mathbb {N}$⊥→${displaystyle mathbb {N}$⊥.

De hecho, este es un esquema general para la semántica denotacional composicional. No hay nada específico sobre dominios y funciones continuas aquí. En su lugar, se puede trabajar con una categoría diferente. Por ejemplo, en la semántica de juegos, la categoría de juegos tiene juegos como objetos y estrategias como morfismos: podemos interpretar tipos como juegos y programas como estrategias. Para un lenguaje simple sin recursividad general, podemos conformarnos con la categoría de conjuntos y funciones. Para un lenguaje con efectos secundarios, podemos trabajar en la categoría Kleisli para una mónada. Para un lenguaje con estado, podemos trabajar en una categoría de funtores. Milner ha abogado por modelar la ubicación y la interacción trabajando en una categoría con interfaces como objetos y bigrafías como morfismos.

Semántica versus implementación

Según Dana Scott (1980):

No es necesario que los semánticos determinen una aplicación, pero debería establecer criterios para demostrar que una aplicación es correcta.

Según Clinger (1981):

Por lo general, sin embargo, la semántica formal de un lenguaje de programación secuencial convencional puede interpretarse para proporcionar una aplicación (ineficiente) del idioma. Sin embargo, una semántica formal no siempre debe proporcionar tal aplicación, y creer que la semántica debe proporcionar una implementación conduce a confusión acerca de la semántica formal de los idiomas concurrentes. Tal confusión es dolorosamente evidente cuando se dice que la presencia de no determinación sin límites en la semántica de un lenguaje de programación implica que el lenguaje de programación no puede ser implementado.

Conexiones con otras áreas de la informática

Algunos trabajos en semántica denotacional han interpretado los tipos como dominios en el sentido de la teoría de dominios, que puede verse como una rama de la teoría de modelos, lo que lleva a conexiones con la teoría de tipos y la teoría de categorías. Dentro de la informática, existen conexiones con la interpretación abstracta, la verificación de programas y la verificación de modelos.