Информационная система Скотта

В теории предметной области , разделе математики и информатики , информационная система Скотта представляет собой примитивный вид логической дедуктивной системы, часто используемый в качестве альтернативного способа представления доменов Скотта .

Определение

представляет Информационная система Скотта A собой упорядоченную тройку $(T,Con,\vdash )$

• $T{\mbox{ is a set of tokens (the basic units of information)}}$
• $Con\subseteq {\mathcal {P}}_{f}(T){\mbox{ the finite subsets of }}T$
• ${\vdash }\subseteq (Con\setminus \lbrace \emptyset \rbrace )\times T$

удовлетворяющий

1. ${\mbox{If }}a\in X\in Con{\mbox{ then }}X\vdash a$
2. ${\mbox{If }}X\vdash Y{\mbox{ and }}Y\vdash a{\mbox{, then }}X\vdash a$
3. ${\mbox{If }}X\vdash a{\mbox{ then }}X\cup \{a\}\in Con$
4. $\forall a\in T:\{a\}\in Con$
5. ${\mbox{If }}X\in Con{\mbox{ and }}X^{\prime }\,\subseteq X{\mbox{ then }}X^{\prime }\in Con.$

Здесь $X\vdash Y$ означает $\forall a\in Y,X\vdash a.$

Примеры

Натуральные числа

Возвращаемое значение частично рекурсивной функции , которая либо возвращает натуральное число, либо переходит в бесконечную рекурсию, может быть выражено в виде простой информационной системы Скотта следующим образом:

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

То есть результатом может быть натуральное число, представленное одноэлементным набором $\{n\}$или «бесконечная рекурсия», представленная $\emptyset$.

Разумеется, то же построение можно провести и с любым другим набором вместо $\mathbb {N}$.

Исчисление высказываний

Исчисление высказываний дает нам следующую очень простую информационную систему Скотта:

• $T:=\{\phi \mid \phi {\mbox{ is satisfiable}}\}$
• $Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ is consistent}}\}$
• $X\vdash a\iff X\vdash a{\mbox{ in the propositional calculus}}.$

Домены Скотта

Пусть D — область Скотта . Тогда мы можем определить информационную систему следующим образом

• $T:=D^{0}$ набор компактных элементов $D$
• $Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ has an upper bound}}\}$
• $X\vdash d\iff d\sqsubseteq \bigsqcup X.$

Позволять ${\mathcal {I}}$ — это отображение, которое переносит нас из домена Скотта D в информационную систему, определенную выше.

Информационные системы

Учитывая информационную систему, $A=(T,Con,\vdash )$, мы можем создать домен Скотта следующим образом.

• Определение: $x\subseteq T$ является точкой тогда и только тогда, когда
  • ${\mbox{If }}X\subseteq _{f}x{\mbox{ then }}X\in Con$
  • ${\mbox{If }}X\vdash a{\mbox{ and }}X\subseteq _{f}x{\mbox{ then }}a\in x.$

Позволять ${\mathcal {D}}(A)$ обозначим множество точек A с упорядоченным подмножеством. ${\mathcal {D}}(A)$ будет счетной областью Скотта, когда T счетно. В общем случае для любого домена Скотта D и информационной системы A

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

где второе сравнение задается аппроксимируемыми отображениями .

См. также

• Домен Скотта
• Теория предметной области

Ссылки

• Глинн Винскель: «Формальная семантика языков программирования: введение», MIT Press, 1993 (глава 12)