Scott information system

A Scott information system, A, is an ordered triple $(T,\; Con,\; \backslash vdash)$

• $T\; \backslash mbox\{\; is\; a\; set\; of\; tokens\; (the\; basic\; units\; of\; information)\}$
• $Con\; \backslash subseteq\; \backslash mathcal\{P\}\_f(T)\; \backslash mbox\{\; the\; finite\; subsets\; of\; \}\; T$
• $\{\backslash vdash\}\; \backslash subseteq\; (Con\; \backslash setminus\; \backslash lbrace\; \backslash emptyset\; \backslash rbrace)\backslash times\; T$

satisfying

1. $\backslash mbox\{If\; \}\; a\; \backslash in\; X\; \backslash in\; Con\backslash mbox\{\; then\; \}X\; \backslash vdash\; a$
2. $\backslash mbox\{If\; \}\; X\; \backslash vdash\; Y\; \backslash mbox\{\; and\; \}Y\; \backslash vdash\; a\; \backslash mbox\{,\; then\; \}X\; \backslash vdash\; a$
3. $\backslash mbox\{If\; \}X\; \backslash vdash\; a\; \backslash mbox\{\; then\; \}\; X\; \backslash cup\; \backslash \{\; a\; \backslash \}\; \backslash in\; Con$
4. $\backslash forall\; a\; \backslash in\; T\; :\; \backslash \{\; a\backslash \}\; \backslash in\; Con$
5. $\backslash mbox\{If\; \}X\; \backslash in\; Con\; \backslash mbox\{\; and\; \}\; X^\backslash prime\backslash ,\; \backslash subseteq\; X\; \backslash mbox\{\; then\; \}X^\backslash prime\; \backslash in\; Con.$

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

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\; :=\; \backslash mathbb\{N\}$
• $Con\; :=\; \backslash \{\; \backslash empty\; \backslash \}\; \backslash cup\; \backslash \{\; \backslash \{\; n\; \backslash \}\; \backslash mid\; n\; \backslash in\; \backslash mathbb\{N\}\; \backslash \}$
• $X\; \backslash vdash\; a\backslash iff\; a\; \backslash in\; X.$

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

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

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

• $T\; :=\; \backslash \{\; \backslash phi\; \backslash mid\; \backslash phi\; \backslash mbox\{\; is\; satisfiable\}\; \backslash \}$
• $Con\; :=\; \backslash \{\; X\; \backslash in\; \backslash mathcal\{P\}\_f(T)\; \backslash mid\; X\; \backslash mbox\{\; is\; consistent\}\; \backslash \}$
• $X\; \backslash vdash\; a\backslash iff\; X\; \backslash vdash\; a\; \backslash mbox\{\; in\; the\; propositional\; calculus\}.$

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

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

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

• Definition: $x\; \backslash subseteq\; T$ is a point if and only if
• $\backslash mbox\{If\; \}X\; \backslash subseteq\_f\; x\; \backslash mbox\{\; then\; \}\; X\; \backslash in\; Con$
• $\backslash mbox\{If\; \}X\; \backslash vdash\; a\; \backslash mbox\{\; and\; \}\; X\; \backslash subseteq\_f\; x\; \backslash mbox\{\; then\; \}\; a\; \backslash in\; x.$

Let $\backslash mathcal\{D\}(A)$ denote the set of points of A with the subset ordering. $\backslash 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

• $\backslash mathcal\{D\}(\backslash mathcal\{I\}(D))\; \backslash cong\; D$
• $\backslash mathcal\{I\}(\backslash mathcal\{D\}(A))\; \backslash cong\; A$

where the second congruence is given by approximable mappings.

• Scott domain
• Domain theory

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

Category:Models of computation

Category:Domain theory