Logical deductive 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[edit]
A Scott information system, A, is an ordered triple
![{\displaystyle T{\mbox{ is a set of tokens (the basic units of information)}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e0dcc4b897789bf15519990392edc59c8e8029db)
![{\displaystyle Con\subseteq {\mathcal {P}}_{f}(T){\mbox{ the finite subsets of }}T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e2361258141521a468f070130038407865682d5d)
![{\displaystyle {\vdash }\subseteq (Con\setminus \lbrace \emptyset \rbrace )\times T}](https://wikimedia.org/api/rest_v1/media/math/render/svg/25ed03181c0a49f83eb2af5942c7e149bbee1bdc)
satisfying
![{\displaystyle {\mbox{If }}a\in X\in Con{\mbox{ then }}X\vdash a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/040ccb35c8e5d40f650cc0445feeb4e6cd7f5c24)
![{\displaystyle {\mbox{If }}X\vdash Y{\mbox{ and }}Y\vdash a{\mbox{, then }}X\vdash a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a0b9664573ad7abf0dff9a2a433d6016843c5257)
![{\displaystyle {\mbox{If }}X\vdash a{\mbox{ then }}X\cup \{a\}\in Con}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b75dd36c3c97bfd6358fa56f4d653da625de5ec6)
![{\displaystyle \forall a\in T:\{a\}\in Con}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8ee9a67c929d97965d4ded48fa01546590d7072a)
![{\displaystyle {\mbox{If }}X\in Con{\mbox{ and }}X^{\prime }\,\subseteq X{\mbox{ then }}X^{\prime }\in Con.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/12b633601ed489730f2aefab52e6d20528f1a727)
Here
means
Examples[edit]
Natural numbers[edit]
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:
![{\displaystyle T:=\mathbb {N} }](https://wikimedia.org/api/rest_v1/media/math/render/svg/9a275c84b8ecdffa2a275d9e2f96510551f55f72)
![{\displaystyle Con:=\{\emptyset \}\cup \{\{n\}\mid n\in \mathbb {N} \}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d3c910a3b8365286d2c5439d787252a37f82e713)
![{\displaystyle X\vdash a\iff a\in X.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f21a64c3a70725367fe31713f2a21815645ab16)
That is, the result can either be a natural number, represented by the singleton set
, or "infinite recursion," represented by
.
Of course, the same construction can be carried out with any other set instead of
.
Propositional calculus[edit]
The propositional calculus gives us a very simple Scott information system as follows:
![{\displaystyle T:=\{\phi \mid \phi {\mbox{ is satisfiable}}\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de280f0eed05d468489cce85f3bb9147b743bbc4)
![{\displaystyle Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ is consistent}}\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f33350019789ebda920702320476c20c8434a710)
![{\displaystyle X\vdash a\iff X\vdash a{\mbox{ in the propositional calculus}}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4d2d1e2914b00101a52083ab408390b7e6a8db7d)
Scott domains[edit]
Let D be a Scott domain. Then we may define an information system as follows
the set of compact elements of ![{\displaystyle D}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f34a0c600395e5d4345287e21fb26efd386990e6)
![{\displaystyle Con:=\{X\in {\mathcal {P}}_{f}(T)\mid X{\mbox{ has an upper bound}}\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bcc8d6ffbe75cb8cdcf54dfa8e8811d6e282edc1)
![{\displaystyle X\vdash d\iff d\sqsubseteq \bigsqcup X.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6cbdd8974c19a9520a73f7d11ac8669442ed9720)
Let
be the mapping that takes us from a Scott domain, D, to the information system defined above.
Information systems and Scott domains[edit]
Given an information system,
, we can build a Scott domain as follows.
- Definition:
is a point if and only if ![{\displaystyle {\mbox{If }}X\subseteq _{f}x{\mbox{ then }}X\in Con}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3f1b3cfbd54478b67505a780d550e517a81500ed)
![{\displaystyle {\mbox{If }}X\vdash a{\mbox{ and }}X\subseteq _{f}x{\mbox{ then }}a\in x.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dacada668103fc8dec8b3a1b961aef34fb8afe2e)
Let
denote the set of points of A with the subset ordering.
will be a countably based Scott domain when T is countable. In general, for any Scott domain D and information system A
![{\displaystyle {\mathcal {D}}({\mathcal {I}}(D))\cong D}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8bcb10a49cf19b57a4b4819283e8252f9018136d)
![{\displaystyle {\mathcal {I}}({\mathcal {D}}(A))\cong A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bf1f6206c0da2b6a1db86d38b41c65d5c6f31c21)
where the second congruence is given by approximable mappings.
See also[edit]
References[edit]
- Glynn Winskel: "The Formal Semantics of Programming Languages: An Introduction", MIT Press, 1993 (chapter 12)