Scott information system explained

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 isasetoftokens(thebasicunitsofinformation) Con \subseteq l{P} _{f(T)} thefinitesubsetsof T {\vdash} \subseteq (Con \setminus \lbrace \emptyset \rbrace) x T satisfyingIf a \in X \in Con then X \vdash a If X \vdash Y and Y \vdash a ,then X \vdash a If X \vdash a then X \cup \{ a \} \in Con \forall a \in T : \{ a\} \in Con If X \in Con and X ^{\prime} \subseteq X then X ^{\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 : = N Con : = \{ \empty \} \cup \{ \{ n \} \mid n \in N \} X \vdash a\iff a \in X.

That is, the result can either be a natural number, represented by the singleton set

\{n\} , or "infinite recursion," represented by \empty .

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

N .

Propositional calculus

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

T : = \{ \phi \mid \phi issatisfiable \} Con : = \{ X \in l{P} _{f(T)} \mid X isconsistent \} X \vdash a\iff X \vdash a inthepropositionalcalculus .

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 \in l{P} _{f(T)} \mid X hasanupperbound \} X \vdash d\iff d \sqsubseteq s qcup X.

Let

l{I} 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 ifIf X \subseteq _{f} x then X \in Con If X \vdash a and X \subseteq _{f} x then a \in x.

Let

l{D}(A) denote the set of points of A with the subset ordering. l{D}(A) will be a countably based Scott domain when T is countable. In general, for any Scott domain D and information system Al{D}( l{I}(D)) \cong D l{I}( l{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)