Scott Information System

In domain theory, a branch of mathematics and computer science, a Scott information system is a primitive kind of logical deductive system often used as an alternative way of presenting Scott domains.

Definition

A Scott information system, ''A'', is an ordered triple $(T, Con, \vdash)$
* $T \mbox$
* $Con \subseteq \mathcal_f(T) \mbox T$
* $\subseteq (Con \setminus \lbrace \emptyset \rbrace)\times T$
satisfying
# $\mbox a \in X \in Con\mboxX \vdash a$
# $\mbox X \vdash Y \mboxY \vdash a \mboxX \vdash a$
# $\mboxX \vdash a \mbox X \cup \ \in Con$
# $\forall a \in T : \ \in Con$
# $\mboxX \in Con \mbox X^\prime\, \subseteq X \mboxX^\prime \in Con.$

Here $X \vdash Y$ means $\forall a \in Y, X \vdash a.$

Examples

Natural numbers

The return value of a partial recursive function, which either returns a natural number or goes into an infinite recursion, can be expressed as a simple Scott information system as follows:
* $T := \mathbb$
* $Con := \ \cup \$
* $X \vdash a\iff a \in X.$

That is, the result can either be a natural number, represented by the singleton set $\$, or "infinite recursion," represented by $\empty$.

Of course, the same construction can be carried out with any other set instead of $\mathbb$.

Propositional calculus

The propositional calculus gives us a very simple Scott information system as follows:

* $T := \$
* $Con := \$
* $X \vdash a\iff X \vdash a \mbox.$

Scott domains

Let ''D'' be a Scott domain. Then we may define an information system as follows

* $T := D^0$ the set of compact elements of $D$
* $Con := \$
* $X \vdash d\iff d \sqsubseteq \bigsqcup X.$

Let $\mathcal$ be the mapping that takes us from a Scott domain, ''D'', to the information system defined above.

Information systems and Scott domains

Given an information system, $A = (T, Con, \vdash)$, we can build a Scott domain as follows.

* Definition: $x \subseteq T$ is a point if and only if
** $\mboxX \subseteq_f x \mbox X \in Con$
** $\mboxX \vdash a \mbox X \subseteq_f x \mbox a \in x.$

Let $\mathcal(A)$ denote the set of points of ''A'' with the subset ordering. $\mathcal(A)$ will be a countably based Scott domain when ''T'' is countable. In general, for any Scott domain ''D'' and information system ''A''
* $\mathcal(\mathcal(D)) \cong D$
* $\mathcal(\mathcal{D}(A)) \cong A$
where the second congruence is given by approximable mappings.

See also

* Scott domain
* Domain theory

References

* Glynn Winskel: "The Formal Semantics of Programming Languages: An Introduction", MIT Press, 1993 (chapter 12)

Models of computation
Domain theory