スコット情報システム

数学とコンピュータサイエンスの一分野であるドメイン理論において、スコット情報システムは、スコット領域を表現する代替方法としてよく使用される、原始的な種類の論理演繹システムです。

スコット情報システムAは、順序付けられた3つの${\displaystyle (T,Con,\vdash )}$

• ${\displaystyle T{\mbox{ はトークン（情報の基本単位）の集合である}}}$
• ${\displaystyle Con\subseteq {\mathcal {P}}_{f}(T){\mbox{ }}T の有限部分集合}$
• ${\displaystyle {\vdash }\subseteq (Con\setminus \lbrace \emptyset \rbrace )\times T}$

満足のいく

1. ${\displaystyle {\mbox{a\in X\in Con{\mbox{ ならば X\vdash a}$
2. ${\displaystyle {\mbox{}}X\vdash Y{\mbox{ かつ }}Y\vdash a{\mbox{ ならば }}X\vdash a}$
3. ${\displaystyle {\mbox{X\vdash a{\mbox{ ならば }}X\cup \{a\}\in Con}$
4. ${\displaystyle \forall a\in T:\{a\}\in Con}$
5. ${\displaystyle {\mbox{X\in Con{\mbox{ かつ }}X^{\prime }\,\subseteq X{\mbox{ ならば }}X^{\prime }\in Con.}$

ここでの意味は${\displaystyle X\vdash Y}$${\displaystyle \forall a\in Y,X\vdash a.}$

自然数を返すか無限再帰に入る 部分再帰関数の戻り値は、次のように単純なスコット情報システムとして表現できます。

• ${\displaystyle T:=\mathbb {N} }$
• ${\displaystyle Con:=\{\emptyset \}\cup \{\{n\}\mid n\in \mathbb {N} \}}$
• ${\displaystyle X\vdash a\iff a\in X.}$

つまり、結果は、シングルトン セット で表される自然数、または で表される「無限再帰」のいずれかになります。 ${\displaystyle \{n\}}$${\displaystyle \emptyset}$

もちろん、 の代わりに他の任意のセットを使用して同じ構築を実行することもできます。 ${\displaystyle \mathbb {N} }$

命題計算により、次のような非常に単純なスコット情報システムが得られます。

• ${\displaystyle T:=\{\phi \mid \phi {\mbox{ は満たされる}}\}}$
• ${\displaystyle Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ は矛盾しない}}\}}$
• ${\displaystyle X\vdash a\iff X\vdash a{\mbox{ 命題論理において}}.}$

Dをスコットドメインとする。すると、情報システムは次のように定義できる。

• ${\displaystyle T:=D^{0}}$コンパクト要素の集合${\displaystyle D}$
• ${\displaystyle Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ には上限がある}}\}}$
• ${\displaystyle X\vdash d\iff d\sqsubseteq \bigsqcup X.}$

スコットドメインDから上記で定義した情報システムへ のマッピングをとします。${\displaystyle {\mathcal {I}}}$

情報システム が与えられた場合、次のようにスコットドメインを構築できます。 ${\displaystyle A=(T,Con,\vdash )}$

• 定義:は点であり、その場合のみ ${\displaystyle x\subseteq T}$
  • ${\displaystyle {\mbox{X\subseteq _{f}x{​​\mbox{ ならば、X\in Con}$
  • ${\displaystyle {\mbox{X\vdash a{\mbox{ かつ X\subseteq _{f}x{​​\mbox{ ならば a\in x.}$

を部分集合の順序を持​​つAの点の集合とします。Tが可算な場合、は可算基底スコット領域になります。一般に、任意のスコット領域Dと情報システムAに対して、${\displaystyle {\mathcal {D}}(A)}$${\displaystyle {\mathcal {D}}(A)}$

• ${\displaystyle {\mathcal {D}}({\mathcal {I}}(D))\cong D}$
• ${\displaystyle {\mathcal {I}}({\mathcal {D}}(A))\cong A}$

ここで、2 番目の合同は近似可能なマッピングによって与えられます。

• スコットドメイン
• ドメイン理論

• グリン・ウィンスケル:「プログラミング言語の形式意味論: 入門」、MIT 出版、1993 年 (第 12 章)