Силовые домены

В денотационной семантике и теории доменов степенные домены — это области недетерминированных и параллельных вычислений.

Идея степенных областей для функций заключается в том, что недетерминированная функция может быть описана как детерминированная многозначная функция, где набор содержит все значения, которые недетерминированная функция может принимать для данного аргумента. Идея параллельных систем состоит в том, чтобы выразить набор всех возможных вычислений.

Грубо говоря, энергетический домен — это домен, элементы которого являются определенными подмножествами домена. Однако наивный подход к этому подходу часто приводит к появлению областей, которые не совсем обладают желаемыми свойствами, и поэтому мы приходим ко все более сложным понятиям области власти. Существует три распространенных варианта: домены Плоткина, верхняя и нижняя степень. Один из способов понять эти концепции — это свободные модели теорий недетерминизма.

В большей части этой статьи мы довольно широко используем термины «область применения» и «непрерывная функция», имея в виду соответственно некую упорядоченную структуру и некую функцию, сохраняющую предел. Эта гибкость подлинна; например, в некоторых параллельных системах естественно наложить условие, согласно которому каждое отправленное сообщение должно в конечном итоге быть доставлено. Однако пределом цепочки приближений, в которой сообщение не было доставлено, было бы завершенное вычисление, в котором сообщение так и не было доставлено!

Современной ссылкой на эту тему является глава Абрамского и Юнга [1994]. Более старые ссылки включают работы Плоткина [1983, глава 8] и Смита [1978].

Властные области как свободные модели теорий недетерминизма

Теоретики предметной области пришли к абстрактному пониманию доменов власти как свободных моделей теорий недетерминизма. Подобно тому, как конструкция с конечной степенью является свободной полурешеткой , конструкции степенной области следует понимать абстрактно как свободные модели теорий недетерминизма. Изменяя теории недетерминизма, возникают разные сферы власти.

Абстрактная характеристика доменов власти часто является самым простым способом работы с ними, поскольку явные описания очень сложны. (Единственным исключением является домен власти Хоара, который имеет довольно простое описание.)

Теории недетерминизма

Напомним три теории недетерминизма. Они являются вариациями теории полурешеток . Теории не являются алгебраическими теориями в общепринятом смысле, поскольку некоторые из них включают порядок базовой области.

Все теории имеют один вид X и одну бинарную операцию ∪. Идея состоит в том, что операция $\cup: X \times X \to X$ принимает две комбинации и возвращает недетерминированный выбор из них.

Теория власти Плоткина (по Гордону Плоткину ) имеет следующие аксиомы:

Идемпотентность: x ∪ x = x
Коммутативность: x ∪ y = y ∪ x
Ассоциативность: ( Икс ∪ y ) ∪ z знак равно Икс ∪ ( y ∪ z )

Нижняя теория власти (или Хоара , в честь Тони Хоара ) состоит из теории власти Плоткина, дополненной неравенством

Икс ≤ Икс ∪ у .

Верхняя теория власти (или Смита , по имени М.Б. Смита) состоит из теории власти Плоткина, дополненной неравенством

Икс ∪ у ≤ Икс .

Модели теорий власти

Моделью теории власти Плоткина является непрерывная полурешетка : это полурешетка, носителем которой является область и для которой операция непрерывна. Обратите внимание, что оператор не обязательно должен быть участником встречи или объединения для заказа домена. Гомоморфизм непрерывных полурешеток — это непрерывная функция между их носителями, уважающая решеточный оператор.

Модели теории пониженной степени называются инфляционными полурешетками; существует дополнительное требование, чтобы оператор вел себя как соединение заказа. В теории верхней степени модели называются дефляционными полурешетками; здесь оператор ведет себя немного как при встрече. ^{[ тон ]}

Power домены как бесплатные модели

Пусть D — область. Область власти Плоткина на D является свободной моделью теории власти Плоткина над D . Она определяется как (если она существует) модель P ( D ) степенной теории Плоткина (т. е. непрерывная полурешетка), снабженная непрерывной функцией D → P ( D ), такая, что для любой другой непрерывной полурешетки L над D существует единственный непрерывный гомоморфизм полурешетки P ( D ) → L, делающий очевидную диаграмму коммутирующей .

Другие домены власти определяются абстрактно аналогичным образом.

Явное описание доменов власти

Пусть D — область. Область более низкой мощности может быть определена как

п [ D ] знак равно {замыкание [ А ] | Ø ∈ A ⊆ D } где

замыкание [ А ] знак равно { d ∈ D | ∃ X ⊆ D , X направленный , d =

\vee

X и ≤ ∀ x ∈ X ∃ a ∈ A x a } .

Другими словами, P [ D ] — это совокупность замкнутых вниз подмножеств D которые также замкнуты относительно существующих наименьших верхних границ направленных множеств в D. , Обратите внимание, что хотя порядок на P [ D ] задается отношением подмножества, минимальные верхние границы обычно не совпадают с объединениями.

Важно проверить, какие свойства областей сохраняются конструкциями степенных областей. Например, степенная область Хоара ω-полной области снова является ω-полной.

Домены мощности для параллелизма и актеров

Домен власти Клингера

Клингер [1981] построил энергетическую область для модели Актера на основе базовой области диаграмм событий Актера , которая является неполной. См. модель Клингера .

Временные диаграммы мощности домена

Хьюитт [2006] построил энергетическую область для модели Актера (которая технически проще и легче для понимания, чем модель Клингера), основываясь на базовой области временных диаграмм событий Актера, которая является полной. Идея состоит в том, чтобы прикрепить время прибытия для каждого сообщения, полученного Актером. См. Модель временных диаграмм .

Связи с топологией и пространством Виеториса.

Домены можно понимать как топологические пространства , и в этом случае конструкции степенных областей могут быть связаны с подмножеств пространством построения , введенным Леопольдом Виеторисом . См., например, [Smyth 1983].

Ссылки

Ирен Грейф. Семантика взаимодействия параллельных процессов Докторская диссертация MIT EECS. Август 1975 года.
Джозеф Э. Стой , Денотационная семантика: подход Скотта-Стрейчи к семантике языка программирования . MIT Press, Кембридж, Массачусетс, 1977. (Классический, хотя и устаревший учебник.)
Гордон Плоткин. Конструкция энергетической области . SIAM Journal on Computing, сентябрь 1976 г.
Карл Хьюитт и Генри Бейкер Актеры и непрерывные функционалы. Материалы рабочей конференции ИФИП по формальному описанию концепций программирования. 1–5 августа 1977 г.
Генри Бейкер . Акторные системы для вычислений в реальном времени. Докторская диссертация MIT EECS. Январь 1978 года.
Майкл Смит. Энергетические домены Журнал компьютерных и системных наук . 1978.
Джордж Милн и Робин Милнер . Параллельные процессы и их синтаксис JACM . Апрель 1979 года.
АВТОМОБИЛЬ Хоар . Взаимодействие последовательных процессов CACM . Август 1978 года.
Ниссим Франсез , К.АР. Хоар, Дэниел Леманн и Виллем де Ровер. Семантика недетерминизма, параллелизма и коммуникации . Журнал компьютерных и системных наук. Декабрь 1979 года.
Джеральд Шварц Денотационная семантика параллелизма в семантике параллельных вычислений. Спрингер-Верлаг. 1979.
Уильям Уэдж. Расширенная обработка тупиковой ситуации потока данных . Семантика параллельных вычислений. Спрингер-Верлаг. 1979.
Ральф-Йохан Назад . Семантика неограниченного недетерминизма ICALP 1980.
Дэвид Парк. О семантике справедливого параллелизма. Материалы Зимней школы по формальным спецификациям программного обеспечения. Спрингер-Верларг. 1980.
Уилл Клингер, Основы семантики актеров . Докторская диссертация по математике в Массачусетском технологическом институте, июнь 1981 г.
Гордон Плоткин. Домены (примечания Пизы) . 1983. Доступно в [1] .
М.Б. Смит, Степенные области и преобразователи предикатов: топологический взгляд , LNCS 154, Springer, 1983.
С. Абрамский, А. Юнг: Теория предметной области . В С. Абрамский, Д.М. Габбай, TSE Майбаум, редакторы, Справочник по логике в информатике, том. III. Издательство Оксфордского университета, 1994. ( ISBN 0-19-853762-X ) (скачать PDF PS.GZ )