Scott Information Systems

Following Dana Scott, "Domains for Denotational Semantics" (ICALP 1982) and the compact presentation in Glynn Winskel, The Formal Semantics of Programming Languages, Chapter 8.

Following Scott's Definition 2.1, an information system is a structure (P, Δ, Con, ⊢) where

• P is a set of data objects / propositions (our token type α);
• Δ ∈ P is a distinguished least informative object (here the field bot);
• Con is a set of finite subsets of P, the consistent sets; and
• ⊢ (entailment, here Ent) relates a finite set to a token it forces.

Scott's six axioms (Def. 2.1) are, for finite u, v ⊆ P and X ∈ P:

• (i) u ∈ Con whenever u ⊆ v ∈ Con — con_subset
• (ii) {X} ∈ Con — con_sing
• (iii) u ∪ {X} ∈ Con whenever u ⊢ X — ent_con
• (iv) u ⊢ Δ — ent_bot
• (v) u ⊢ X whenever X ∈ u — ent_refl
• (vi) if v ⊢ Y for all Y ∈ u and u ⊢ X then v ⊢ X — ent_trans

The domain determined by an information system is the poset of its elements (a.k.a. ideals): sets of tokens that are consistent on every finite subset and closed under entailment, ordered by inclusion. This file sets up the structure, the notion of element, and the partial order; later files build the function, product, and sum spaces.

This is the 1982 presentation; the development is kept choice-free (constructive), matching Scott's emphasis on the constructive nature of the definitions.

structure InfoSys (α : Type u_1) [DecidableEq α] : Type u_1

A Scott information system on a type of tokens α, following Scott's Definition 2.1 in "Domains for Denotational Semantics" (ICALP 1982).

DecidableEq α is required so that finite token sets support union (X ∪ {a}) and the other Finset operations the axioms mention.

• bot : α

  The distinguished least-informative object Δ.

• Con : Set (Finset α)

  The consistent finite sets of tokens.

• Ent : Finset α → α → Prop

  Entailment: Ent u a means the consistent set u forces the token a.

• con_subset {u v : Finset α} : u ∈ self.Con → v ⊆ u → v ∈ self.Con

  (i) Consistency is downward closed under ⊆.

• con_sing (a : α) : {a} ∈ self.Con

  (ii) Every singleton is consistent.

• ent_con {u : Finset α} {a : α} : self.Ent u a → insert a u ∈ self.Con

  (iii) A set entailing a stays consistent when a is added. Scott writes this as u ∪ {a} ∈ Con; we use the definitionally identical insert a u, because mathlib's Finset union instance (unlike insert) depends on Classical.choice, which would break the constructive development.

• ent_bot {u : Finset α} : u ∈ self.Con → self.Ent u self.bot

  (iv) The least token Δ is entailed by every consistent set.

• ent_refl {u : Finset α} {a : α} : u ∈ self.Con → a ∈ u → self.Ent u a

  (v) Entailment is reflexive on members of a consistent set.

• ent_trans {u v : Finset α} {c : α} : v ∈ self.Con → u ∈ self.Con → (∀ y ∈ u, self.Ent v y) → self.Ent u c → self.Ent v c

  (vi) Entailment is transitive (cut): if a consistent v entails every member of a consistent u, and u ⊢ c, then v ⊢ c.

structure InfoSys.Element {α : Type u_1} [DecidableEq α] (sys : InfoSys α) : Type u_1

An element (ideal) of the domain: a set of tokens that is consistent on every finite subset and closed under entailment.

• carrier : Set α

  The underlying set of tokens.

• consistent (Y : Finset α) : ↑Y ⊆ self.carrier → Y ∈ sys.Con

  Every finite subset of the element is consistent.

• closed (Y : Finset α) (a : α) : ↑Y ⊆ self.carrier → sys.Ent Y a → a ∈ self.carrier

  The element is closed under entailment.

@[implicit_reducible]

instance InfoSys.instPartialOrderElement {α : Type u_1} [DecidableEq α] (sys : InfoSys α) : PartialOrder sys.Element

Elements are ordered by inclusion of their carriers; this is the Scott ordering.

Equations

• sys.instPartialOrderElement = { le := fun (x y : sys.Element) => x.carrier ⊆ y.carrier, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }