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

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

Информационная система Скотта , A , представляет собой упорядоченную тройку${\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\если и только если a\в 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\ifl 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}$

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

• Домен Скотта
• Теория домена

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