В теории предметной области , разделе математики и информатики , информационная система Скотта - это примитивный вид логической дедуктивной системы, часто используемый в качестве альтернативного способа представления предметных областей Скотта .
Определение [ править ] Информационная система Скотта , , является упорядоченной тройкой ( Т , C о п , ⊢ ) {\ displaystyle (T, Con, \ vdash)}
Т представляет собой набор токенов (основных единиц информации) {\ displaystyle T {\ mbox {- это набор токенов (основные единицы информации)}}} C о п ⊆ п ж ( Т ) конечные подмножества Т {\ displaystyle Con \ substeq {\ mathcal {P}} _ {f} (T) {\ mbox {конечные подмножества}} T} ⊢ ⊆ ( C о п ∖ { ∅ } ) × Т {\ Displaystyle {\ vdash} \ substeq (Con \ setminus \ lbrace \ emptyset \ rbrace) \ times T} удовлетворение
Если а ∈ Икс ∈ C о п тогда Икс ⊢ а {\ displaystyle {\ mbox {If}} a \ in X \ in Con {\ mbox {then}} X \ vdash a} Если Икс ⊢ Y and Y ⊢ a , then X ⊢ a {\displaystyle {\mbox{If }}X\vdash Y{\mbox{ and }}Y\vdash a{\mbox{, then }}X\vdash a} If X ⊢ a then X ∪ { a } ∈ C o n {\displaystyle {\mbox{If }}X\vdash a{\mbox{ then }}X\cup \{a\}\in Con} ∀ a ∈ T : { a } ∈ C o n {\displaystyle \forall a\in T:\{a\}\in Con} If X ∈ C o n and X ′ ⊆ X then X ′ ∈ C o n . {\displaystyle {\mbox{If }}X\in Con{\mbox{ and }}X^{\prime }\,\subseteq X{\mbox{ then }}X^{\prime }\in Con.} Здесь означает X ⊢ Y {\displaystyle X\vdash Y} ∀ a ∈ Y , X ⊢ a . {\displaystyle \forall a\in Y,X\vdash a.}
Натуральные числа [ править ] Возвращаемое значение частично рекурсивной функции , которая либо возвращает натуральное число, либо переходит в бесконечную рекурсию, может быть выражено как простая информационная система Скотта следующим образом:
T := N {\displaystyle T:=\mathbb {N} } C o n := { ∅ } ∪ { { n } ∣ n ∈ N } {\displaystyle Con:=\{\emptyset \}\cup \{\{n\}\mid n\in \mathbb {N} \}} X ⊢ a ⟺ a ∈ X . {\displaystyle X\vdash a\iff a\in X.} То есть результатом может быть либо натуральное число, представленное одноэлементным набором , либо «бесконечная рекурсия», представленная . { n } {\displaystyle \{n\}} ∅ {\displaystyle \emptyset }
Конечно, такую же конструкцию можно провести с любым другим набором вместо . N {\displaystyle \mathbb {N} }
Исчисление высказываний [ править ] Исчисление дает нам очень простую информационную систему Скотт следующим образом :
T := { ϕ ∣ ϕ is satisfiable } {\displaystyle T:=\{\phi \mid \phi {\mbox{ is satisfiable}}\}} C o n := { X ∈ P f ( T ) ∣ X is consistent } {\displaystyle Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ is consistent}}\}} X ⊢ a ⟺ X ⊢ a in the propositional calculus . {\displaystyle X\vdash a\iff X\vdash a{\mbox{ in the propositional calculus}}.} Домены Скотта [ править ] Пусть D - область Скотта . Тогда мы можем определить информационную систему следующим образом
T := D 0 {\displaystyle T:=D^{0}} множество компактных элементов из D {\displaystyle D} C o n := { X ∈ P f ( T ) ∣ X has an upper bound } {\displaystyle Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ has an upper bound}}\}} X ⊢ d ⟺ d ⊑ ⨆ X . {\displaystyle X\vdash d\iff d\sqsubseteq \bigsqcup X.} Позвольте быть отображением, которое ведет нас из области Скотта, D , в информационную систему, определенную выше. I {\displaystyle {\mathcal {I}}}
Информационные системы и домены Скотта [ править ] Учитывая информационную систему, мы можем построить домен Скотта следующим образом. A = ( T , C o n , ⊢ ) {\displaystyle A=(T,Con,\vdash )}
Определение: является точкой тогда и только тогда, когда x ⊆ T {\displaystyle x\subseteq T} If X ⊆ f x then X ∈ C o n {\displaystyle {\mbox{If }}X\subseteq _{f}x{\mbox{ then }}X\in Con} If X ⊢ a and X ⊆ f x then a ∈ x . {\displaystyle {\mbox{If }}X\vdash a{\mbox{ and }}X\subseteq _{f}x{\mbox{ then }}a\in x.} Обозначим через множество точек A с упорядочением подмножеств. будет счетной областью Скотта, когда T является счетным. В общем, для любого домена Скотта D и информационной системы A D ( A ) {\displaystyle {\mathcal {D}}(A)} D ( A ) {\displaystyle {\mathcal {D}}(A)}
D ( I ( D ) ) ≅ D {\displaystyle {\mathcal {D}}({\mathcal {I}}(D))\cong D} I ( D ( A ) ) ≅ A {\displaystyle {\mathcal {I}}({\mathcal {D}}(A))\cong A} где второе сравнение дается аппроксимируемыми отображениями .
Глинн Винскель: "Формальная семантика языков программирования: введение", MIT Press, 1993 (глава 12)