Example 6.1 (Scott 1981, PRG-19, §6) — the tree algebra D^§ and the domain

equation D^§ ≅ D + (D^§ × D^§)

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture VI, Introduction to domain equations. Starting from a fixed domain D (a neighbourhood system over Δ) Scott iterates the product D × D indefinitely and collects all the iterates into a single domain D^§, the tree algebra over D. The construction:

• the tokens of D^§ live in Γ = {1,2}* 0 Δ — a finite {1,2}-path (here a List Bool, true = 1, false = 2) followed by a separator 0 and a D-token in Δ. We model this as List Bool × α with the master neighbourhood Γ = {t | t.2 ∈ Δ};
• the neighbourhoods of D^§ are the least family containing (i) Γ, (ii) 0X = {([], a) ∣ a ∈ X} for X ∈ 𝒟, and (iii) 1P ∪ 2Q for P, Q ∈ 𝒟^§. This is the inductive predicate MemS.

The heart of the example is Scott's verification that D^§ is a neighbourhood system: closure under consistent intersection, proved by induction on the way X was put into D^§, using the standing assumption ∅ ∉ 𝒟 (passed as hD : ∀ X, 𝒟.mem X → X.Nonempty). The pay-off is the domain equation

D^§ ≅ D + (D^§ × D^§),

formalized as the order-isomorphism dsharpEquiv : (Dsharp D hD).Element ≃o (sum D (prod …) …).Element, i.e. Dsharp D hD ≅ᴰ sum D (prod (Dsharp D hD) (Dsharp D hD)) ….

We use the project's + (sum, Exercise 3.18) and × (prod, Definition 3.1). All data is choice-free (#print axioms ⊆ {propext, Quot.sound}).

Token embeddings 0X, 1P, 2Q and the master Γ.

def Domain.Neighborhood.Example61.embZero {α : Type u_1} (X : Set α) : Set (List Bool × α)

0X = {([], a) ∣ a ∈ X}: the 0-tagged copy of a D-neighbourhood X (empty {1,2}-path).

Equations

• Domain.Neighborhood.Example61.embZero X = {t : List Bool × α | t.1 = [] ∧ t.2 ∈ X}

def Domain.Neighborhood.Example61.embL {α : Type u_1} (P : Set (List Bool × α)) : Set (List Bool × α)

1P = {(1::p, a) ∣ (p, a) ∈ P}: the 1-prefixed copy of a D^§-neighbourhood P.

Equations

• Domain.Neighborhood.Example61.embL P = {t : List Bool × α | ∃ (p' : List Bool), t.1 = true :: p' ∧ (p', t.2) ∈ P}

def Domain.Neighborhood.Example61.embR {α : Type u_1} (Q : Set (List Bool × α)) : Set (List Bool × α)

2Q = {(2::q, a) ∣ (q, a) ∈ Q}: the 2-prefixed copy of a D^§-neighbourhood Q.

Equations

• Domain.Neighborhood.Example61.embR Q = {t : List Bool × α | ∃ (q' : List Bool), t.1 = false :: q' ∧ (q', t.2) ∈ Q}

def Domain.Neighborhood.Example61.embPair {α : Type u_1} (P Q : Set (List Bool × α)) : Set (List Bool × α)

1P ∪ 2Q: the product-style neighbourhood of D^§.

Equations

• Domain.Neighborhood.Example61.embPair P Q = Domain.Neighborhood.Example61.embL P ∪ Domain.Neighborhood.Example61.embR Q

def Domain.Neighborhood.Example61.Gamma {α : Type u_1} (D : NeighborhoodSystem α) : Set (List Bool × α)

The master neighbourhood Γ = {1,2}* 0 Δ of D^§: any path, D-token in Δ.

Equations

• Domain.Neighborhood.Example61.Gamma D = {t : List Bool × α | t.2 ∈ D.master}

@[simp]

theorem Domain.Neighborhood.Example61.mem_embZero {α : Type u_1} {X : Set α} {p : List Bool} {a : α} : (p, a) ∈ embZero X ↔ p = [] ∧ a ∈ X

@[simp]

theorem Domain.Neighborhood.Example61.mem_embL {α : Type u_1} {P : Set (List Bool × α)} {p : List Bool} {a : α} : (p, a) ∈ embL P ↔ ∃ (p' : List Bool), p = true :: p' ∧ (p', a) ∈ P

@[simp]

theorem Domain.Neighborhood.Example61.mem_embR {α : Type u_1} {Q : Set (List Bool × α)} {p : List Bool} {a : α} : (p, a) ∈ embR Q ↔ ∃ (q' : List Bool), p = false :: q' ∧ (q', a) ∈ Q

@[simp]

theorem Domain.Neighborhood.Example61.mem_embPair {α : Type u_1} {P Q : Set (List Bool × α)} {p : List Bool} {a : α} : (p, a) ∈ embPair P Q ↔ (∃ (p' : List Bool), p = true :: p' ∧ (p', a) ∈ P) ∨ ∃ (q' : List Bool), p = false :: q' ∧ (q', a) ∈ Q

@[simp]

theorem Domain.Neighborhood.Example61.mem_Gamma {α : Type u_1} {D : NeighborhoodSystem α} {p : List Bool} {a : α} : (p, a) ∈ Gamma D ↔ a ∈ D.master

Intersection identities.

theorem Domain.Neighborhood.Example61.embZero_inter {α : Type u_1} (X X' : Set α) : embZero X ∩ embZero X' = embZero (X ∩ X')

theorem Domain.Neighborhood.Example61.embPair_inter {α : Type u_1} (P Q P' Q' : Set (List Bool × α)) : embPair P Q ∩ embPair P' Q' = embPair (P ∩ P') (Q ∩ Q')

theorem Domain.Neighborhood.Example61.embZero_inter_embPair {α : Type u_1} (X : Set α) (P Q : Set (List Bool × α)) : embZero X ∩ embPair P Q = ∅

Subset / injectivity.

theorem Domain.Neighborhood.Example61.embZero_subset {α : Type u_1} {X X' : Set α} : embZero X ⊆ embZero X' ↔ X ⊆ X'

theorem Domain.Neighborhood.Example61.embPair_subset {α : Type u_1} {P Q P' Q' : Set (List Bool × α)} : embPair P Q ⊆ embPair P' Q' ↔ P ⊆ P' ∧ Q ⊆ Q'

theorem Domain.Neighborhood.Example61.embZero_injective {α : Type u_1} {X X' : Set α} (h : embZero X = embZero X') : X = X'

theorem Domain.Neighborhood.Example61.embPair_injective {α : Type u_1} {P Q P' Q' : Set (List Bool × α)} (h : embPair P Q = embPair P' Q') : P = P' ∧ Q = Q'

Nonemptiness and ⊆ Γ.

theorem Domain.Neighborhood.Example61.embZero_nonempty {α : Type u_1} {X : Set α} (hX : X.Nonempty) : (embZero X).Nonempty

theorem Domain.Neighborhood.Example61.embPair_nonempty {α : Type u_1} {P Q : Set (List Bool × α)} (hP : P.Nonempty) : (embPair P Q).Nonempty

theorem Domain.Neighborhood.Example61.embZero_subset_Gamma {α : Type u_1} {D : NeighborhoodSystem α} {X : Set α} (hX : D.mem X) : embZero X ⊆ Gamma D

theorem Domain.Neighborhood.Example61.embPair_subset_Gamma {α : Type u_1} {D : NeighborhoodSystem α} {P Q : Set (List Bool × α)} (hP : P ⊆ Gamma D) (hQ : Q ⊆ Gamma D) : embPair P Q ⊆ Gamma D

theorem Domain.Neighborhood.Example61.Gamma_nonempty {α : Type u_1} {D : NeighborhoodSystem α} (hD : ∀ (X : Set α), D.mem X → X.Nonempty) : (Gamma D).Nonempty

The neighbourhood system D^§.

inductive Domain.Neighborhood.Example61.MemS {α : Type u_1} (D : NeighborhoodSystem α) : Set (List Bool × α) → Prop

Example 6.1 (Scott 1981, PRG-19). The neighbourhoods of D^§, defined inductively as the least family of subsets of Γ containing (i) Γ, (ii) 0X for X ∈ 𝒟, and (iii) 1P ∪ 2Q whenever it already contains P and Q. This is Scott's fixed-point family 𝒟^§ = {Γ} ∪ {0X ∣ X ∈ 𝒟} ∪ {1P ∪ 2Q ∣ P, Q ∈ 𝒟^§}.

• gamma {α : Type u_1} {D : NeighborhoodSystem α} : MemS D (Gamma D)
• zero {α : Type u_1} {D : NeighborhoodSystem α} {X : Set α} : D.mem X → MemS D (embZero X)
• pair {α : Type u_1} {D : NeighborhoodSystem α} {P Q : Set (List Bool × α)} : MemS D P → MemS D Q → MemS D (embPair P Q)

theorem Domain.Neighborhood.Example61.memS_subset_gamma {α : Type u_1} {D : NeighborhoodSystem α} {W : Set (List Bool × α)} (hW : MemS D W) : W ⊆ Gamma D

Every neighbourhood of D^§ is a subset of the master Γ (Scott's 𝒟^§ ⊆ 𝒫(Γ)).

theorem Domain.Neighborhood.Example61.memS_nonempty {α : Type u_1} {D : NeighborhoodSystem α} (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {W : Set (List Bool × α)} (hW : MemS D W) : W.Nonempty

Under Scott's standing assumption ∅ ∉ 𝒟, no neighbourhood of D^§ is empty.

theorem Domain.Neighborhood.Example61.memS_inter {α : Type u_1} {D : NeighborhoodSystem α} (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {X : Set (List Bool × α)} : MemS D X → ∀ {Y : Set (List Bool × α)}, MemS D Y → ∀ {Z : Set (List Bool × α)}, MemS D Z → Z ⊆ X ∩ Y → MemS D (X ∩ Y)

Example 6.1 — closure under consistent intersection. Scott's central verification, "by induction on the number of steps required to put X and Y into 𝒟^§". The cross cases (0A ∩ (1P∪2Q) = ∅, etc.) are discharged because the consistency witness Z is non-empty (memS_nonempty); the 0A ∩ 0B case uses 𝒟's own closure; the (1P∪2Q) ∩ (1P'∪2Q') case recurses on P, P' and Q, Q'.

def Domain.Neighborhood.Example61.Dsharp {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) : NeighborhoodSystem (List Bool × α)

Example 6.1 (Scott 1981, PRG-19). The tree algebra D^§: a neighbourhood system over Γ = {1,2}* 0 Δ, under the standing assumption ∅ ∉ 𝒟 (hD).

Equations

• Domain.Neighborhood.Example61.Dsharp D hD = { mem := Domain.Neighborhood.Example61.MemS D, master := Domain.Neighborhood.Example61.Gamma D, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

@[simp]

theorem Domain.Neighborhood.Example61.Dsharp_mem {α : Type u_1} {D : NeighborhoodSystem α} {hD : ∀ (X : Set α), D.mem X → X.Nonempty} {W : Set (List Bool × α)} : (Dsharp D hD).mem W ↔ MemS D W

@[simp]

theorem Domain.Neighborhood.Example61.Dsharp_master {α : Type u_1} {D : NeighborhoodSystem α} {hD : ∀ (X : Set α), D.mem X → X.Nonempty} : (Dsharp D hD).master = Gamma D

Inversion lemmas for D^§-neighbourhoods.

Because the three neighbourhood shapes Γ, 0X, 1P ∪ 2Q are mutually distinguishable (by the shape of their {1,2}-paths, using non-emptiness), a D^§-neighbourhood of a given shape can only have arisen from the matching constructor.

theorem Domain.Neighborhood.Example61.memS_embZero_inv {α : Type u_1} {D : NeighborhoodSystem α} (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {X : Set α} (h : MemS D (embZero X)) : D.mem X

theorem Domain.Neighborhood.Example61.memS_embPair_inv {α : Type u_1} {D : NeighborhoodSystem α} (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {P Q : Set (List Bool × α)} (h : MemS D (embPair P Q)) : MemS D P ∧ MemS D Q

The domain equation D^§ ≅ D + (D^§ × D^§).

theorem Domain.Neighborhood.Example61.prod_dsharp_nonempty {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (V : Set (List Bool × α ⊕ List Bool × α)) : (prod (Dsharp D hD) (Dsharp D hD)).mem V → V.Nonempty

No neighbourhood of D^§ × D^§ is empty (needed to form the sum D + (D^§ × D^§)).

def Domain.Neighborhood.Example61.sumSys {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) : NeighborhoodSystem (Option (α ⊕ List Bool × α ⊕ List Bool × α))

The right-hand side of Scott's domain equation: the sum system D + (D^§ × D^§).

Equations

• Domain.Neighborhood.Example61.sumSys D hD = Domain.Neighborhood.sum D (Domain.Neighborhood.prod (Domain.Neighborhood.Example61.Dsharp D hD) (Domain.Neighborhood.Example61.Dsharp D hD)) hD ⋯

theorem Domain.Neighborhood.Example61.sum_mem_inj₀_inv {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {X : Set α} (h : (sumSys D hD).mem (inj₀ X)) : D.mem X

A sum-neighbourhood of the form 0X arises only from the left factor, so X ∈ 𝒟.

theorem Domain.Neighborhood.Example61.sum_mem_inj₁_inv {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {V : Set (List Bool × α ⊕ List Bool × α)} (h : (sumSys D hD).mem (inj₁ V)) : (prod (Dsharp D hD) (Dsharp D hD)).mem V

A sum-neighbourhood of the form 1V arises only from the right factor, so V ∈ 𝒟^§ × 𝒟^§.

theorem Domain.Neighborhood.Example61.sumSys_mem_nonempty {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {W : Set (Option (α ⊕ List Bool × α ⊕ List Bool × α))} (h : (sumSys D hD).mem W) : W.Nonempty

No neighbourhood of the sum D + (D^§ × D^§) is empty.

def Domain.Neighborhood.Example61.toS {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (z : (Dsharp D hD).Element) : (sumSys D hD).Element

Example 6.1 — the forward half of the domain equation. Sends an element z of D^§ to an element of D + (D^§ × D^§), recording for each branch which 0X/1V neighbourhoods z reaches: 0X ∈ toS z ↔ embZero X ∈ z and 1(P∪Q) ∈ toS z ↔ (1P∪2Q) ∈ z.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.Example61.toS_mem_inj₀ {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {z : (Dsharp D hD).Element} {X : Set α} (hX : D.mem X) : (toS D hD z).mem (inj₀ X) ↔ z.mem (embZero X)

@[simp]

theorem Domain.Neighborhood.Example61.toS_mem_inj₁ {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {z : (Dsharp D hD).Element} {P Q : Set (List Bool × α)} (hP : MemS D P) (hQ : MemS D Q) : (toS D hD z).mem (inj₁ (prodNbhd P Q)) ↔ z.mem (embPair P Q)

def Domain.Neighborhood.Example61.fromS {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (s : (sumSys D hD).Element) : (Dsharp D hD).Element

Example 6.1 — the inverse half of the domain equation. Sends an element s of D + (D^§ × D^§) back to an element of D^§.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Example61.embZero_ne_Gamma {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (X : Set α) : embZero X ≠ Gamma D

theorem Domain.Neighborhood.Example61.embPair_ne_Gamma {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (P Q : Set (List Bool × α)) : embPair P Q ≠ Gamma D

theorem Domain.Neighborhood.Example61.embZero_ne_embPair {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {X : Set α} (hX : D.mem X) (P Q : Set (List Bool × α)) : embZero X ≠ embPair P Q

@[simp]

theorem Domain.Neighborhood.Example61.fromS_mem_embZero {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {s : (sumSys D hD).Element} {X : Set α} (hX : D.mem X) : (fromS D hD s).mem (embZero X) ↔ s.mem (inj₀ X)

@[simp]

theorem Domain.Neighborhood.Example61.fromS_mem_embPair {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {s : (sumSys D hD).Element} {P Q : Set (List Bool × α)} (hP : MemS D P) (hQ : MemS D Q) : (fromS D hD s).mem (embPair P Q) ↔ s.mem (inj₁ (prodNbhd P Q))

theorem Domain.Neighborhood.Example61.fromS_toS {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (z : (Dsharp D hD).Element) : fromS D hD (toS D hD z) = z

fromS ∘ toS = id.

theorem Domain.Neighborhood.Example61.toS_fromS {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (s : (sumSys D hD).Element) : toS D hD (fromS D hD s) = s

toS ∘ fromS = id.

def Domain.Neighborhood.Example61.dsharpEquiv {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) : (Dsharp D hD).Element ≃o (sumSys D hD).Element

Example 6.1 (Scott 1981, PRG-19) — the domain equation, as an order-isomorphism. |D^§| ≃o |D + (D^§ × D^§)|.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Example61.dsharp_domain_equation {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) : Dsharp D hD ≅ᴰ sum D (prod (Dsharp D hD) (Dsharp D hD)) hD ⋯

Example 6.1 (Scott 1981, PRG-19) — the domain equation D^§ ≅ D + (D^§ × D^§). The tree algebra D^§ is, as a domain, isomorphic to D + (D^§ × D^§) — Scott's defining isomorphism, "as can be seen by reference to the equation for D^§ and the definitions of + and ×".

The isomorphic injections x ↦ x^§ and x, y ↦ ⟨x, y⟩.

Scott exhibits the finite-element structure of |D^§| through two one-one (information-preserving) injections: λx. x^§ : D → D^§ and λx, y. ⟨x, y⟩ : D^§ × D^§ → D^§, with bottom ⊥ = {Γ} (the system's own bot).

def Domain.Neighborhood.Example61.inSharp {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (x : D.Element) : (Dsharp D hD).Element

Scott's injection x^§ = {Γ} ∪ {0X ∣ X ∈ x} of a D-element into D^§.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Example61.inSharp_le_iff {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {x x' : D.Element} : inSharp D hD x ≤ inSharp D hD x' ↔ x ≤ x'

Example 6.1 (Scott 1981, PRG-19). λx. x^§ is an isomorphic injection: x^§ ⊑ x'^§ ↔ x ⊑ x' (in particular one-one).

def Domain.Neighborhood.Example61.pairSharp {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) (x y : (Dsharp D hD).Element) : (Dsharp D hD).Element

Scott's pairing ⟨x, y⟩ = {Γ} ∪ {1P ∪ 2Q ∣ P ∈ x, Q ∈ y} of two D^§-elements.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Example61.pairSharp_le_iff {α : Type u_1} (D : NeighborhoodSystem α) (hD : ∀ (X : Set α), D.mem X → X.Nonempty) {x x' y y' : (Dsharp D hD).Element} : pairSharp D hD x y ≤ pairSharp D hD x' y' ↔ x ≤ x' ∧ y ≤ y'

Example 6.1 (Scott 1981, PRG-19). λx, y. ⟨x, y⟩ is an isomorphic injection: ⟨x, y⟩ ⊑ ⟨x', y'⟩ ↔ x ⊑ x' ∧ y ⊑ y'.