Semántica denotacional

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

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 .

Desarrollo historico

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 entre sí. 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.

Significados de programas recursivos

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*mproduce una denotación cuando se le proporciona un entorno que tiene vinculación para sus dos variables libres: ny m. Si en el entorno ntiene el valor 3 y mel 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. ${\displaystyle \mathbb {N} }$ ${\displaystyle \mathbb {N} }$

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 ): ${\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_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 todos < 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 ⁿ para indicar que F se aplica 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)}: está definida en 0, es 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 argumentos 0,1,2,3,4.

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. ${\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 se puede expresar 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 demostrar esto necesitamos un teorema del punto fijo más complejo, como el teorema de Knaster-Tarski .

Semántica denotacional de programas no deterministas.

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]

Semántica denotacional de la concurrencia

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 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 (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]}

Semántica denotacional del estado

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 3asignado 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]}

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 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 α lists 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]

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 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 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.

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 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]}

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 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.

1. Independencia de sintaxis : las denotaciones de programas no deben involucrar la sintaxis del idioma 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.

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:

1. Constructivismo : El constructivismo se ocupa de si se puede demostrar que los elementos del dominio existen mediante métodos constructivos.
2. Independencia de la semántica denotacional y operativa : La semántica denotacional debe formalizarse utilizando estructuras matemáticas que sean independientes de la semántica operativa 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. Total integridad 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, 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.

1. Comenzamos describiendo el significado de los tipos de nuestra lengua: 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 tipográficos. Establecemos 〚x ₁ :τ ₁ ,..., x _n :τ _n〛 = 〚 τ ₁〛× ... ×〚τ _n〛. Por ejemplo, 〚x : nat, y : nat〛= _⊥ × _⊥ . Como caso especial, el significado del contexto de escritura 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-mecanografía. Supongamos que P es un fragmento de programa de tipo σ, en el contexto de escritura Γ, a menudo escrito Γ⊢ P :σ. Entonces el significado de este programa en contexto de escritura debe ser una función continua 〚Γ⊢ P :σ〛:〚Γ〛→〚σ〛. Por ejemplo, 〚⊢7: nat〛:1→ _⊥ es la función constantemente "7", 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: 〛: nat1→ _⊥ , 〚⊢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, é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 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 debe proporcionar criterios para demostrar que una implementación es correcta.

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

Sin embargo, normalmente 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 necesita proporcionar tal implementación, y creer que la semántica debe proporcionar una implementación lleva a confusión sobre la semántica formal de los lenguajes concurrentes. Tal 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 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 .

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 Grupo de Investigación de Programación de Oxford. PRG-6. 1971.
3. Jan Jürjens. J. Juegos en la semántica de los lenguajes de programación: una introducción elemental. Síntesis 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 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” Jornada sobre Diseño e Implementación de Lenguajes de Programación. 1999.
7. Levy, Paul Blain (2007). "Amb rompe la precisión, Ground Amb no". Electrón. Notas teóricas. Computadora. Ciencia . 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 DAIMI, Universidad de Aarhus, 67 págs., abril de 1983.
9. Nissim Francez , CAR Hoare , Daniel Lehmann y Willem-Paul de Roever. "Semántica del no determinismo, concurrencia y comunicación", Revista de Ciencias de la Computación y Sistemas . 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 dominio para la concurrencia". Teor. Computadora. Ciencia . 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. Electrón. Notas teóricas. Computadora. Ciencia. 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. mil novecientos ochenta y dos.
14. Reus, Bernhard; Streicher, Thomas (2004). "Semántica y lógica del cálculo de objetos". Teor. Computadora. Ciencia . 316 (1): 191–213. doi : 10.1016/j.tcs.2004.01.030 .
15. Baillot, P. (2004). "Espacios de coherencia estratificada: una semántica denotacional para la lógica lineal ligera". Teor. Computadora. Ciencia . 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. Martín Abadi. "Protección en traducciones de lenguajes de programación". Proc. del ICALP'98 . LNCS 1443. 1998.
18. Kennedy, Andrés (2006). "Asegurar el modelo de programación .NET". Teor. Computadora. Ciencia . 364 (3): 311–7. doi : 10.1016/j.tcs.2006.08.014 .
19. Curien, Pierre-Louis (2007). "Definibilidad y abstracción total". Apuntes Electrónicos 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 . Prensa de la Universidad de Cambridge. 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?", Serie de conferencias distinguidas del Laboratorio de Ciencias de la Computación del MIT, 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 de Tecnología de Massachusetts. hdl : 1721.1/6935 . AITR-633.

Otras lecturas

Libros de texto

• Milne, RE; Strachey, C. (1976). Una teoría de la semántica del lenguaje 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. Saltador. ISBN 978-1-4612-6228-2.
• Stoy, José E. (1977). Semántica denotacional: el enfoque de Scott-Strachey para la semántica del lenguaje de programación . Prensa del MIT. 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 y tocino. ISBN 978-0-205-10450-5.
  • agotado ahora; 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.
• Günter, Carl (1992). Semántica de lenguajes de programación: estructuras y técnicas . Prensa del MIT. ISBN 978-0-262-07143-7.
• Winskel, Glynn (1993). Semántica formal de lenguajes de programación . Prensa del MIT. 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. Prensa de la Universidad de Oxford. 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.; Lindstrom, I.; Griffin, ER (1994). Teoría Matemática de Dominios . Prensa de la Universidad de Cambridge. ISBN 978-0-521-38344-8.

Notas de lectura

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

otras referencias

• Greif, Irene (agosto de 1975). Semántica de la comunicación de procesos paralelos (PDF) (tesis doctoral). Proyecto MAC. Instituto de Tecnología de Massachusetts. ADA016302.
• Plotkin, GD (1976). "Una construcción en el dominio del poder". SIAM J. Computación . 5 (3): 452–487. CiteSeerX  10.1.1.158.4318 . doi :10.1137/0205035.
• Dijkstra, Edsger W. (1976). Una disciplina de programación . Serie de Prentice-Hall en computación automática. Englewood Cliffs, Nueva Jersey 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). "Puntos menos fijos revisados". Informática Teórica . 2 (2): 155–181. doi : 10.1016/0304-3975(76)90031-1 .
• Smith, Michael B. (1978). "Dominios de poder". J. Computación. Sistema. Ciencia . 16 : 23–36. doi : 10.1016/0022-0000(78)90048-X .
• Francez, Nissim; Hoare, COCHE; Lehmann, Daniel; de Roever, Willem-Paul (diciembre de 1979). Semántica de no determinismo, concurrencia y comunicación . Apuntes de conferencias sobre 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 la computación concurrente: actas del simposio internacional, Évian, Francia, 2 al 4 de julio de 1979 . Saltador. ISBN 978-3-540-09511-8.
• Schwartz, Jerald (1979). "Semántica denotacional del paralelismo". Kahn 1979 .
• Wadge, William (1979). "Un tratamiento ampliado del estancamiento del flujo de datos". Kahn 1979 .
• Atrás, Ralph-Johan (1980). "Semántica del no determinismo ilimitado". En de Bakker, Jacó; van Leeuwen, enero (eds.). Autómatas, Lenguajes y Programación. Apuntes de conferencias sobre 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.
• Parque, David (1980). "Sobre la semántica del paralelismo justo". En Bjøorner, Dines (ed.). Especificaciones de software abstractas (PDF) . Apuntes de conferencias sobre informática. vol. 86. Berlín, Heidelberg: Springer Berlín Heidelberg. págs. 504–526. doi :10.1007/3-540-10007-5_47. ISBN 978-3-540-10007-2.
• Allison, L. (1986). Una introducción práctica a la semántica denotacional. Prensa de la Universidad de Cambridge. 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 mecanografiados . Prensa del MIT. ISBN 978-0-262-69171-0.

enlaces externos

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