En semántica denotacional y teoría de dominios , los dominios de poder son dominios de cálculos concurrentes y no deterministas .
La idea de dominios de poder para funciones es que una función no determinista puede describirse como una función determinista valorada por un conjunto , donde el conjunto contiene todos los valores que la función no determinista puede tomar para un argumento dado. Para sistemas concurrentes, la idea es expresar el conjunto de todos los cálculos posibles.
En términos generales, un dominio de poder es un dominio cuyos elementos son ciertos subconjuntos de un dominio. Sin embargo, tomar este enfoque de manera ingenua, a menudo da lugar a dominios que no tienen las propiedades deseadas, por lo que uno se ve conducido a nociones cada vez más complicadas de dominio de poder. Hay tres variantes comunes: los dominios de poder de Plotkin, superior e inferior. Una forma de entender estos conceptos es como modelos libres de teorías del no determinismo.
En la mayor parte de este artículo usamos los términos "dominio" y "función continua" de manera bastante vaga, lo que significa, respectivamente, algún tipo de estructura ordenada y algún tipo de función de preservación de límites. Esta flexibilidad es genuina; por ejemplo, en algunos sistemas concurrentes es natural imponer la condición de que todos los mensajes enviados deben entregarse eventualmente. Sin embargo, el límite de una cadena de aproximaciones en las que no se entregó un mensaje, sería un cálculo completo en el que el mensaje nunca se entregó.
Una referencia moderna a este tema es el capítulo de Abramsky y Jung [1994]. Las referencias más antiguas incluyen las de Plotkin [1983, Capítulo 8] y Smyth [1978].
Dominios de poder como modelos libres de teorías del no determinismo
Los teóricos del dominio han llegado a entender los dominios de poder de manera abstracta como modelos libres para las teorías del no determinismo. Así como la construcción de conjuntos de poderes finitos es la semirrejilla libre , las construcciones de dominio de poder deben entenderse abstractamente como modelos libres de teorías del no determinismo. Al cambiar las teorías del no determinismo, surgen diferentes dominios de poder.
La caracterización abstracta de los dominios de poder es a menudo la forma más fácil de trabajar con ellos, porque las descripciones explícitas son muy complejas. (Una excepción es el dominio de potencia de Hoare, que tiene una descripción bastante sencilla).
Teorías del no determinismo
Recordamos tres teorías del no determinismo. Son variaciones de la teoría de las semirretículas . Las teorías no son teorías algebraicas en el sentido convencional, porque algunas involucran el orden del dominio subyacente.
Todas las teorías tienen un tipo X y una operación binaria ∪. La idea es que la operación ∪: X × X → X toma dos combinaciones y devuelve la elección no determinista de ellas.
La teoría del poder de Plotkin (después de Gordon Plotkin ) tiene los siguientes axiomas:
- Idempotencia: x ∪ x = x
- Conmutatividad: x ∪ y = y ∪ x
- Asociatividad: ( x ∪ y ) ∪ z = x ∪ ( y ∪ z )
La teoría del poder inferior (o Hoare , después de Tony Hoare ) consiste en la teoría del poder de Plotkin aumentada con la desigualdad
- x ≤ x ∪ y .
La teoría de potencia superior (o Smyth , después de MB Smyth) consiste en la teoría de potencia de Plotkin aumentada con la desigualdad
- x ∪ y ≤ x .
Modelos de las teorías de potencia
Un modelo de la teoría del poder de Plotkin es una semirrejilla continua : es una semirrejilla cuyo portador es un dominio y para el cual la operación es continua. Tenga en cuenta que el operador no necesita ser un encuentro o unirse para el pedido del dominio. Un homomorfismo de semirretículos continuos es una función continua entre sus portadores que respeta al operador del retículo.
Los modelos de la teoría de la potencia inferior se denominan semirretículas inflacionarias; Existe un requisito adicional de que el operador se comporte un poco como una combinación para el pedido. Para la teoría del poder superior, los modelos se denominan semirretículos deflacionarios; aquí, el operador se comporta un poco como un encuentro.
Dominios de poder como modelos gratuitos
Sea D un dominio. El PowerDomain Plotkin en D es el modelo de libre de la powertheory Plotkin sobre D . Se define como (cuando existe) un modelo P ( D ) de la teoría de potencia de Plotkin (es decir, una semirrejilla continua) equipada con una función continua D → P ( D ) tal que para cualquier otra semirrejilla continua L sobre D , hay un homomorfismo de semirretículo continuo único P ( D ) → L que hace que el diagrama evidente se conmute .
Otros dominios de poder se definen de manera abstracta de manera similar.
Descripciones explícitas de dominios de poder
Sea D un dominio. El dominio de menor potencia se puede definir por
- P [ D ] = {cierre [ A ] | Ø ∈ A ⊆ D } donde
- cierre [ A ] = { d ∈ D | ∃ X ⊆ D , X dirigido , d = X , y ∀ x ∈ X ∃ a ∈ A x ≤ a }.
En otras palabras, P [ D ] es la colección de subconjuntos hacia abajo-cerradas de D , que también son cerrados bajo límites menos superiores existentes de conjuntos dirigidos en D . Tenga en cuenta que mientras que el orden en P [ D ] viene dado por la relación de subconjunto, los límites superiores mínimos no coinciden en general con las uniones.
Es importante comprobar qué propiedades de los dominios se conservan mediante las construcciones de los dominios de potencia. Por ejemplo, el dominio de potencia Hoare de un dominio ω-completo es nuevamente ω-completo.
Dominios de poder para concurrencia y actores
Dominio de poder de Clinger
Clinger [1981] construyó un dominio de poder para el modelo de Actor basándose en el dominio base de los diagramas de eventos de Actor , que está incompleto. Vea el modelo de Clinger .
Dominio de poder de diagramas temporizados
Hewitt [2006] construyó un dominio de poder para el modelo Actor (que es técnicamente más simple y más fácil de entender que el modelo de Clinger) basándose en un dominio base de diagramas de eventos de Actor cronometrados, que es completo. La idea es adjuntar una hora de llegada para cada mensaje recibido por un actor. Ver modelo de diagramas cronometrados .
Conexiones con topología y el espacio de Vietoris
Los dominios pueden entenderse como espacios topológicos y, en este escenario, las construcciones de los dominios de poder se pueden conectar con el espacio de construcción de subconjuntos introducido por Leopold Vietoris . Véase, por ejemplo, [Smyth 1983].
Referencias
- Irene Greif. Semántica de la comunicación de procesos paralelos Tesis doctoral EECS del MIT. Agosto de 1975.
- Joseph E. Stoy , Semántica denotacional: El enfoque de Scott-Strachey para la semántica del lenguaje de programación . MIT Press, Cambridge, Massachusetts, 1977. (Un libro de texto clásico aunque anticuado).
- Gordon Plotkin. Una construcción de dominio de potencia SIAM Journal on Computing, septiembre de 1976.
- Carl Hewitt y Henry Baker Actores y Actas de Funcionalidad Continua de la Conferencia de Trabajo de IFIP sobre Descripción Formal de Conceptos de Programación. 1-5 de agosto de 1977.
- Henry Baker . Actor Sistemas de Computación en Tiempo Real MIT EECS Tesis Doctoral. Enero de 1978.
- Michael Smyth. Power domains Journal of Computer and System Sciences . 1978.
- George Milne y Robin Milner . Procesos concurrentes y su sintaxis JACM . Abril de 1979.
- COCHE Hoare . Comunicación de procesos secuenciales CACM . Agosto de 1978.
- Nissim Francez , CAR Hoare, Daniel Lehmann y Willem de Roever. Semántica del no determinismo, concurrencia y comunicación Journal of Computer and System Sciences. Diciembre de 1979.
- Jerald Schwartz Semántica denotacional del paralelismo en Semantics of Concurrent Computation. Springer-Verlag. 1979.
- William Wadge. Un tratamiento extensivo de la semántica del interbloqueo del flujo de datos de la computación concurrente. Springer-Verlag. 1979.
- Ralph-Johan Back . Semántica del no determinismo ilimitado ICALP 1980.
- David Park. Sobre la semántica del paralelismo justo Actas de la Escuela de Invierno sobre Especificación de Software Formal. Springer-Verlarg. 1980.
- Will Clinger, Fundamentos de la semántica del actor . Tesis de Doctorado en Matemáticas del MIT, junio de 1981.
- Gordon Plotkin. Dominios (notas de Pisa) . 1983. Disponible en [1] .
- MB Smyth, Dominios de poder y transformadores de predicado: una vista topológica , LNCS 154, Springer, 1983.
- S. Abramsky, A. Jung: teoría del dominio . En S. Abramsky, DM Gabbay, TSE Maibaum, editores, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994. ( ISBN 0-19-853762-X ) (descargar PDF PS.GZ )