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{ 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\mbox{ 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\mbox{ 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\mbox{ 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 iff
  • $\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.

See also

• Scott domain
• Domain theory

References

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