Example 6.2 (Scott 1981, PRG-19, §6) — C ≅ {{Λ}} + C + C

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture VI. This module formalizes the second domain equation of Example 6.2, for the system C of finite or infinite binary sequences (Example 4.4):

C ≅ {{Λ}} + C + C,

where {{Λ}} = 𝟙 is the one-point (unit) domain (Exercise 3.15). Presented over {0,1}*,

C = {Σ*} ∪ {{Λ}} ∪ {0X ∣ X ∈ C} ∪ {1X ∣ X ∈ C},

so a neighbourhood of C is the master Σ* (= cone []), the terminator {Λ} = {[]}, a 0-copy 0X = embBit false X, or a 1-copy 1X = embBit true X. These four shapes are exactly those of a three-way separated sum 𝟙 + C + C: a fresh basepoint, plus one 𝟙-copy (the lone {Λ}), plus two C-copies.

Crucially this is a genuine three-way sum: nesting the binary sum (𝟙 + (C + C)) would introduce a spurious extra bottom element (the inner sum's basepoint) with no counterpart in C. So we first build the three-way separated sum sum3 (mirroring Exercise 3.18), then exhibit the order-isomorphism ccEquiv : |C| ≃o |𝟙 + C + C|.

All data is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The three-way separated sum D₀ + D₁ + D₂.

Tokens are Option (α ⊕ β ⊕ γ): a fresh basepoint Λ = none below three disjoint tagged copies.

def Domain.Neighborhood.t0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) : Option (α ⊕ β ⊕ γ)

Left tag 0a = some (inl a).

Equations

• Domain.Neighborhood.t0 a = some (Sum.inl a)

def Domain.Neighborhood.t1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) : Option (α ⊕ β ⊕ γ)

Middle tag 1b = some (inr (inl b)).

Equations

• Domain.Neighborhood.t1 b = some (Sum.inr (Sum.inl b))

def Domain.Neighborhood.t2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) : Option (α ⊕ β ⊕ γ)

Right tag 2c = some (inr (inr c)).

Equations

• Domain.Neighborhood.t2 c = some (Sum.inr (Sum.inr c))

def Domain.Neighborhood.j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (X : Set α) : Set (Option (α ⊕ β ⊕ γ))

The tagged left copy 0X.

Equations

• Domain.Neighborhood.j0 X = {w : Option (α ⊕ β ⊕ γ) | ∃ (a : α), w = Domain.Neighborhood.t0 a ∧ a ∈ X}

def Domain.Neighborhood.j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (Y : Set β) : Set (Option (α ⊕ β ⊕ γ))

The tagged middle copy 1Y.

Equations

• Domain.Neighborhood.j1 Y = {w : Option (α ⊕ β ⊕ γ) | ∃ (b : β), w = Domain.Neighborhood.t1 b ∧ b ∈ Y}

def Domain.Neighborhood.j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (Z : Set γ) : Set (Option (α ⊕ β ⊕ γ))

The tagged right copy 2Z.

Equations

• Domain.Neighborhood.j2 Z = {w : Option (α ⊕ β ⊕ γ) | ∃ (c : γ), w = Domain.Neighborhood.t2 c ∧ c ∈ Z}

@[simp]

theorem Domain.Neighborhood.t0_mem_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {X : Set α} {a : α} : t0 a ∈ j0 X ↔ a ∈ X

@[simp]

theorem Domain.Neighborhood.t1_mem_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Y : Set β} {b : β} : t1 b ∈ j1 Y ↔ b ∈ Y

@[simp]

theorem Domain.Neighborhood.t2_mem_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Z : Set γ} {c : γ} : t2 c ∈ j2 Z ↔ c ∈ Z

@[simp]

theorem Domain.Neighborhood.none_not_mem_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {X : Set α} : none ∉ j0 X

@[simp]

theorem Domain.Neighborhood.none_not_mem_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Y : Set β} : none ∉ j1 Y

@[simp]

theorem Domain.Neighborhood.none_not_mem_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Z : Set γ} : none ∉ j2 Z

@[simp]

theorem Domain.Neighborhood.t1_not_mem_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {X : Set α} {b : β} : t1 b ∉ j0 X

@[simp]

theorem Domain.Neighborhood.t2_not_mem_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {X : Set α} {c : γ} : t2 c ∉ j0 X

@[simp]

theorem Domain.Neighborhood.t0_not_mem_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Y : Set β} {a : α} : t0 a ∉ j1 Y

@[simp]

theorem Domain.Neighborhood.t2_not_mem_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Y : Set β} {c : γ} : t2 c ∉ j1 Y

@[simp]

theorem Domain.Neighborhood.t0_not_mem_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Z : Set γ} {a : α} : t0 a ∉ j2 Z

@[simp]

theorem Domain.Neighborhood.t1_not_mem_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Z : Set γ} {b : β} : t1 b ∉ j2 Z

theorem Domain.Neighborhood.j0_inter_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (X X' : Set α) : j0 X ∩ j0 X' = j0 (X ∩ X')

theorem Domain.Neighborhood.j1_inter_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (Y Y' : Set β) : j1 Y ∩ j1 Y' = j1 (Y ∩ Y')

theorem Domain.Neighborhood.j2_inter_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (Z Z' : Set γ) : j2 Z ∩ j2 Z' = j2 (Z ∩ Z')

theorem Domain.Neighborhood.j0_inter_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (X : Set α) (Y : Set β) : j0 X ∩ j1 Y = ∅

theorem Domain.Neighborhood.j0_inter_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (X : Set α) (Z : Set γ) : j0 X ∩ j2 Z = ∅

theorem Domain.Neighborhood.j1_inter_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (Y : Set β) (Z : Set γ) : j1 Y ∩ j2 Z = ∅

theorem Domain.Neighborhood.j0_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {X : Set α} (hX : X.Nonempty) : (j0 X).Nonempty

theorem Domain.Neighborhood.j1_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Y : Set β} (hY : Y.Nonempty) : (j1 Y).Nonempty

theorem Domain.Neighborhood.j2_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Z : Set γ} (hZ : Z.Nonempty) : (j2 Z).Nonempty

theorem Domain.Neighborhood.j0_subset_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {X X' : Set α} : j0 X ⊆ j0 X' ↔ X ⊆ X'

theorem Domain.Neighborhood.j1_subset_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Y Y' : Set β} : j1 Y ⊆ j1 Y' ↔ Y ⊆ Y'

theorem Domain.Neighborhood.j2_subset_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Z Z' : Set γ} : j2 Z ⊆ j2 Z' ↔ Z ⊆ Z'

theorem Domain.Neighborhood.j0_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {X X' : Set α} (h : j0 X = j0 X') : X = X'

theorem Domain.Neighborhood.j1_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Y Y' : Set β} (h : j1 Y = j1 Y') : Y = Y'

theorem Domain.Neighborhood.j2_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Z Z' : Set γ} (h : j2 Z = j2 Z') : Z = Z'

def Domain.Neighborhood.master3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : Set (Option (α ⊕ β ⊕ γ))

The master neighbourhood of the three-way sum: {Λ} ∪ 0Δ₀ ∪ 1Δ₁ ∪ 2Δ₂.

Equations

• Domain.Neighborhood.master3 V₀ V₁ V₂ = insert none (Domain.Neighborhood.j0 V₀.master ∪ Domain.Neighborhood.j1 V₁.master ∪ Domain.Neighborhood.j2 V₂.master)

@[simp]

theorem Domain.Neighborhood.none_mem_master3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} : none ∈ master3 V₀ V₁ V₂

theorem Domain.Neighborhood.j0_subset_master3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {X : Set α} (hX : V₀.mem X) : j0 X ⊆ master3 V₀ V₁ V₂

theorem Domain.Neighborhood.j1_subset_master3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {Y : Set β} (hY : V₁.mem Y) : j1 Y ⊆ master3 V₀ V₁ V₂

theorem Domain.Neighborhood.j2_subset_master3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {Z : Set γ} (hZ : V₂.mem Z) : j2 Z ⊆ master3 V₀ V₁ V₂

theorem Domain.Neighborhood.master3_inter_j0 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {X : Set α} (hX : V₀.mem X) : master3 V₀ V₁ V₂ ∩ j0 X = j0 X

theorem Domain.Neighborhood.master3_inter_j1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {Y : Set β} (hY : V₁.mem Y) : master3 V₀ V₁ V₂ ∩ j1 Y = j1 Y

theorem Domain.Neighborhood.master3_inter_j2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {Z : Set γ} (hZ : V₂.mem Z) : master3 V₀ V₁ V₂ ∩ j2 Z = j2 Z

theorem Domain.Neighborhood.eq_master3_of_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {W : Set (Option (α ⊕ β ⊕ γ))} (hsub : master3 V₀ V₁ V₂ ⊆ W) (hsub' : W ⊆ master3 V₀ V₁ V₂) : W = master3 V₀ V₁ V₂

def Domain.Neighborhood.sum3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) (h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty) (h₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty) : NeighborhoodSystem (Option (α ⊕ β ⊕ γ))

Example 6.2 — the three-way separated sum D₀ + D₁ + D₂ over {Λ} ∪ 0Δ₀ ∪ 1Δ₁ ∪ 2Δ₂, under the standing assumption that no neighbourhood of any factor is empty.

Equations

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

The domain equation C ≅ 𝟙 + C + C.

theorem Domain.Neighborhood.Example62C.unitSys_nonempty (X : Set Unit) : unitSys.mem X → X.Nonempty

𝟙 is positive: its single neighbourhood univ (over the inhabited Unit) is nonempty.

theorem Domain.Neighborhood.Example62C.C_nonempty (X : Set ExampleB.Str) : Example44.C.mem X → X.Nonempty

Scott's standing assumption ∅ ∉ C: every neighbourhood of C is nonempty.

theorem Domain.Neighborhood.Example62C.embBit_singleton (b : Bool) (σ : ExampleB.Str) : Example62.embBit b {σ} = {b :: σ}

b{σ} = {bσ}: prepending a bit to a singleton.

theorem Domain.Neighborhood.Example62C.memC_embBit (b : Bool) {X : Set ExampleB.Str} (hX : Example44.C.mem X) : Example44.C.mem (Example62.embBit b X)

Prepending a bit lands back in C.

theorem Domain.Neighborhood.Example62C.memC_cases {W : Set ExampleB.Str} (hW : Example44.C.mem W) : W = Set.univ ∨ W = {[]} ∨ (∃ (X : Set ExampleB.Str), Example44.C.mem X ∧ W = Example62.embBit false X) ∨ ∃ (Y : Set ExampleB.Str), Example44.C.mem Y ∧ W = Example62.embBit true Y

Example 6.2 — the shape of a C-neighbourhood. Every neighbourhood of C is the master Σ* = cone [], the terminator {Λ} = {[]}, a 0-copy 0X with X ∈ C, or a 1-copy 1X.

theorem Domain.Neighborhood.Example62C.memC_embBit_inv {b : Bool} {W : Set ExampleB.Str} (h : Example44.C.mem (Example62.embBit b W)) : Example44.C.mem W

If bW ∈ C then W ∈ C.

theorem Domain.Neighborhood.Example62C.singleton_nil_inter_embBit (b : Bool) (X : Set ExampleB.Str) : {[]} ∩ Example62.embBit b X = ∅

theorem Domain.Neighborhood.Example62C.singleton_nil_ne_univ : {[]} ≠ Set.univ

theorem Domain.Neighborhood.Example62C.singleton_nil_ne_embBit (b : Bool) (X : Set ExampleB.Str) : {[]} ≠ Example62.embBit b X

@[reducible, inline]

abbrev Domain.Neighborhood.Example62C.CC : NeighborhoodSystem (Option (Unit ⊕ ExampleB.Str ⊕ ExampleB.Str))

The right-hand side of the domain equation: the three-way sum 𝟙 + C + C.

Equations

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

theorem Domain.Neighborhood.Example62C.sum3_mem_j1_inv {X : Set ExampleB.Str} (h : CC.mem (j1 X)) : Example44.C.mem X

theorem Domain.Neighborhood.Example62C.sum3_mem_j2_inv {Y : Set ExampleB.Str} (h : CC.mem (j2 Y)) : Example44.C.mem Y

theorem Domain.Neighborhood.Example62C.sum3_mem_nonempty {W : Set (Option (Unit ⊕ ExampleB.Str ⊕ ExampleB.Str))} (h : CC.mem W) : W.Nonempty

The forward half toCC : |C| → |𝟙 + C + C|.

def Domain.Neighborhood.Example62C.toCC (x : Example44.C.Element) : CC.Element

Example 6.2 — forward half of C ≅ 𝟙 + C + C.

Equations

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

@[simp]

theorem Domain.Neighborhood.Example62C.toCC_mem_j0 {x : Example44.C.Element} : (toCC x).mem (j0 Set.univ) ↔ x.mem {[]}

theorem Domain.Neighborhood.Example62C.toCC_mem_j1 {x : Example44.C.Element} {X : Set ExampleB.Str} (hX : Example44.C.mem X) : (toCC x).mem (j1 X) ↔ x.mem (Example62.embBit false X)

theorem Domain.Neighborhood.Example62C.toCC_mem_j2 {x : Example44.C.Element} {Y : Set ExampleB.Str} (hY : Example44.C.mem Y) : (toCC x).mem (j2 Y) ↔ x.mem (Example62.embBit true Y)

The inverse half fromCC : |𝟙 + C + C| → |C|.

def Domain.Neighborhood.Example62C.fromCC (s : CC.Element) : Example44.C.Element

Example 6.2 — inverse half of C ≅ 𝟙 + C + C.

Equations

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

@[simp]

theorem Domain.Neighborhood.Example62C.fromCC_mem_nil {s : CC.Element} : (fromCC s).mem {[]} ↔ s.mem (j0 Set.univ)

theorem Domain.Neighborhood.Example62C.fromCC_mem_embF {s : CC.Element} {X : Set ExampleB.Str} (hX : Example44.C.mem X) : (fromCC s).mem (Example62.embBit false X) ↔ s.mem (j1 X)

theorem Domain.Neighborhood.Example62C.fromCC_mem_embT {s : CC.Element} {Y : Set ExampleB.Str} (hY : Example44.C.mem Y) : (fromCC s).mem (Example62.embBit true Y) ↔ s.mem (j2 Y)

The two halves are mutually inverse.

theorem Domain.Neighborhood.Example62C.fromCC_toCC (x : Example44.C.Element) : fromCC (toCC x) = x

theorem Domain.Neighborhood.Example62C.toCC_fromCC (s : CC.Element) : toCC (fromCC s) = s

The domain equation C ≅ 𝟙 + C + C.

def Domain.Neighborhood.Example62C.ccEquiv : Example44.C.Element ≃o CC.Element

Example 6.2 (Scott 1981, PRG-19) — the isomorphism |C| ≃o |𝟙 + C + C|.

Equations

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

theorem Domain.Neighborhood.Example62C.C_domain_equation : Example44.C ≅ᴰ sum3 unitSys Example44.C Example44.C unitSys_nonempty C_nonempty C_nonempty

Example 6.2 (Scott 1981, PRG-19) — the domain equation C ≅ {{Λ}} + C + C. Scott's domain C of finite-or-infinite binary sequences is, as a domain, isomorphic to the three-way separated sum 𝟙 + C + C: a sequence is bottom, the finished empty sequence Λ (the 𝟙 summand), or begins with 0 or 1 (the two C summands).