Scott information system

Definition

A Scott information system, A, is an ordered triple (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 satisfying

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.

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{N}
• Con := { \empty } \cup { { n } \mid n \in \mathbb{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 \mathbb{N}.

Propositional calculus

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

• 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}.

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 \mathcal{P}_f(T) \mid X \mbox{ has an upper bound} }
• X \vdash d\iff d \sqsubseteq \bigsqcup X.

Let \mathcal{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 if
  • \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.

Let \mathcal{D}(A) denote the set of points of A with the subset ordering. \mathcal{D}(A) will be a countably based Scott domain when T is countable. In general, for any Scott domain D and information system A

• \mathcal{D}(\mathcal{I}(D)) \cong D
• \mathcal{I}(\mathcal{D}(A)) \cong A where the second congruence is given by approximable mappings.

References

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