パワードメイン

表示的意味論とドメイン理論では、電力ドメインは非決定論的かつ並行的な計算 のドメインです。

関数のべき乗ドメインの考え方は、非決定性関数は決定性集合値関数として記述できるというものです。集合には、非決定性関数が特定の引数に対して取ることができるすべての値が含まれます。並行システムの場合、この考え方は、すべての可能な計算の集合を表現することです。

大まかに言えば、パワー ドメインとは、その要素がドメインの特定のサブセットであるドメインです。ただし、このアプローチを単純に採用すると、望ましい特性を持たないドメインが生まれることが多く、パワー ドメインの概念はますます複雑になります。一般的なバリエーションには、Plotkin パワー ドメイン、上位パワー ドメイン、下位パワー ドメインの 3 つがあります。これらの概念を理解する 1 つの方法は、非決定論の理論の自由モデルとして理解することです。

この記事の大部分では、「ドメイン」と「連続関数」という用語をかなり緩く使用しており、それぞれある種の秩序立った構造とある種の限界保存関数を意味します。この柔軟性は本物です。たとえば、一部の並行システムでは、送信されたすべてのメッセージが最終的に配信される必要があるという条件を課すのは当然です。ただし、メッセージが配信されなかった近似の連鎖の限界は、メッセージが配信されなかった完了した計算になります。

この主題に関する最近の参考文献としては、アブラムスキーとユング[1994]の章があります。より古い参考文献としては、プロトキン[1983、第8章]とスミス[1978]のものがあります。

ドメイン理論家は、パワードメインを非決定論の理論の自由モデルとして抽象的に理解するようになりました。有限パワーセット構成が自由半格子であるのと同様に、パワードメイン構成は非決定論の理論の自由モデルとして抽象的に理解されるべきです。非決定論の理論を変えることで、異なるパワードメインが生まれます。

明示的な説明は非常に複雑なため、パワードメインの抽象的な特徴付けは、パワードメインを扱う最も簡単な方法であることがよくあります。(例外は Hoare パワードメインで、これはかなり簡単な説明になっています。)

非決定論の 3 つの理論を思い出します。これらは半格子理論のバリエーションです。これらの理論は、基礎となる領域の順序に関係するものもあるため、従来の意味での代数理論ではありません。

すべての理論には、1 つのソートXと 1 つの二項演算∪ があります。その考え方は、演算∪: X × X → X が2 つの組み合わせを受け取り、それらの非決定的な選択を返すというものです。

プロトキンのべき乗理論(ゴードン・プロトキンに由来) には次の公理があります。

• 冪等性: x ∪ x = x
• 交換法則: x ∪ y = y ∪ x
• 結合性: ( x ∪ y ) ∪ z = x ∪ ( y ∪ z )

下側の（またはトニー・ホーアにちなんでホーアの）べき乗理論は、プロトキンのべき乗理論に不等式を加えたものである。

• x ≤ x ∪ yです。

上方（またはMBスミスにちなんでスミス）のべき乗理論は、プロトキンのべき乗理論に不等式を加えたものである。

• x ∪ y ≤ xです。

Plotkin のべき理論のモデルは連続半格子です。これは、キャリアがドメインであり、演算が連続する半格子です。演算子は、ドメインの順序に対して meet または join である必要がないことに注意してください。連続半格子の準同型は、格子演算子を尊重するキャリア間の連続関数です。

下位のべき理論のモデルはインフレーション半格子と呼ばれます。演算子が順序に対してジョインのように動作するという追加の要件があります。上位のべき理論の場合、モデルはデフレーション半格子と呼ばれます。この場合、演算子はミートのように動作します。^[トーン]

D を領域とする。 D上の Plotkin 冪領域は、 D上の Plotkin 冪理論の自由モデルである。これは、（存在する場合）連続関数D → P ( D ) を備えた Plotkin 冪理論のモデルP ( D ) （つまり連続半格子）であると定義され、 D上の他の任意の連続半格子Lに対して、明らかな図式が可換となる一意の連続半格子準同型P ( D ) → Lが存在する。

他のパワードメインも同様の方法で抽象的に定義されます。

Dをドメインと する。下べきドメインは次のように定義される。

• P [ D ] = {閉包[ A ] | Ø ∈ A ⊆ D } ただし

閉包[ A ] = { d ∈ D | ∃ X ⊆ D、X は有向、d = X、∀ x ∈ X ∃ a ∈ A x ≤ a }。${\displaystyle \vee}$

言い換えれば、P [ D ] は、 Dの下向きに閉じた部分集合の集合であり、 D内の有向集合の既存の最小上限の下でも閉じています。 P [ D ]上の順序は部分集合関係によって与えられますが、最小上限は一般に和集合と一致しないことに注意してください。

パワードメイン構成によってドメインのどの特性が保持されるかを確認することが重要です。たとえば、ω 完全ドメインの Hoare パワードメインは、やはり ω 完全です。

Clinger[1981]は、不完全なアクターイベントダイアグラムの基本ドメインに基づいて、アクターモデルのパワードメインを構築しました。Clingerのモデルを参照してください。

Hewitt [2006] は、完全な時間指定の Actor イベント ダイアグラムの基本ドメインに基づいて、 Actor モデルのパワー ドメイン(技術的には Clinger のモデルよりも単純で理解しやすい) を構築しました。そのアイデアは、Actor が受信した各メッセージに到着時刻を添付することです。時間指定のダイアグラム モデルを参照してください。

ドメインは位相空間として理解することができ、この設定では、べきドメイン構成はレオポルド・ヴィエトリスによって導入された部分集合空間構成と関連付けることができます。たとえば、[Smyth 1983]を参照してください。

• アイリーン・グレイフ。 並列プロセスの通信の意味論、 MIT EECS 博士論文。1975 年 8 月。
• Joseph E. Stoy著『表示的意味論: プログラミング言語意味論に対する Scott-Strachey アプローチ』。MIT Press、マサチューセッツ州ケンブリッジ、1977 年。(時代遅れではあるが、古典的教科書。)
• Gordon Plotkin. パワードメイン構築 SIAM Journal on Computing 1976 年 9 月。
• Carl HewittとHenry Baker の 「アクターと連続関数」、 プログラミング概念の形式的記述に関する IFIP ワーキング カンファレンスの議事録。1977 年 8 月 1 ～ 5 日。
• ヘンリー・ベイカー.リアルタイム計算のためのアクターシステムMIT EECS 博士論文. 1978 年 1 月.
• マイケル・スミス。 電力ドメイン、 コンピュータおよびシステム科学ジャーナル。1978 年。
• George Milne とRobin Milner . 並行プロセスとその構文 JACM . 1979 年 4 月。
• CAR Hoare . 通信シーケンシャルプロセス CACM . 1978 年 8 月。
• Nissim Francez、CAR Hoare、Daniel Lehmann、および Willem de Roever。 非決定性、並行性、および通信のセマンティクス、 Journal of Computer and System Sciences。1979 年 12 月。
• ジェラルド・シュワルツ「並行計算の意味論」における並列処理の表示的意味論。Springer-Verlag、1979年。
• ウィリアム・ワッジ。 データフローデッドロックの拡張的処理、並行計算の意味論。Springer-Verlag。1979年。
• Ralph-Johan Back .無制限非決定性の意味論 ICALP 1980.
• David Park. 公平な並列処理の意味論について形式ソフトウェア仕様に関する冬期講習会の議事録。Springer-Verlarg。1980 年。
• ウィル・クリンガー、「アクターセマンティクスの基礎」、MIT数学博士論文、1981年6月。
• ゴードン・プロトキン.ドメイン（ピサノート） .1983.[1]から入手可能。
• MB Smyth、「電力ドメインと述語トランスフォーマー：トポロジカルな視点」、LNCS 154、Springer、1983 年。
• S. Abramsky、A. Jung:ドメイン理論。S. Abramsky、DM Gabbay、TSE Maibaum 編著『Handbook of Logic in Computer Science』第 3 巻。オックスフォード大学出版局、1994 年。( ISBN  0-19-853762-X ) (PDF PS.GZ をダウンロード)