Domeny władzy

W semantyce denotacyjnej i teorii dziedzin dziedziny mocy są dziedzinami obliczeń niedeterministycznych i współbieżnych .

Idea dziedzin mocy dla funkcji polega na tym, że funkcję niedeterministyczną można opisać jako deterministyczną funkcję o wartościach zbiorczych , gdzie zbiór zawiera wszystkie wartości, jakie funkcja niedeterministyczna może przyjąć dla danego argumentu. W przypadku systemów współbieżnych chodzi o wyrażenie zbioru wszystkich możliwych obliczeń.

Z grubsza mówiąc, domena mocy to domena, której elementami są pewne podzbiory domeny. Jednak naiwne podejście często prowadzi do powstania domen, które nie do końca mają pożądane właściwości, co prowadzi do coraz bardziej skomplikowanych pojęć dziedziny władzy. Istnieją trzy popularne warianty: Plotkin, górna i dolna domena władzy. Jednym ze sposobów rozumienia tych pojęć są swobodne modele teorii niedeterminizmu.

Przez większą część tego artykułu używamy terminów „dziedzina” i „funkcja ciągła” dość luźno, oznaczając odpowiednio pewien rodzaj uporządkowanej struktury i pewien rodzaj funkcji zachowującej granice. Ta elastyczność jest autentyczna; na przykład w niektórych systemach współbieżnych naturalne jest nałożenie warunku, że każda wysłana wiadomość musi ostatecznie zostać dostarczona. Jednak granicą łańcucha przybliżeń, w którym wiadomość nie została dostarczona, byłoby pełne obliczenie, w którym wiadomość nigdy nie została dostarczona!

Współczesnym odniesieniem do tego tematu jest rozdział Abramsky'ego i Junga [1994]. Starsze odniesienia obejmują Plotkin [1983, rozdział 8] i Smyth [1978].

Dziedziny władzy jako swobodne modele teorii niedeterminizmu

Teoretycy dziedzin doszli do abstrakcyjnego rozumienia dziedzin władzy jako wolnych modeli teorii niedeterminizmu. Tak jak konstrukcja skończonego zbioru mocy jest swobodną półkratą , tak konstrukcje potęgowe należy rozumieć abstrakcyjnie jako swobodne modele teorii niedeterminizmu. Zmieniając teorie niedeterminizmu, powstają różne domeny władzy.

Abstrakcyjna charakterystyka domen mocy jest często najłatwiejszym sposobem pracy z nimi, ponieważ jawne opisy są bardzo zawiłe. (Jedynym wyjątkiem jest domena mocy Hoare, która ma dość prosty opis.)

Teorie niedeterminizmu

Przypomnijmy sobie trzy teorie niedeterminizmu. Są to odmiany teorii półsieci . Teorie nie są teoriami algebraicznymi w konwencjonalnym sensie, ponieważ niektóre obejmują porządek dziedziny leżącej u ich podstaw.

Wszystkie teorie mają jedno sortowanie X i jedną operację binarną ∪. Chodzi o to, że operacja $\cup: X \times X \to X$ przyjmuje dwie kombinacje i zwraca niedeterministyczny wybór z nich.

Teoria potęgi Plotkina (za Gordonem Plotkinem ) ma następujące aksjomaty:

Idempotentność: x ∪ x = x
Przemienność: x ∪ y = y ∪ x
Łączność: ( x ∪ y ) ∪ z = x ∪ ( y ∪ z )

Niższa (lub Hoare , za Tonym Hoare'em ) teoria potęgi składa się z teorii potęgi Plotkina powiększonej o nierówność

x ≤ x ∪ y .

Górna (lub Smytha , za MB Smythem) teoria potęgi składa się z teorii potęgi Plotkina powiększonej o nierówność

x ∪ y ≤ x .

Modele teorii potęg

Modelem teorii potęgi Plotkina jest ciągła półkrata : jest to półsieć, której nośnikiem jest domena i dla której operacja jest ciągła. Pamiętaj, że operator nie musi być spotkaniem ani dołączeniem do zamówienia domeny. Homomorfizm ciągłych półsieci jest ciągłą funkcją między ich nośnikami, która szanuje operatora sieci.

Modele niższej teorii potęg nazywane są półsieciami inflacyjnymi; istnieje dodatkowy wymóg, aby operator zachowywał się trochę jak łączenie dla zamówienia. W przypadku teorii potęg wyższych modele nazywane są półsieciami deflacyjnymi; tutaj operator zachowuje się trochę jak spotkanie.

Dziedziny mocy jako wolne modele

Niech D będzie dziedziną. Dziedzina potęgowa Plotkina na D jest wolnym modelem teorii potęgowej Plotkina na D . Jest zdefiniowany jako (jeśli istnieje) model P ( D ) teorii potęg Plotkina (tj. ciągła półkrata) wyposażony w ciągłą funkcję D → P ( D ) taką, że dla dowolnej innej ciągłej półsieci L nad D istnieje unikalny ciągły homomorfizm półsieciowy P ( D ) → L sprawia, że oczywisty diagram dojeżdża do pracy .

Inne domeny władzy są definiowane abstrakcyjnie w podobny sposób.

Jawne opisy domen władzy

Niech D będzie dziedziną. Niższą domenę mocy można zdefiniować za pomocą

P. [ re ] = {zamknięcie [ ZA ] | Ø ∈ ZA ⊆ re } gdzie

zamknięcie [ ZA ] = { re ∈ re | ∃ X ⊆ re , X skierowane , re =

{\ Displaystyle \ vee}

X i ∀ x ∈ X ∃ za ∈ ZA x ≤ za } .

Innymi słowy, P [ D ] jest zbiorem podzbiorów D zamkniętych w dół , które są również domknięte pod istniejącymi najmniejszymi górnymi granicami zbiorów skierowanych w D . Należy zauważyć, że chociaż uporządkowanie na P [ D ] jest określone przez relację podzbioru, najmniejsze górne granice na ogół nie pokrywają się ze związkami.

Ważne jest, aby sprawdzić, które właściwości domen są zachowywane przez konstrukcje domen potęgowych. Na przykład dziedzina mocy Hoare'a ω-zupełnej jest ponownie ω-zupełna.

Domeny mocy dla współbieżności i aktorów

Domena mocy Clingera

Clinger [1981] skonstruował dziedzinę potęgi dla modelu aktora budując na domenie bazowej diagramów zdarzeń aktora , która jest niekompletna. Zobacz model Clingera .

Dziedzina mocy diagramów czasowych

Hewitt [2006] skonstruował dziedzinę mocy dla modelu aktora (który jest technicznie prostszy i łatwiejszy do zrozumienia niż model Clingera), opierając się na domenie bazowej czasowych diagramów zdarzeń aktora, która jest kompletna. Pomysł polega na dołączeniu czasu przybycia do każdej wiadomości otrzymanej przez Aktora. Zobacz Model diagramów czasowych .

Powiązania z topologią i przestrzenią Vietorisa

Dziedziny mogą być rozumiane jako przestrzenie topologiczne iw tym układzie konstrukcje potęgowe można łączyć z przestrzenią konstrukcji podzbiorów wprowadzoną przez Leopolda Vietorisa . Patrz np. [Smyth 1983].

Irena Greif. Semantyka komunikowania procesów równoległych Rozprawa doktorska MIT EECS. sierpień 1975.
Joseph E. Stoy , Semantyka denotacyjna: podejście Scotta-Stracheya do semantyki języka programowania . MIT Press, Cambridge, Massachusetts, 1977. (Klasyczny, choć przestarzały podręcznik).
Gordona Plotkina. Budowa powerdomain SIAM Journal on Computing, wrzesień 1976.
Carl Hewitt i Henry Baker Aktorzy i ciągłe działania funkcjonalne konferencji roboczej IFIP na temat formalnego opisu koncepcji programowania. 1-5 sierpnia 1977.
Henryk Baker . Systemy aktorów do obliczeń w czasie rzeczywistym Rozprawa doktorska MIT EECS. styczeń 1978.
Michał Smyth. Domeny mocy Journal of Computer and System Sciences . 1978.
George'a Milne'a i Robina Milnera . Procesy współbieżne i ich składnia JACM . kwiecień 1979.
SAMOCHÓD Hoare . Komunikacja sekwencyjnych procesów CACM . sierpień 1978.
Nissim Francez , CAR Hoare, Daniel Lehmann i Willem de Roever. Semantyka niedeterminizmu, współbieżności i komunikacji Journal of Computer and System Sciences . grudzień 1979.
Jerald Schwartz Denotacyjna semantyka równoległości w semantyce obliczeń współbieżnych. Springer-Verlag. 1979.
Williama Wadge'a. Ekstensjonalne traktowanie zakleszczenia przepływu danych Semantyka współbieżnych obliczeń. Springer-Verlag. 1979.
Ralph-Johan Powrót . Semantyka nieograniczonego niedeterminizmu ICALP 1980.
Dawid Park. O semantyce uczciwego paralelizmu Obrady Szkoły Zimowej w sprawie formalnej specyfikacji oprogramowania. Springer-Verlarg. 1980.
Will Clinger, Podstawy semantyki aktora . Rozprawa doktorska z matematyki MIT, czerwiec 1981.
Gordona Plotkina. Domeny (notatki z Pizy) . 1983. Dostępne od [1] .
MB Smyth, Dziedziny mocy i transformatory predykatów: widok topologiczny , LNCS 154, Springer, 1983.
S. Abramsky, A. Jung: Teoria domeny . W S. Abramsky, DM Gabbay, TSE Maibaum, redaktorzy, Handbook of Logic in Computer Science, tom. III. Oxford University Press, 1994. ( ISBN 0-19-853762-X ) (pobierz PDF PS.GZ )