Semántica denotacional

Estudio de lenguajes de programación a través de objetos matemáticos.

En informática , la semántica denotacional (conocida inicialmente como semántica matemática o semántica de Scott-Strachey ) es un enfoque de formalización de 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 los lenguajes de programación incluyen la semántica axiomática y la semántica operacional .

En términos generales, la semántica denotacional se ocupa de encontrar objetos matemáticos llamados dominios que representan lo que hacen los programas. Por ejemplo, los programas (o frases de programas) 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 .

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. ^{[1] [2]} Tal como fue desarrollada originalmente por Strachey y Scott, la semántica denotacional proporcionaba el significado de un programa informático como una función que mapeaba la entrada en la salida. ^[2] Para dar significados 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 el trabajo en la 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 usan capacidades como concurrencia y excepciones , por ejemplo, Concurrent ML , ^[4] CSP , ^[5] y Haskell . ^[6] La semántica de estos lenguajes 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 se pueden evaluar 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 lanzar una excepción que podría terminar la ejecución del otro. Las secciones siguientes describen casos especiales de la semántica de estos lenguajes de programación modernos.

Significados de 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*mproduce una denotación cuando se le proporciona un entorno que tiene un enlace para sus dos variables libres: ny m. Si en el entorno ntiene el valor 3 y mtiene 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 sin definir en caso contrario.

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 darle 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 a factorial. Al principio, empezamos sin llamadas, por lo tanto, no hay nada definido. En la siguiente aproximación, podemos agregar el par ordenado (0,1), porque esto no requiere llamar a factorial nuevamente. De manera similar, podemos agregar (1,1), (2,2), etc., agregando un par en cada aproximación sucesiva porque calcular factorial(n) requiere n+1 llamadas. En el límite obtenemos una función total de a definida en todas partes en su dominio. ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

Formalmente, modelamos cada aproximación como una función parcial . Nuestra aproximación consiste entonces en aplicar repetidamente una función que implementa "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 ): ${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$ ${\displaystyle F:(\mathbb {N} \rightharpoonup \mathbb {N} )\to (\mathbb {N} \rightharpoonup \mathbb {N} )}$Map<int,int> ${\displaystyle \mathbb {N} \rightharpoonup \mathbb {N} }$

int factorial_no_recursivo ( Map < int , int > factorial_menos_definido , int n ) { si ( n == 0 ) entonces devuelve 1 ; de lo contrario si ( fprev = lookup ( factorial_menos_definido , n -1 )) entonces devuelve n * fprev ; de lo contrario devuelve NO_DEFINIDO ; }                         Mapa < int , int > F ( Mapa < int , int > factorial_menos_definido ) { Mapa < int , int > nuevo_factorial = Mapa . empty (); para ( int n en todos < int > ()) { si ( f = factorial_no_recursivo ( factorial_menos_definido , n ) != NO_DEFINIDO ) nuevo_factorial . put ( n , f ); } devolver nuevo_factorial ; }                         

Luego 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, como 1, y no está definida en ningún 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 a . Las funciones parciales forman un orden parcial de cadena completa utilizando ⊆ como ordenamiento. Además, este proceso iterativo de mejores aproximaciones de la función factorial forma una aplicación expansiva (también llamada progresiva) porque cada una utiliza ⊆ como ordenamiento. Entonces, por un teorema de punto fijo (específicamente el teorema de Bourbaki-Witt ), existe un punto fijo para este proceso iterativo. ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$ ${\displaystyle F^{i}\leq F^{i+1}}$

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

${\displaystyle \bigcup _{i\in \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 demostrarlo 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 programas secuenciales no deterministas. Escribiendo P para un constructor de dominio de potencia, el dominio P ( D ) es el dominio de los cálculos no deterministas del tipo denotado por D .

Existen dificultades con la equidad y la ilimitación en los modelos teóricos del dominio del no determinismo. ^[7]

Semántica denotacional de la 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 esta razón se han introducido varios modelos nuevos . A principios de la década de 1980, la gente comenzó a usar el estilo de semántica denotacional para dar semántica para lenguajes concurrentes. Los ejemplos incluyen el trabajo de Will Clinger con el modelo de actor ; 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 (ver por ejemplo los diversos modelos denotacionales para CSP ^[5] ).

Recientemente, Winskel y otros han propuesto la categoría de profunctores como una teoría de dominio para la concurrencia. ^{[10] [11]}

Semántica denotacional del estado

Los estados (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 con 3asignado a x. El operador de secuenciación " ;" se denota por composición de funciones. Las construcciones de punto fijo se utilizan entonces para dar una semántica a las construcciones de bucle, como " while".

Las cosas se complican más al modelar 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. ^{[12] [13]}

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

 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 que se modificaran los elementos de una lista recursiva de este tipo.

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

tipo de datos  D  =  D  de  ( D  →  D )

El problema de resolver ecuaciones de dominios se relaciona con encontrar dominios que modelen este tipo de tipos de datos. Un enfoque, en términos generales, consiste en considerar la colección de todos los dominios como un dominio en sí mismo y luego resolver la definición recursiva que se encuentra allí.

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

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 tipo string list.

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.

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

Semántica denotacional para programas de complejidad restringida

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]

Semántica denotacional de la secuencialidad

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 parte en la década de 1990 con el desarrollo de la semántica de juegos y también con técnicas que involucraban relaciones lógicas . ^[16] Para más detalles, consulte la página sobre PCF.

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

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 un código de bytes. (De hecho, la semántica denotacional convencional puede considerarse 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 completa, ayudan a satisfacer las preocupaciones de seguridad. ^{[17] [18]}

Abstracción

A menudo se considera importante conectar la semántica denotacional con la semántica operacional . Esto es especialmente importante cuando la semántica denotacional es más bien matemática y abstracta, y la semántica operacional 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 de sintaxis : las denotaciones de los programas no deben involucrar la sintaxis del lenguaje fuente.
2. Adecuación (o solidez) : Todos los programas observablemente distintos tienen denotaciones distintas;
3. Abstracción completa : todos los programas observacionalmente equivalentes tienen denotaciones iguales.

En el caso de la semántica tradicional, la adecuación y la abstracción completa pueden entenderse, en líneas generales, como el requisito de que "la equivalencia operacional coincida con la igualdad denotacional". En el caso de la semántica denotacional en modelos más intensionales, como el modelo de actores y los cálculos de procesos , existen diferentes nociones de equivalencia dentro de cada modelo, por lo que los conceptos de adecuación y de abstracción completa son un tema de debate y más difíciles de precisar. Además, la estructura matemática de la semántica operacional y la semántica denotacional pueden llegar a ser muy parecidas.

Otras propiedades deseables que podríamos desear mantener entre la semántica operacional y denotacional son:

1. Constructivismo : El constructivismo se ocupa de si se puede demostrar la existencia de los elementos del dominio mediante 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. Consulte la sección sobre composicionalidad a continuación.
3. Completitud total o definibilidad : cada morfismo del modelo semántico debe ser la denotación de un programa. ^[19]

Composicionalidad

Un aspecto importante de la semántica denotacional de los lenguajes de programación es la composicionalidad, por 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 consiste en 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 compositiva porque se da de la siguiente manera. Comenzamos considerando fragmentos de programas, es decir, programas con variables libres. Un contexto de tipificación asigna un tipo a cada variable libre. Por ejemplo, en la expresión ( x + y ) se podría considerar en un contexto de tipificación ( x : nat, y : nat). Ahora damos una semántica denotacional a fragmentos de programas, utilizando 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 que denota el tipo τ. Por ejemplo, el significado de tipo natdebería ser el dominio de los números naturales: 〚nat〛= _⊥ . ${\displaystyle \mathbb {N} }$
2. Del significado de los tipos derivamos un significado para los contextos de tipificación. Establecemos 〚x ₁ :τ ₁ ,..., x _n :τ _n〛 = 〚 τ ₁〛× ... ×〚τ _n〛. Por ejemplo, 〚x : nat, y : nat〛= _⊥ × _⊥ . Como caso especial, el significado del contexto de tipificación vacío, sin variables, es el dominio con un elemento, denotado 1. ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$
3. Finalmente, debemos darle un significado a cada fragmento de programa en contexto de tipificación. Supongamos que P es un fragmento de programa de tipo σ, en contexto de tipificación Γ, a menudo escrito Γ⊢ P :σ. Entonces el significado de este programa en contexto de tipificación debe ser una función continua 〚Γ⊢ P :σ〛:〚Γ〛→〚σ〛. Por ejemplo, 〚⊢7: nat〛:1→ _⊥ es la función "7" constante, mientras que 〚x : , y : ⊢ x + y : 〛: _⊥ × _⊥ → _⊥ es la función que suma dos números. ${\displaystyle \mathbb {N} }$natnatnat ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

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 : 〛: _⊥ × _⊥ → _⊥ . ${\displaystyle \mathbb {N} }$nat ${\displaystyle \mathbb {N} }$natnatnat ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

De hecho, este es un esquema general para la semántica denotacional compositiva. No hay nada específico sobre dominios y funciones continuas aquí. Uno puede trabajar con una categoría diferente en su lugar. 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 recursión general, podemos arreglárnoslas con la categoría de conjuntos y funciones . Para un lenguaje con efectos secundarios, podemos trabajar en la categoría de Kleisli para una mónada. Para un lenguaje con estado, podemos trabajar en una categoría de functor . 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]

Semántica versus implementación

Según Dana Scott (1980): ^[21]

No es necesario que la semántica determine una implementación, pero debería proporcionar criterios para demostrar que una implementación es correcta.

Según Clinger (1981): ^{[22] : 79}

Sin embargo, por lo general, la semántica formal de un lenguaje de programación secuencial convencional puede interpretarse como una implementación (ineficiente) del lenguaje. Sin embargo, una semántica formal no siempre tiene por qué proporcionar dicha implementación, y creer que la semántica debe proporcionar una implementación conduce a una confusión sobre la semántica formal de los lenguajes concurrentes. Dicha confusión es dolorosamente evidente cuando se dice que la presencia de un no determinismo ilimitado en la semántica de un lenguaje de programación implica que el lenguaje de programación no se puede implementar.

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 considerarse 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 . En el ámbito de la informática, existen conexiones con la interpretación abstracta , la verificación de programas y la comprobación de modelos .

Referencias

1. Dana S. Scott. Esquema de una teoría matemática de la computación. Monografía técnica PRG-2, Laboratorio de Computación de la Universidad de Oxford, Oxford, Inglaterra, noviembre de 1970.
2. Dana Scott y Christopher Strachey . Hacia una semántica matemática para lenguajes informáticos. Monografía técnica del Oxford Programming Research Group. PRG-6. 1971.
3. Jan Jürjens. J. Juegos en la semántica de los lenguajes de programación: una introducción elemental. Synthese 133, 131–158 (2002). https://doi.org/10.1023/A:1020883810034
4. John Reppy "ML concurrente: diseño, aplicación y semántica" en Springer-Verlag, Lecture Notes in Computer Science , vol. 693, 1993
5. AW Roscoe . "La teoría y la práctica de la concurrencia", Prentice-Hall. Revisado en 2005.
6. Simon Peyton Jones , Alastair Reid, Fergus Henderson, Tony Hoare y Simon Marlow. "Una semántica para excepciones imprecisas". Conferencia sobre diseño e implementación de lenguajes de programación. 1999.
7. Levy, Paul Blain (2007). "Amb rompe la precisión, Amb terrestre no". Electron. Notes Theor. Comput. Sci . 173 : 221–239. doi : 10.1016/j.entcs.2007.02.036 .
8. Semántica de estructura de eventos para CCS y lenguajes relacionados . Informe de investigación de DAIMI, Universidad de Aarhus, 67 pp., abril de 1983.
9. Nissim Francez , CAR Hoare , Daniel Lehmann y Willem-Paul de Roever. "Semántica del no determinismo, concurrencia y comunicación", Journal of Computer and System Sciences . Diciembre de 1979.
10. Cattani, Gian Luca; Winskel, Glynn (2005). "Profunctores, mapas abiertos y bisimulación". Estructuras matemáticas en informática . 15 (3): 553–614. CiteSeerX 10.1.1.111.6243 . doi :10.1017/S0960129505004718. S2CID  16356708. 
11. Nygaard, Mikkel; Winskel, Glynn (2004). "Teoría de dominios para concurrencia". Theor. Comput. Sci . 316 (1–3): 153–190. doi : 10.1016/j.tcs.2004.01.029 .
12. Peter W. O'Hearn , John Power, Robert D. Tennent, Makoto Takeyama. Revisión del control sintáctico de la interferencia. Electron. Notes Theor. Comput. Sci. 1. 1995.
13. Frank J. Oles. Un enfoque teórico de categorías para la semántica de la programación . Tesis doctoral, Universidad de Syracuse , Nueva York, EE.UU., 1982.
14. Reus, Bernhard; Streicher, Thomas (2004). "Semántica y lógica de los cálculos de objetos". Theor. Comput. Sci . 316 (1): 191–213. doi : 10.1016/j.tcs.2004.01.030 .
15. Baillot, P. (2004). "Espacios de coherencia estratificados: una semántica denotacional para lógica lineal ligera". Theor. Comput. Sci . 318 (1–2): 29–55. doi : 10.1016/j.tcs.2003.10.015 .
16. O'Hearn, PW; Riecke, JG (julio de 1995). "Relaciones lógicas de Kripke y PCF". Información y computación . 120 (1): 107–116. doi : 10.1006/inco.1995.1103 . S2CID  6886529.
17. Martin Abadi. "Protección en las traducciones de lenguajes de programación". Actas de ICALP'98 . LNCS 1443. 1998.
18. Kennedy, Andrew (2006). "Securing the .NET programming model" (Protección del modelo de programación .NET). Theor. Comput. Sci . 364 (3): 311–7. doi : 10.1016/j.tcs.2006.08.014 .
19. Curien, Pierre-Louis (2007). "Definibilidad y abstracción completa". Notas electrónicas en informática teórica . 172 : 301–310. doi : 10.1016/j.entcs.2007.02.011 .
20. Milner, Robin (2009). El espacio y el movimiento de los agentes comunicantes . Cambridge University Press. ISBN 978-0-521-73833-0.Borrador de 2009 Archivado el 2 de abril de 2012 en Wayback Machine .
21. "¿Qué es la semántica denotacional?", MIT Laboratory for Computer Science Distinguished Lecture Series, 17 de abril de 1980, citado en Clinger (1981).
22. Clinger, William D. (mayo de 1981). Fundamentos de la semántica de actores (tesis doctoral). Instituto Tecnológico de Massachusetts. hdl : 1721.1/6935 . AITR-633.

Lectura adicional

Libros de texto

• Milne, RE; Strachey, C. (1976). Una teoría de la semántica de los lenguajes de programación . ISBN 978-1-5041-2833-9.
• Gordon, MJC (2012) [1979]. La descripción denotacional de los lenguajes de programación: una introducción. Springer. ISBN 978-1-4612-6228-2.
• Stoy, Joseph E. (1977). Semántica denotacional: el enfoque Scott-Strachey para la semántica de lenguajes de programación . MIT Press. ISBN 978-0-262-19147-0.(Un libro de texto clásico, aunque anticuado.)
• Schmidt, David A. (1986). Semántica denotacional: una metodología para el desarrollo del lenguaje . Allyn & Bacon. ISBN 978-0-205-10450-5.
  • Agotado actualmente; versión electrónica gratuita disponible: Schmidt, David A. (1997) [1986]. Semántica denotacional: una metodología para el desarrollo del lenguaje. Universidad Estatal de Kansas.
• Gunter, Carl (1992). Semántica de lenguajes de programación: estructuras y técnicas . MIT Press. ISBN 978-0-262-07143-7.
• Winskel, Glynn (1993). Semántica formal de lenguajes de programación . MIT Press. ISBN 978-0-262-73103-4.
• Tennent, RD (1994). "Semántica denotacional". En Abramsky, S.; Gabbay, Dov M.; Maibaum, TSE (eds.). Estructuras semánticas . Manual de lógica en informática. Vol. 3. Oxford University Press. págs. 169–322. ISBN. 978-0-19-853762-5.
• Abramsky, S .; Jung, A. (1994). "Teoría del dominio" (PDF) . Abramsky, Gabbay y Maibaum 1994 .
• Stoltenberg-Hansen, V.; Lindström, I.; Griffor, ER (1994). Teoría matemática de dominios . Cambridge University Press. ISBN 978-0-521-38344-8.

Notas de la conferencia

• Winskel, Glynn. "Semántica denotacional" (PDF) . Universidad de Cambridge.

Otras referencias

• Greif, Irene (agosto de 1975). Semántica de los procesos paralelos de comunicación (PDF) (tesis doctoral). Proyecto MAC. Instituto Tecnológico de Massachusetts. ADA016302.
• Plotkin, GD (1976). "Una construcción de dominio de potencia". SIAM J. Comput . 5 (3): 452–487. CiteSeerX  10.1.1.158.4318 . doi :10.1137/0205035.
• Dijkstra, Edsger W. (1976). Una disciplina de programación . Serie Prentice-Hall sobre computación automática. Englewood Cliffs, NJ ISBN 0-13-215871-X.OCLC 1958445  .{{cite book}}: CS1 maint: location missing publisher (link)
• Apto, Krzysztof R .; de Bakker, JW (1976). Ejercicios de semántica denotacional . Afdeling Informática. Ámsterdam: Mathematisch Centrum. OCLC  63400684.
• De Bakker, JW (1976). "Revisitando los puntos menos fijos". Ciencias de la computación teórica . 2 (2): 155–181. doi : 10.1016/0304-3975(76)90031-1 .
• Smyth, Michael B. (1978). "Dominios de potencia". J. Comput. Syst. Sci . 16 : 23–36. doi : 10.1016/0022-0000(78)90048-X .
• Francez, Nissim; Hoare, CAR; Lehmann, Daniel; de Roever, Willem-Paul (diciembre de 1979). Semántica del no determinismo, la concurrencia y la comunicación . Notas de clase en informática. Vol. 64. págs. 191–200. doi :10.1007/3-540-08921-7_67. hdl :1874/15886. ISBN . 978-3-540-08921-6. {{cite book}}: |work=ignorado ( ayuda )
• Lynch, Nancy ; Fischer, Michael J. (1979). "Sobre la descripción del comportamiento de los sistemas distribuidos". En Kahn, G. (ed.). Semántica de computación concurrente: actas del simposio internacional, Évian, Francia, 2-4 de julio de 1979 . Springer. ISBN 978-3-540-09511-8.
• Schwartz, Jerald (1979). "Semántica denotacional del paralelismo". Kahn 1979 .
• Wadge, William (1979). "Un tratamiento extensional del bloqueo del flujo de datos". Kahn 1979 .
• Back, Ralph-Johan (1980). "Semántica del no determinismo ilimitado". En de Bakker, Jaco; van Leeuwen, Jan (eds.). Autómatas, lenguajes y programación. Apuntes de clase en informática. Vol. 85. Berlín, Heidelberg: Springer. págs. 51–63. doi :10.1007/3-540-10003-2_59. ISBN 978-3-540-39346-7.OCLC 476017025  .
• Park, David (1980). "Sobre la semántica del paralelismo justo". En Bjøorner, Dines (ed.). Resumen de especificaciones de software (PDF) . Lecture Notes in Computer Science. Vol. 86. Berlín, Heidelberg: Springer Berlin Heidelberg. págs. 504–526. doi :10.1007/3-540-10007-5_47. ISBN 978-3-540-10007-2.
• Allison, L. (1986). Introducción práctica a la semántica denotacional. Cambridge University Press. ISBN 978-0-521-31423-7.
• América, P.; de Bakker, J.; Kok, JN; Rutten, J. (1989). "Semántica denotacional de un lenguaje paralelo orientado a objetos". Información y Computación . 83 (2): 152–205. doi : 10.1016/0890-5401(89)90057-6 . S2CID  2405175.
• Schmidt, David A. (1994). La estructura de los lenguajes de programación tipados . MIT Press. ISBN 978-0-262-69171-0.

Enlaces externos

• Semántica denotacional. Resumen del libro de Lloyd Allison
• Schreiner, Wolfgang (1995). "Estructura de lenguajes de programación I: Semántica denotacional". Apuntes del curso .