Scott information system

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

Template:Short description 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,⊢)

  • T is a set of tokens (the basic units of information)
  • Con⊆𝒫f(T) the finite subsets of T
  • ⊢⊆(Con∖{∅})×T

satisfying

  1. If a∈X∈Con then X⊢a
  2. If X⊢Y and Y⊢a, then X⊢a
  3. If X⊢a then X∪{a}∈Con
  4. ∀a∈T:{a}∈Con
  5. If X∈Con and X′⊆X then X′∈Con.

Here X⊢Y means ∀a∈Y,X⊢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:=ℕ
  • Con:={∅}∪{{n}∣n∈ℕ}
  • X⊢a⟺a∈X.

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

Of course, the same construction can be carried out with any other set instead of ℕ.

Propositional calculus

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

  • T:={ϕ∣ϕ is satisfiable}
  • Con:={X∈𝒫f(T)∣X is consistent}
  • X⊢a⟺X⊢a in the propositional calculus.

Scott domains

Let D be a Scott domain. Then we may define an information system as follows

  • T:=D0 the set of compact elements of D
  • Con:={X∈𝒫f(T)∣X has an upper bound}
  • X⊢d⟺d⊑⨆X.

Let ℐ 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,⊢), we can build a Scott domain as follows.

  • Definition: x⊆T is a point if and only if
    • If X⊆fx then X∈Con
    • If X⊢a and X⊆fx then a∈x.

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

  • 𝒟(ℐ(D))≅D
  • ℐ(𝒟(A))≅A

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)