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 [math]\displaystyle{ (T, Con, \vdash) }[/math]
- [math]\displaystyle{ T \mbox{ is a set of tokens (the basic units of information)} }[/math]
- [math]\displaystyle{ Con \subseteq \mathcal{P}_f(T) \mbox{ the finite subsets of } T }[/math]
- [math]\displaystyle{ {\vdash} \subseteq (Con \setminus \lbrace \emptyset \rbrace)\times T }[/math]
satisfying
- [math]\displaystyle{ \mbox{If } a \in X \in Con\mbox{ then }X \vdash a }[/math]
- [math]\displaystyle{ \mbox{If } X \vdash Y \mbox{ and }Y \vdash a \mbox{, then }X \vdash a }[/math]
- [math]\displaystyle{ \mbox{If }X \vdash a \mbox{ then } X \cup \{ a \} \in Con }[/math]
- [math]\displaystyle{ \forall a \in T : \{ a\} \in Con }[/math]
- [math]\displaystyle{ \mbox{If }X \in Con \mbox{ and } X^\prime\, \subseteq X \mbox{ then }X^\prime \in Con. }[/math]
Here [math]\displaystyle{ X \vdash Y }[/math] means [math]\displaystyle{ \forall a \in Y, X \vdash a. }[/math]
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:
- [math]\displaystyle{ T := \mathbb{N} }[/math]
- [math]\displaystyle{ Con := \{ \empty \} \cup \{ \{ n \} \mid n \in \mathbb{N} \} }[/math]
- [math]\displaystyle{ X \vdash a\iff a \in X. }[/math]
That is, the result can either be a natural number, represented by the singleton set [math]\displaystyle{ \{n\} }[/math], or "infinite recursion," represented by [math]\displaystyle{ \empty }[/math].
Of course, the same construction can be carried out with any other set instead of [math]\displaystyle{ \mathbb{N} }[/math].
Propositional calculus
The propositional calculus gives us a very simple Scott information system as follows:
- [math]\displaystyle{ T := \{ \phi \mid \phi \mbox{ is satisfiable} \} }[/math]
- [math]\displaystyle{ Con := \{ X \in \mathcal{P}_f(T) \mid X \mbox{ is consistent} \} }[/math]
- [math]\displaystyle{ X \vdash a\iff X \vdash a \mbox{ in the propositional calculus}. }[/math]
Scott domains
Let D be a Scott domain. Then we may define an information system as follows
- [math]\displaystyle{ T := D^0 }[/math] the set of compact elements of [math]\displaystyle{ D }[/math]
- [math]\displaystyle{ Con := \{ X \in \mathcal{P}_f(T) \mid X \mbox{ has an upper bound} \} }[/math]
- [math]\displaystyle{ X \vdash d\iff d \sqsubseteq \bigsqcup X. }[/math]
Let [math]\displaystyle{ \mathcal{I} }[/math] 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, [math]\displaystyle{ A = (T, Con, \vdash) }[/math], we can build a Scott domain as follows.
- Definition: [math]\displaystyle{ x \subseteq T }[/math] is a point if and only if
- [math]\displaystyle{ \mbox{If }X \subseteq_f x \mbox{ then } X \in Con }[/math]
- [math]\displaystyle{ \mbox{If }X \vdash a \mbox{ and } X \subseteq_f x \mbox{ then } a \in x. }[/math]
Let [math]\displaystyle{ \mathcal{D}(A) }[/math] denote the set of points of A with the subset ordering. [math]\displaystyle{ \mathcal{D}(A) }[/math] will be a countably based Scott domain when T is countable. In general, for any Scott domain D and information system A
- [math]\displaystyle{ \mathcal{D}(\mathcal{I}(D)) \cong D }[/math]
- [math]\displaystyle{ \mathcal{I}(\mathcal{D}(A)) \cong A }[/math]
where the second congruence is given by approximable mappings.
See also
References
- Glynn Winskel: "The Formal Semantics of Programming Languages: An Introduction", MIT Press, 1993 (chapter 12)
 |  |
