Области степеней в денотационной семантике и теории доменов.
Power domains
Power domains в семантике и теории доменов: недетерминированные вычисления, множества значений функций, параллельные системы. Сложные понятия для корректности.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В денотационной семантике и теории доменов, силовые домены – это домены недетерминированных и параллельных вычислений. Идея силовых доменов для функций заключается в том, что недетерминированную функцию можно описать как детерминированную функцию, принимающую на вход множество значений, содержащее все возможные результаты, которые недетерминированная функция может выдать для данного аргумента. Для параллельных систем идея состоит в том, чтобы выразить множество всех возможных траекторий вычислений. В общих чертах, силовой домен – это домен, элементы которого являются определенными подмножествами исходного домена. Однако, наивное применение этого подхода часто приводит к доменам, не обладающим необходимыми свойствами, что заставляет разрабатывать все более сложные определения силовых доменов. Существует три основных варианта: силовые домены Плоткина, верхний и нижний силовые домены. Один из способов понять эти концепции – рассматривать их как свободные модели теорий недетерминизма. На протяжении большей части этой статьи мы используем термины "домен" и "непрерывная функция" в достаточно широком смысле, подразумевая под ними, соответственно, некоторую упорядоченную структуру и функцию, сохраняющую пределы. Эта гибкость оправдана; например, в некоторых параллельных системах естественно требовать, чтобы каждое отправленное сообщение в конечном итоге было доставлено. Однако, предел цепочки приближений, в которой сообщение не было доставлено, будет представлять собой завершенное вычисление, в котором сообщение так и не было доставлено! Современным обзором этой темы является глава Абрамского и Юнга [1994]. Более ранние работы включают работы Плоткина [1983, глава 8] и Смита [1978].
In denotational semantics and domain theory, power domains are domains of nondeterministic and concurrent computations. The idea of power domains for functions is that a nondeterministic function may be described as a deterministic set valued function, where the set contains all values the nondeterministic function can take for a given argument. For concurrent systems, the idea is to express the set of all possible computations. Roughly speaking, a power domain is a domain whose elements are certain subsets of a domain. Taking this approach naively, though, often gives rise to domains that don't quite have the desired properties, and so one is led to increasingly complicated notions of the power domain. There are three common variants: the Plotkin, upper, and lower power domains. One way to understand these concepts is as free models of theories of nondeterminism. For most of this article we use the terms "domain" and "continuous function" quite loosely, meaning respectively some kind of ordered structure and some kind of limit preserving function. This flexibility is genuine; for example, in some concurrent systems it is natural to impose the condition that every message sent must eventually be delivered. However, the limit of a chain of approximations in which a message was not delivered, would be a completed computation in which the message was never delivered! A modern reference to this subject is the chapter by Abramsky and Jung [1994]. Older references include those of Plotkin [1983, Chapter 8] and Smyth [1978].
Домены власти как свободные модели теорий недетерминизма
Теоретики доменов стали понимать домены власти абстрактно как свободные модели теорий недетерминизма. Подобно тому как конечное построение множества степеней является свободной полурешеткой, построения доменов власти следует понимать абстрактно как свободные модели теорий недетерминизма. Изменяя теории недетерминизма, получаются различные домены власти. Абстрактная характеристика доменов власти часто является наиболее удобным способом работы с ними, поскольку явные описания слишком сложны. (Исключением является домен власти Хоара, который имеет достаточно простое описание.)
Domain theorists have come to understand power domains abstractly as free models for theories of non determinism. Just as the finite powerset construction is the free semilattice, the powerdomain constructions should be understood abstractly as free models of theories of non determinism. By changing the theories of non determinism, different power domains arise. The abstract characterisation of powerdomains is often the easiest way to work with them, because explicit descriptions are so intricate. (One exception is the Hoare powerdomain, which has a rather straightforward description.)
Модели теорий движения
Модель теории мощности Плоткина является непрерывной полурешеткой: это полурешетка, носителем которой является домен и для которой операция является непрерывной. Следует отметить, что оператор не обязательно должен быть операцией взятия точной нижней грани или точной верхней грани для порядка в домене. Гомоморфизм непрерывных полурешеток — это непрерывная функция между их носителями, сохраняющая операцию полурешетки. Модели нижней теории мощности называются инфляционными полурешетками; существует дополнительное требование, чтобы оператор в некоторой степени вел себя как операция взятия точной верхней грани для порядка. Для верхней теории мощности модели называются дефляционными полурешетками; здесь оператор в некоторой степени ведет себя как операция взятия точной нижней грани.
A model of the Plotkin powertheory is a continuous semilattice: it is a semilattice whose carrier is a domain and for which the operation is continuous. Note that the operator need not be a meet or join for the order of the domain. A homomorphism of continuous semilattices is a continuous function between their carriers that respects the lattice operator. Models of the lower powertheory are called inflationary semilattices; there is an additional requirement that the operator behave a little like a join for the order. For the upper powertheory, models are called deflationary semilattices; here, the operator behaves a little like a meet.
Власть домены как свободные модели
Пусть D — домен. Поле мощностей Плоткина над D является свободной моделью теории мощностей Плоткина над D. Оно определяется как (если существует) модель P(D) теории мощностей Плоткина (то есть непрерывная полурешетка), снабженная непрерывным отображением D → P(D), таким что для любой другой непрерывной полурешетки L над D существует единственный непрерывный гомоморфизм полурешеток P(D) → L, делающий очевидную диаграмму коммутативной. Другие поля мощностей определяются абстрактно аналогичным образом.
Let D be a domain. The Plotkin powerdomain on D is the free model of the Plotkin powertheory over D. It is defined to be (when it exists) a model P(D) of the Plotkin powertheory (i. e. a continuous semilattice) equipped with a continuous function D → P(D) such that for any other continuous semilattice L over D, there is a unique continuous semilattice homomorphism P(D) → L making the evident diagram commute. Other powerdomains are defined abstractly in a similar manner.
Силовая область Клингера
Клингер [1981] построил домен мощностей для модели Actor, основываясь на базовом домене диаграмм событий Actor, который не является полным. См. модель Клингера.
Clinger [1981] constructed a power domain for the Actor model building on the base domain of Actor event diagrams, which is incomplete. See Clinger's model.
Диаграммы с временем
Хьюитт [2006] построил силовую область для модели акторов (которая технически проще и легче для понимания, чем модель Клингера), основываясь на базовой области полных диаграмм событий акторов, определяемых по времени. Идея заключается в присвоении времени прибытия каждому сообщению, полученному актором. См. Модель диаграмм, определяемых по времени.
Hewitt [2006] constructed a power domain for the Actor model (which is technically simpler and easier to understand than Clinger's model) building on a base domain of timed Actor event diagrams, which is complete. The idea is to attach an arrival time for each message received by an Actor. See Timed Diagrams Model.
Связи с топологией и пространством Вьеториса
Домены могут рассматриваться как топологические пространства, и в этом контексте построения домена степеней могут быть соотнесены с построением пространства подмножеств, предложенным Леопольдом Виеторисом. См., например, [Smyth 1983].
Domains can be understood as topological spaces, and, in this setting, the power domain constructions can be connected with the space of subsets construction introduced by Leopold Vietoris. See, for instance, [Smyth 1983].