Loading article…
表示的意味論および領域理論において、パワー領域とは、非決定論的かつ並行的な計算が行われる領域のことである。
関数のべき領域の概念は、非決定性関数を決定性集合値関数として記述できるというものです。ここで、集合には、与えられた引数に対して非決定性関数が取り得るすべての値が含まれます。並行システムの場合、この概念は、可能なすべての計算の集合を表現することにあります。
大まかに言えば、パワー領域とは、ある領域の特定の部分集合を要素とする領域のことである。しかし、このアプローチを単純に採用すると、望ましい特性を必ずしも備えていない領域が生じ、パワー領域の概念はますます複雑化していく。一般的なパワー領域には、プロトキン領域、上位パワー領域、下位パワー領域の3種類がある。これらの概念を理解する一つの方法は、非決定論の理論の自由モデルとして捉えることである。
この記事の大部分において、「ドメイン」と「連続関数」という用語をかなり緩やかに用いています。それぞれ、何らかの順序構造と、何らかの極限保存関数を意味します。この柔軟性は正当なものです。例えば、一部の並行システムでは、送信されたすべてのメッセージが最終的に配信されるという条件を課すのが自然です。しかし、メッセージが配信されなかった一連の近似処理の極限は、メッセージが一度も配信されなかった完了済みの計算結果となるでしょう。
このテーマに関する現代的な参考文献としては、アブラムスキーとユングによる章[1994]が挙げられる。より古い参考文献としては、プロトキン[1983、第8章]やスミス[1978]の論文がある。
領域理論家は、パワー領域を非決定論の理論のための自由モデルとして抽象的に理解するようになった。有限冪集合の構成が自由半束であるのと同様に、パワー領域の構成も非決定論の理論のための自由モデルとして抽象的に理解されるべきである。非決定論の理論を変えることで、異なるパワー領域が生じる。
パワードメインを抽象的に特徴づけることは、明示的な記述が非常に複雑であるため、多くの場合、それらを扱う最も簡単な方法となる。（例外として、比較的わかりやすい記述を持つホーアのパワードメインがある。）
非決定論の3つの理論を振り返ってみよう。これらは半束理論の変形である。これらの理論は、基底となる領域の順序に関わるものもあるため、従来の意味での代数理論ではない。
すべての理論には、1つのソートXと1つの二項演算∪が存在する。演算∪: X × X → Xは2つの組み合わせを受け取り、それらの非決定的な選択を返すという考え方である。
プロトキンのべき乗理論（ゴードン・プロトキンにちなんで名付けられた）は、以下の公理を持つ。
下位（またはトニー・ホーアにちなんでホーア）べき乗理論は、不等式で拡張されたプロトキンべき乗理論から構成される。
上位（またはMBスミスにちなんでスミス）べき乗理論は、不等式で拡張されたプロトキンべき乗理論から構成される。
プロトキンべき理論のモデルは連続半束です。これは、担体が領域であり、演算が連続である半束です。演算子は、領域の順序に関して、必ずしも交わりや結合である必要はありません。連続半束の準同型写像は、それらの担体間の連続関数であり、かつ半束準同型写像でもあります。
低べき乗理論のモデルはインフレーション半束と呼ばれ、演算子が順序に対して結合のように振る舞うという追加要件があります。高べき乗理論の場合、モデルはデフレーション半束と呼ばれ、ここでは演算子がミートのように振る舞います。
Dを領域とする。D 上のプロトキン冪領域は、D上のプロトキン冪理論の自由モデルである。それは、（存在する場合）プロトキン冪理論のモデルP ( D )（すなわち連続半束）であり、連続関数D → P ( D ) を備え、他の任意の連続半束Lおよび連続関数D → Lに対して、明らかな図式が可換となるような一意の連続半束準同型P ( D ) → Lが存在するものと定義される。
他の権力領域も同様の方法で抽象的に定義される。
Dを領域とする。低べき領域は次のように定義できる。
言い換えれば、P [ D ] は、 Dの下方閉集合の集合であり、かつD内の有向集合の既存の最小上界の下でも閉集合である集合の集合です。P [ D ]上の順序は部分集合関係によって与えられますが、最小上界は一般に和集合とは一致しないことに注意してください。
べき領域の構成によって、領域のどの性質が保持されるかを確認することが重要です。例えば、ω完全領域のホーアべき領域は、再びω完全になります。
クリンガー[1981]は、不完全なアクターイベント図の基本ドメインに基づいて、アクターモデルのパワードメインを構築しました。クリンガーのモデルを参照してください。
Hewitt [2006] は、完全な時間付きアクターイベント図の基本ドメインに基づいて、アクターモデルのパワードメインを構築しました（これは、技術的には Clinger のモデルよりも単純で理解しやすいものです）。そのアイデアは、アクターが受信する各メッセージに到着時間を関連付けることです。時間付き図モデルを参照してください。
ドメインは位相空間として理解することができ、この設定では、冪ドメイン構成はレオポルド・ヴィエトリスによって導入された部分集合空間構成と関連付けることができる。例えば、[Smyth 1983]を参照のこと。
