Денотационная семантика модели Актера

Денотационная семантика модели Актера является предметом теории денотационной области для Актеров . Историческое развитие этой темы описано в [Hewitt 2008b].

Семантика фиксированной точки актера

Денотатационная теория семантики вычислительных систем занимается поиском математических объектов, которые представляют то, что делают системы. Коллекции таких объектов называются доменами . Актер . использует область сценариев диаграммы событий Обычно предполагают некоторые свойства области, такие как существование пределов цепей (см. cpo ) и нижнего элемента. Различные дополнительные свойства часто бывают разумными и полезными: более подробная информация содержится в статье по теории предметной области .

Домен обычно представляет собой частичный порядок , который можно понимать как порядок определенности. Например, данные сценарии диаграммы событий х и да , можно было бы позволить " x≤y "означает, что" y расширяет вычисления х ».

Математическое обозначение системы S находится путем построения все более лучших приближений из начального пустого обозначения, называемого ⊥ _S с использованием некоторой аппроксимирующей функции обозначения прогрессия _S для построения обозначения (значения) для С следующим образом:

$\mathbf {Denote} _{\mathtt {S}}\equiv \lim _{i\to \infty }\mathbf {progression} _{{\mathtt {S}}^{i}}(\bot _{\mathtt {S}})$

Можно было бы ожидать, что прогрессия _S была бы монотонной , т. е . если бы x≤y тогда прогресс _S (x) ≤ прогресс _S (y) . В более общем плане мы ожидаем, что

Если ∀ i ∈ω х _я ≤ х _{я +1} , тогда $\mathbf {progression} _{\mathtt {S}}(\lim _{i\to \infty }{\mathtt {x}}_{i})=\lim _{i\to \infty }\mathbf {progression} _{\mathtt {S}}({\mathtt {x}}_{i})$

Это последнее заявленное свойство прогрессия _S называется ω-непрерывностью.

Центральный вопрос денотационной семантики — определить, когда можно создавать денотаты (значения) в соответствии с уравнением для Обозначим _С . Фундаментальная теорема теории вычислительной области состоит в том, что если прогрессия _S ω-непрерывна, то Обозначим _S будет существовать.

Это следует из ω-непрерывности прогрессия _S, которая

прогрессия _S ( Обозначим _S ) = Обозначим _S

Приведенное выше уравнение мотивирует терминологию, которая Обозначим _S — неподвижная точка прогрессия _С. ​

Кроме того, эта неподвижная точка является наименьшей среди всех неподвижных точек прогрессия _С. ​

Композиционность в языках программирования

Важным аспектом денотационной семантики языков программирования является композиционность, при которой денотат программы строится из обозначений ее частей. Например, рассмотрим выражение « <выражение ₁ > + <выражение ₂ > ". Композиционность в этом случае заключается в том, чтобы придать смысл " <выражение ₁ > + <выражение ₂ > " с точки зрения значений <выражение ₁ > и <выражение ₂ > .

Модель актера обеспечивает современный и очень общий способ анализа композиционности программ. Скотт и Стрейчи [1971] предложили свести семантику языков программирования к семантике лямбда-исчисления и, таким образом, унаследовать денотационную семантику лямбда-исчисления . Однако оказалось, что параллельные вычисления не могут быть реализованы в лямбда-исчислении (см. Неопределённость в параллельных вычислениях ). Таким образом, возникла проблема, как обеспечить модульную денотационную семантику для параллельных языков программирования. Одним из решений этой проблемы является использование модели вычислений Actor. В модели Actor программы — это Актеры, которые отправляются Оценивать сообщения с адресом среды (поясняется ниже), чтобы программы наследовали свою денотационную семантику от денотационной семантики модели Актера (идея, опубликованная в Hewitt [2006]).

Окружающая среда

Среды содержат привязки идентификаторов. Когда среде отправляется Сообщение поиска с адресом идентификатора x возвращает последнюю (лексическую) привязку x .

В качестве примера того, как это работает, рассмотрим лямбда-выражение. <L> ниже, который реализует древовидную структуру данных при наличии параметров для leftSubTree и rightSubTree . Когда такому дереву дается сообщение параметра «getLeft» , он возвращается leftSubTree и аналогично при получении сообщения «getRight» он возвращает rightSubTree .

 λ(leftSubTree, rightSubTree)
   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree

Рассмотрим, что происходит, когда выражение формы «(<L> 1 2)» отправляется Оценить сообщение со E. средой Одна из семантик для выражений приложения, подобных этому, следующая: <L>, 1 и 2 штуки отправлено по Оценивать со средой E. сообщения Целые числа 1 и 2 немедленно ответить на Оценить сообщение с самим собой.

Однако, <L> отвечает на Оцените сообщение, создав замыкающий Актер (процесс) C , который имеет адрес (называемый телом ) для <L> и адрес (называемый средой для E. ) Актер «(<L> 1 2)» затем отправляет C сообщение [1 2] .

Когда C получает сообщение [1 2] , он создает новую среду Actor F, которая ведет себя следующим образом:

1. Когда он получает Сообщение поиска идентификатора leftSubTree , он отвечает 1
2. Когда он получает Сообщение поиска идентификатора rightSubTree , он отвечает 2
3. Когда он получает Сообщение поиска для любого другого идентификатора, оно пересылает Поисковое сообщение для E

Затем актер (процесс) C отправляет Оцените сообщение со средой F следующему актеру (процессу):

   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree

Арифметические выражения

В качестве другого примера рассмотрим Актера для выражения " <выражение ₁ > + <выражение ₂ > ", которое содержит адреса двух других субъектов (процессов) <выражение ₁ > и <выражение ₂ > . Когда составное выражение Актер (процесс) получает Оценочное сообщение с адресами для среды Actor E и клиента C , оно отправляет Оценивать сообщения для <выражение ₁ > и <выражение ₂ > со средой E и отправляет C новый Актер (процесс) C ₀ . Когда C ₀ получил обратно два значения N ₁ и N ₂ , он отправляет C значение N _{1 .} + Н ₂ . Таким образом, денотатационная семантика для исчислений процессов и модель Актера обеспечивают денотационную семантику для « <выражение ₁ > + <выражение ₂ > " с точки зрения семантики для <выражение ₁ > и <выражение ₂ > .

Другие конструкции языка программирования

Представленная выше денотационная композиционная семантика является очень общей и может использоваться для функциональных , императивных , параллельных , логических и т. д. программ (см. [Hewitt 2008a]). Например, он легко предоставляет семантику обозначений для конструкций, которые трудно формализовать с помощью других подходов, таких как задержки и фьючерсы .

Модель Клингера

В своей докторской диссертации Уилл Клингер разработал первую семантику обозначений для модели Актера.

Область вычислений актеров

Клингер [1981] объяснил область вычислений актеров следующим образом:

Расширенные диаграммы событий Актеров (см. Теорию модели Актеров ) образуют частично упорядоченный набор < Диаграммы , ≤ >, из которого можно построить степенную область P [ Диаграммы ] (см. раздел « Обозначения» ниже). Дополненные диаграммы представляют собой частичные истории вычислений, представляющие «моментальные снимки» [относительно некоторой системы отсчета] вычислений на пути к завершению. Для x , y ∈ В диаграммах x x≤y означает, что — это этап, который может пройти вычисление на пути к y . Готовые элементы Диаграммы представляют вычисления, которые завершились, и непрерывные вычисления, которые стали бесконечными. Завершенные элементы можно абстрактно охарактеризовать как максимальные элементы Диаграммы [см. William Wadge 1979]. Конкретно, завершенными элементами являются те элементы, у которых нет ожидающих событий. Интуитивно, Диаграммы не являются ω-полными , поскольку существуют возрастающие последовательности конечных частичных вычислений.

$x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...$

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

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

Обозначения

В своей докторской диссертации Уилл Клингер объяснил, как домены власти получаются из неполных доменов следующим образом:

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

Для домена диаграммы событий субъекта Диаграммы , элемент P [ Диаграммы ] представляет список возможных начальных историй вычислений. Поскольку для элементов x и y из Диаграммы , x≤y означает, что x является начальным сегментом начальной истории y , требование, чтобы элементы P [ Диаграммы ] быть закрытыми вниз имеет четкую основу на интуиции.

...

Обычно частичный порядок, из которого строится степенная область, должен быть ω-полным . Для этого есть две причины. Первая причина заключается в том, что большинство степенных доменов являются просто обобщениями доменов, которые использовались в качестве семантических доменов для обычных последовательных программ, и все такие домены являются полными из-за необходимости вычисления фиксированных точек в последовательном случае. Вторая причина заключается в том, что ω-полнота позволяет решать уравнения рекурсивной области, включающие степенную область, такие как

$R\approx S\rightarrow P[S+(S\times R)]$

которое определяет область возобновлений [Гордон Плоткин 1976]. Однако домены мощности могут быть определены для любого домена. Более того, степенная область домена по сути является степенной областью его ω-пополнения, поэтому рекурсивные уравнения, включающие степенную область неполной области, все еще могут быть решены, предоставляют области, к которым применяются обычные конструкторы (+, ×, → и *) являются ω-полными. Бывает, что определение семантики Актера, как в Clinger [1981], не требует решения каких-либо рекурсивных уравнений, включающих степенную область.

Короче говоря, нет никаких технических препятствий для создания властных доменов из неполных доменов. Но почему человек должен этого хотеть?

В поведенческой семантике , разработанной Ирен Грейф , смысл программы — это спецификация вычислений, которые может выполнять программа. Вычисления формально представлены диаграммами событий актеров. Грейф определил диаграммы событий посредством причинных аксиом, управляющих поведением отдельных акторов [Greif 1975].

Генри Бейкер представил недетерминированный интерпретатор, генерирующий мгновенные графики, которые затем отображаются на диаграммах событий. Он предположил, что соответствующий детерминированный интерпретатор, работающий с наборами мгновенных расписаний, может быть определен с использованием семантики степенной области [Baker 1978].

Семантика, представленная в [Clinger 1981], представляет собой версию поведенческой семантики. Программа обозначает набор диаграмм событий Актера. Набор определяется экстенсионально с использованием семантики степенной области, а не интенционально с использованием причинных аксиом. Поведение отдельных актеров определяется функционально. Однако показано, что результирующий набор диаграмм событий Актеров состоит именно из тех диаграмм, которые удовлетворяют причинным аксиомам, выражающим функциональное поведение Актеров. Таким образом, поведенческая семантика Грейфа совместима с семантикой денотационной области власти.

Мгновенные расписания Бейкера ввели понятие ожидающих событий , которые представляют собой сообщения на пути к своим целям. Каждое ожидающее событие должно рано или поздно стать фактическим (реализованным) событием прибытия, и это требование называется конечной задержкой . Дополнение диаграмм событий субъектов наборами ожидающих событий помогает выразить свойство конечной задержки, которое характерно для истинного параллелизма [Schwartz 1979].

Последовательные вычисления образуют ω-полную подобласть области вычислений Actor.

В своей диссертации 1981 года Клингер показал, как последовательные вычисления образуют подобласть параллельных вычислений:

Вместо того, чтобы начинать с семантики последовательных программ, а затем пытаться расширить ее для обеспечения параллелизма, семантика актеров рассматривает параллелизм как основной и получает семантику последовательных программ как особый случай.

...

Тот факт, что существуют возрастающие последовательности без каких-либо верхних границ, может показаться странным тем, кто привык думать о семантике последовательных программ. Возможно, будет полезно указать, что все возрастающие последовательности, создаваемые последовательными программами, имеют наименьшие верхние границы. Действительно, частичные вычисления, которые могут быть произведены последовательными вычислениями, образуют ω-полную подобласть области вычислений Актера. Диаграммы . Далее следует неформальное доказательство.

С точки зрения Актера, последовательные вычисления представляют собой особый случай параллельных вычислений, отличающийся диаграммами событий. Диаграмма событий последовательных вычислений имеет начальное событие, и ни одно событие не активирует более одного события. Другими словами, порядок активации последовательных вычислений является линейным; диаграмма событий по существу представляет собой традиционную последовательность выполнения. Это означает, что конечные элементы Диаграммы

$x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...$

соответствующие конечным начальным сегментам последовательной последовательности выполнения, все они имеют ровно одно ожидающее событие, за исключением самого большого завершенного элемента, если вычисление завершается. Одно свойство домена расширенных диаграмм событий < Диаграммы , ≤ > заключается в том, что если x≤y и x≠y , то некоторое ожидающее событие x реализуется в y . Поскольку в этом случае каждое xi _{имеет не более одного ожидающего события ,} каждое ожидающее событие в последовательности становится реализованным. Отсюда последовательность

$x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...$

имеет наименьшую верхнюю границу в Диаграммы в соответствии с интуицией.

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

Модель временных диаграмм

Хьюитт [2006b] опубликовал новую денотационную семантику для актеров, основанную на временных диаграммах. Модель временных диаграмм отличается от модели Клингера. [1981] построили ω-полную степенную область на основе неполной диаграммная область, которая не включала время. Преимущество домена Модель временных диаграмм заключается в том, что она физически мотивирована, и в результате вычисления обладают желаемым свойством ω-полноты (следовательно, неограниченной недетерминизм), который обеспечивает гарантию обслуживания.

Область вычислений синхронизированных актеров

Денотационная семантика временных диаграмм создает ω-полную вычислительную систему. домен для вычислений Актера. В домене для каждого события в вычислении Актера существует время доставки, которое представляет собой время, в которое сообщение доставляется так, что каждый момент доставки удовлетворяет следующим условиям:

1. Время доставки — это положительное рациональное число, которое не совпадает со временем доставки любого другого сообщения.
2. Время доставки более чем на фиксированную величину больше времени его активирующего события. Позже выяснится, что значение δ не имеет значения. Фактически, значению δ можно даже позволить линейно уменьшаться со временем, чтобы соответствовать закону Мура.

Временные диаграммы событий Актера образуют частично упорядоченный набор < TimedDiagrams , ≤>. Диаграммы представляют собой частичные истории вычислений, представляющие «моментальные снимки» (относительные к некоторой системе отсчета) вычисления на пути к завершению. Для d1, d2ε TimedDiagrams , d1≤d2 означает, что d1 — это этап, на котором могут пройти вычисления. на пути к d2 Завершенные элементы TimedDiagrams представляют собой вычисления, которые завершенные и незавершающиеся вычисления, ставшие бесконечными. Завершено элементы можно абстрактно охарактеризовать как максимальные элементы TimedDiagrams . Конкретно, завершенными элементами являются элементы, не имеющие ожидающих событий.

Теорема: TimedDiagrams представляет собой ω-полную область вычислений Актеров, т.е.

1. Если D⊆ TimedDiagrams направлена, существует наименьшая верхняя граница ⊔D; более того, ⊔D подчиняется всем законам теории модели актера .
2. Конечные элементы TimedDiagrams счетны, где элемент xε TimedDiagrams конечен (изолирован) тогда и только тогда, когда D⊆ TimedDiagrams направлен и x≤VD, существует dεD с x≤d. Другими словами, x является конечным, если необходимо пройти через x, чтобы достичь или превысить x посредством предельного процесса.
3. Каждый элемент TimedDiagrams является наименьшей верхней границей счетной возрастающей последовательности конечных элементов.

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

• Определение: Область <Power[ TimedDiagrams] , ⊆> — это набор возможных начальных историй M вычислений, таких что
  1. M замкнуто вниз, т.е. если dεM, то ∀d'εTimedDiagrams d'≤d ⇒ d'εM
  2. M замкнуто относительно верхних границ направленных множеств, т.е. если D⊆M направлено, то VDεM
• Примечание. Хотя Power[ TimedDiagrams ] упорядочен по ⊆, ограничения не задаются U . Т.е.,

  (∀iεω M _i ≤M _i+1 ) ⇒ ​​U _iεω M _i ⊆ ⊔ _iεω M _i

  Например, если ∀id _i ε TimedDiagrams и d _i ≤d _i+1 и M _i = {d _k | k ≤i} тогда

  {{{1}}}

• Теорема: Power [ TimedDiagrams ] является ω-полной областью.

Теорема о параллельном представлении

Вычисление Актера может развиваться разными способами. Пусть d — диаграмма со следующим запланированным событием e и Икс ≡ {е' | e ─≈→ _{1-сообщение} e'} (см. теорию модели актора ), Flow(d) определяется как набор всех временных диаграмм с d и расширениями d с помощью X такой, что

1. Прибытие всех событий X было запланировано, где
2. события X запланированы во всех возможных порядках среди запланированных будущих событий d
3. при условии, что каждое событие в X запланировано как минимум через δ после e, а каждое событие в X запланировано как минимум один раз в каждом интервале δ после этого.

(Напомним, что δ — минимальное время доставки сообщения.)

Flow(d) ≡ {d}, если d полно.

Пусть S — акторная система, Progression _S — отображение

Мощность[ TimedDiagrams ]→Мощность[ TimedDiagrams ]

Прогрессия _S (M) ≡ U _dεM Flow(d)

Теорема: Прогрессия _S ω-непрерывна.

Т.е. если ∀i M _i ⊆M _i+1 , то Прогрессия _S (⊔ _iεω M _i ) = ⊔ _iεω Прогрессия _S (M _i )

Кроме того, наименее неподвижная точка прогрессии _S определяется теоремой о параллельном представлении следующим образом:

⊔ _iεω Прогрессия _S ^я (⊥ _S )

где ⊥ _S — начальная конфигурация S.

Обозначение Denote _S системы актеров S представляет собой набор всех вычислений S.

Определите временную абстракцию временной диаграммы как диаграмму с временными аннотациями. удаленный.

Теорема о представлении: Обозначение Denote _{S актерской системы S - это временная абстракция}

⊔ _iεω Прогрессия _S ^я (⊥ _S )

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

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

Ссылки

• Дана Скотт и Кристофер Стрейчи. К математической семантике компьютерных языков. Техническая монография Оксфордской исследовательской группы по программированию. ПРГ-6. 1971.
• Ирен Грейф. Семантика общения параллельных профессий Докторская диссертация MIT EECS. Август 1975 года.
• Джозеф Э. Стой , Денотационная семантика: подход Скотта-Стрейчи к семантике языка программирования . MIT Press , Кембридж, Массачусетс, 1977. (Классический, хотя и устаревший учебник.)
• Гордон Плоткин. Конструкция энергетической области . SIAM Journal on Computing, сентябрь 1976 г.
• Эдсгер Дейкстра . Дисциплина программирования Прентис Холл . 1976.
• Кшиштоф Р. Апт , Дж. В. де Баккер. Упражнения по денотационной семантике MFCS 1976: 1-11.
• Дж. В. де Баккер. Возвращение к теории наименьших фиксированных точек . Вычислить. наук. 2 (2): 155–181 (1976)
• Карл Хьюитт и Генри Бейкер Актеры и непрерывные функционалы. Материалы рабочей конференции ИФИП по формальному описанию концепций программирования. 1–5 августа 1977 г.
• Генри Бейкер . Акторные системы для вычислений в реальном времени. Докторская диссертация MIT EECS. Январь 1978 года.
• Майкл Смит. Энергетические домены Журнал компьютерных и системных наук . 1978.
• АВТОМОБИЛЬ Хоар . Взаимодействие последовательных процессов CACM . Август 1978 года.
• Джордж Милн и Робин Милнер . Параллельные процессы и их синтаксис JACM . Апрель 1979 года.
• Ниссим Франсез, КАР Хоар , Дэниел Леманн и Виллем-Поль де Ровер. Семантика недетерминизма, параллелизма и коммуникации . Журнал компьютерных и системных наук. Декабрь 1979 года.
• Нэнси Линч и Майкл Дж. Фишер . Об описании поведения распределенных систем в семантике параллельных вычислений. Спрингер-Верлаг . 1979.
• Джеральд Шварц Денотационная семантика параллелизма в семантике параллельных вычислений. Спрингер-Верлаг. 1979.
• Уильям Уэдж. Расширенная обработка тупиковой ситуации потока данных . Семантика параллельных вычислений. Спрингер-Верлаг. 1979.
• Ральф-Йохан Бэк. Семантика неограниченного недетерминизма ICALP 1980.
• Дэвид Парк. О семантике справедливого параллелизма. Материалы Зимней школы по формальным спецификациям программного обеспечения. Спрингер-Верлаг. 1980.
• Уилл Клингер, Основы семантики актеров . Докторская диссертация по математике в Массачусетском технологическом институте, июнь 1981 г. (Цитируется с разрешения автора).
• Карл Хьюитт Что такое приверженность? Физические, организационные и социальные Пабло Норьега и др. редакторы. LNAI 4386. Шпрингер-Верлаг. 2007.