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 los 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 semántica formal de 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) podrían representarse mediante funciones parciales [1] [2] o mediante juegos [3] entre el entorno y el sistema.
Un principio importante de la semántica denotacional es que la semántica debe ser compositiva : la denotación de una frase de programa debe construirse a partir de las denotaciones de sus subfrases .
La semántica denotacional se originó en el trabajo de Christopher Strachey y Dana Scott publicado a principios de los años setenta. [1] [2] Tal como fue desarrollada originalmente por Strachey y Scott, la semántica denotacional proporcionó el significado de un programa de computadora como una función que asignaba la entrada a la salida. [2] Para dar significados a 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 el trabajo de investigación de la semántica denotacional apropiada 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 utilizan capacidades como concurrencia y excepciones , por ejemplo, Concurrent ML , [4] CSP , [5] y Haskell . [6] 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 podrían 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.
La semántica denotacional se atribuye a una frase de programa como una función desde un entorno (que contiene los valores actuales de sus variables libres) hasta su denotación. Por ejemplo, la frase n*m
produce una denotación cuando se le proporciona un entorno que tiene vinculación para sus dos variables libres: n
y m
. Si en el entorno n
tiene el valor 3 y m
el valor 5, entonces la denotación es 15. [2]
Una función se puede representar como un conjunto de pares ordenados de argumentos y valores de resultados correspondientes. Por ejemplo, el conjunto {(0,1), (4,3)} denota una función con resultado 1 para el argumento 0, resultado 3 para el argumento 4 y, en caso contrario, indefinido.
Consideremos, por ejemplo, la función factorial , que podría definirse recursivamente como:
int factorial ( int n ) { si ( n == 0 ) entonces devuelve 1 ; de lo contrario, devuelve n * factorial ( n -1 ); }
Para dar un significado a esta definición recursiva, la denotación se construye como el límite de aproximaciones, donde cada aproximación limita el número de llamadas al factorial. Al principio, empezamos sin llamadas, por lo que no hay nada definido. En la siguiente aproximación, podemos sumar el par ordenado (0,1), porque esto no requiere volver a llamar al factorial. De manera similar, podemos sumar (1,1), (2,2), etc., agregando un par en cada aproximación sucesiva porque calcular el factorial(n) requiere n+1 llamadas. En el límite obtenemos una función total desde a definida en todas partes de su dominio.
Formalmente modelamos cada aproximación como una función parcial . Nuestra aproximación es entonces aplicar repetidamente una función que implemente "hacer una función factorial parcial más definida", es decir , comenzando con la función vacía (conjunto vacío). F podría definirse en código de la siguiente manera (usando for ):Map<int,int>
int factorial_nonrecursive ( Mapa < int , int > factorial_less_definido , int n ) { if ( n == 0 ) entonces devuelve 1 ; de lo contrario, si ( fprev = búsqueda ( factorial_less_definido , n -1 )) entonces devuelve n * fprev ; de lo contrario , devuelve NOT_DEFINED ; } Mapa < int , int > F ( Mapa < int , int > factorial_less_definido ) { Mapa < int , int > new_factorial = Mapa . vacío (); for ( int n en todo < int > ()) { if ( f = factorial_nonrecursive ( factorial_less_definido , n ) != NOT_DEFINED ) new_factorial . poner ( n , f ); } devolver nuevo_factorial ; }
Luego podemos introducir la notación F n para indicar que F se aplica n veces .
Este proceso iterativo construye una secuencia de funciones parciales desde hasta . Las funciones parciales forman un orden parcial de cadena completa usando ⊆ como orden. Además, este proceso iterativo de mejores aproximaciones de la función factorial forma un mapeo expansivo (también llamado progresivo) porque cada uno usa ⊆ como orden. Entonces, según un teorema del punto fijo (específicamente el teorema de Bourbaki-Witt ), 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 la factorial
función completa, que se puede expresar como la unión
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 demostrar esto necesitamos un teorema del punto fijo más complejo, como el teorema de Knaster-Tarski .
El concepto de dominios de poder se ha desarrollado para dar una semántica denotacional a programas secuenciales no deterministas. Al escribir P para un constructor de dominio de potencia, el dominio P ( D ) es el dominio de cálculos no deterministas de tipo denotado por D .
Hay dificultades con la equidad y la ilimitación en los modelos de no determinismo basados en la teoría de dominio. [7]
Muchos investigadores han argumentado que los modelos teóricos de dominio proporcionados 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 utilizar el estilo de semántica denotacional para dar semántica a 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 ; [8] y el trabajo de Francez, Hoare, Lehmann y de Roever (1979) sobre semántica de trazas para CSP. [9] Todas estas líneas de investigación siguen bajo investigación (véanse, por ejemplo, los diversos modelos denotacionales para CSP [5] ).
Recientemente, Winskel y otros han propuesto la categoría de profunctores como teoría de dominio para la concurrencia. [10] [11]
El estado (como un montón) y las características imperativas simples se pueden modelar directamente en la semántica denotacional descrita anteriormente. 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 3
asignado a x
. El operador de secuenciación " ;
" se indica por la composición de funciones. Luego, las construcciones de punto fijo se utilizan para dar semántica a las construcciones en bucle, como " while
".
Las cosas se vuelven más difíciles al modelar programas con variables locales. Un enfoque consiste en dejar de trabajar con dominios, sino interpretar los tipos como functores de alguna categoría de mundos a una categoría de dominios. Luego, los programas se indican mediante funciones continuas naturales entre estos functores. [12] [13]
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
lista de tipos de datos = Contras de nat * lista | Vacío
Esta sección trata únicamente de estructuras de datos funcionales que no pueden cambiar. Los lenguajes de programación imperativos convencionales normalmente permitirían cambiar los elementos de dicha lista recursiva.
Para otro ejemplo: el tipo de denotaciones del cálculo lambda sin tipo es
tipo de datos 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 tipos de datos polimórficos son tipos de datos que se definen con un parámetro. Por ejemplo, el tipo de α list
s está definido por
tipo de datos α lista = Contras de α * α lista | Vacío
Las listas de números naturales, entonces, son de tipo nat list
, mientras que las listas de cadenas son de string list
.
Algunos investigadores han desarrollado modelos teóricos de polimorfismo de dominio. Otros investigadores también han modelado el polimorfismo paramétrico dentro de teorías de conjuntos constructivas.
Un área de investigación reciente ha involucrado la semántica denotacional para lenguajes de programación basados en objetos y clases. [14]
Tras el desarrollo de lenguajes de programación basados en lógica lineal , se ha dado semántica denotacional a los lenguajes para uso lineal (ver, por ejemplo, redes de prueba , espacios de coherencia ) y también complejidad de tiempo polinomial. [15]
El problema de la abstracción total para el lenguaje de programación secuencial PCF fue, durante mucho tiempo, una gran cuestión 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 utiliza dominios, como se presentó anteriormente, produce una semántica denotacional que no es completamente abstracta.
Esta cuestión abierta se resolvió en gran medida en la década de 1990 con el desarrollo de la semántica de juegos y también con técnicas que implican relaciones lógicas . [16] Para obtener más detalles, consulte la página sobre PCF.
A menudo resulta útil traducir un lenguaje de programación a otro. Por ejemplo, un lenguaje de programación concurrente podría traducirse a un cálculo de procesos ; 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 al lenguaje interno de la categoría de dominios).
En este contexto, nociones de la semántica denotacional, como la abstracción total, ayudan a satisfacer las preocupaciones de seguridad. [17] [18]
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 más bien 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.
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 de 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 parecida.
Propiedades deseables adicionales que quizás deseemos mantener entre la semántica operativa y denotacional son:
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 de dominios es composicional porque se da de la siguiente manera. Empezamos considerando fragmentos de programa, es decir, programas con variables libres. Un contexto de escritura asigna un tipo a cada variable libre. Por ejemplo, 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.
nat
debería ser el dominio de los números naturales: 〚nat
〛= ⊥ .nat
, y : nat
〛= ⊥ × ⊥ . Como caso especial, el significado del contexto de escritura vacío, sin variables, es el dominio con un elemento, denotado 1.nat
〛:1→ ⊥ es la función constantemente "7", mientras que 〚x : , y : ⊢ x + y : 〛: ⊥ × ⊥ → ⊥ es la función que suma dos números.nat
nat
nat
Ahora, el significado de la expresión compuesta (7+4) se determina componiendo las tres funciones 〚⊢7: nat
〛:1→ ⊥ , 〚⊢4: 〛:1→ ⊥ , y 〚x : , y : ⊢ x + y : 〛: ⊥ × ⊥ → ⊥ .nat
nat
nat
nat
De hecho, éste es un esquema general para la semántica denotacional compositiva. Aquí no hay nada específico sobre dominios y funciones continuas. 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 idioma con estado, podemos trabajar en una categoría de funtor . Milner ha abogado por modelar la ubicación y la interacción trabajando en una categoría con interfaces como objetos y bigrafos como morfismos. [20]
Según Dana Scott (1980): [21]
Según Clinger (1981): [22] : 79
Algunos trabajos en semántica denotacional han interpretado los tipos como dominios en el sentido de 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 .
{{cite book}}
: CS1 maint: location missing publisher (link){{cite book}}
: |work=
ignorado ( ayuda )