Күш домендері: белгісіз және параллель есептеулер теориясы
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] Актерлік модель үшін қуат доменін құрды, бұл Актерлік оқиғалар диаграммасының негізгі доменіне негіделген, бірақ толық емес. Клингердің моделіне қараңыз.
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].