Example 6.2 (Scott 1981, PRG-19, §6) — B and C as solutions of domain

equations

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture VI, Introduction to domain equations. Scott observes that the staple examples B (binary sequences, Example 1.B) and C (finite-or-infinite binary sequences, Example 4.4) satisfy domain equations:

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

where, "if we liked", both systems can be presented over {0,1}* as the least families

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

This module formalizes the B ≅ B + B half. (See Example62C.lean for C's three-way equation C ≅ 𝟙 + C + C.)

The point of the equation is that a neighbourhood of B is either the master Σ* (= cone []), a 0-prefixed copy 0X (= embBit false X), or a 1-prefixed copy 1X (= embBit true X) — exactly the three shapes that build the sum B + B (Exercise 3.18): the fresh basepoint, the left copy 0X, and the right copy 1Y. We exhibit the order-isomorphism bbEquiv : |B| ≃o |B + B| directly from the filter maps toBB (forward) / fromBB (inverse), mirroring Example61.dsharpEquiv.

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

Prepending a single bit: bX = {bw' ∣ w' ∈ X}.

def Domain.Neighborhood.Example62.embBit (b : Bool) (X : Set ExampleB.Str) : Set ExampleB.Str

bX = {b :: w' ∣ w' ∈ X}: the b-prefixed copy of a neighbourhood X (Scott's 0X for b = false and 1X for b = true).

Equations

• Domain.Neighborhood.Example62.embBit b X = {w : Domain.Neighborhood.ExampleB.Str | ∃ (w' : List Bool), w = b :: w' ∧ w' ∈ X}

@[simp]

theorem Domain.Neighborhood.Example62.mem_embBit {b : Bool} {X : Set ExampleB.Str} {w : ExampleB.Str} : w ∈ embBit b X ↔ ∃ (w' : List Bool), w = b :: w' ∧ w' ∈ X

theorem Domain.Neighborhood.Example62.embBit_eq_prepend (b : Bool) (X : Set ExampleB.Str) : embBit b X = ExampleB.prepend [b] X

bX = b·X is exactly the single-bit prepend of Example 1.B.

theorem Domain.Neighborhood.Example62.embBit_cone (b : Bool) (σ : ExampleB.Str) : embBit b (ExampleB.cone σ) = ExampleB.cone (b :: σ)

b(σΣ*) = (bσ)Σ*: prepending a bit to a cone gives the cone of the longer prefix.

theorem Domain.Neighborhood.Example62.memB_embBit (b : Bool) {X : Set ExampleB.Str} (hX : ExampleB.B.mem X) : ExampleB.B.mem (embBit b X)

Prepending a bit lands back in B.

theorem Domain.Neighborhood.Example62.nil_not_mem_embBit {b : Bool} {X : Set ExampleB.Str} : ¬[] ∈ embBit b X

theorem Domain.Neighborhood.Example62.embBit_ne_univ (b : Bool) (X : Set ExampleB.Str) : embBit b X ≠ Set.univ

theorem Domain.Neighborhood.Example62.embBit_inter (b : Bool) (X X' : Set ExampleB.Str) : embBit b X ∩ embBit b X' = embBit b (X ∩ X')

theorem Domain.Neighborhood.Example62.embBit_inter_ne {b b' : Bool} (h : b ≠ b') (X Y : Set ExampleB.Str) : embBit b X ∩ embBit b' Y = ∅

theorem Domain.Neighborhood.Example62.embBit_subset {b : Bool} {X X' : Set ExampleB.Str} : embBit b X ⊆ embBit b X' ↔ X ⊆ X'

theorem Domain.Neighborhood.Example62.embBit_injective {b : Bool} {X X' : Set ExampleB.Str} (h : embBit b X = embBit b X') : X = X'

theorem Domain.Neighborhood.Example62.embBit_nonempty {b : Bool} {X : Set ExampleB.Str} (hX : X.Nonempty) : (embBit b X).Nonempty

theorem Domain.Neighborhood.Example62.memB_embBit_inv {b : Bool} {W : Set ExampleB.Str} (h : ExampleB.B.mem (embBit b W)) : ExampleB.B.mem W

If bW ∈ B then W ∈ B: a b-prefixed neighbourhood that lands in B must be b·(cone w'), so W = cone w'.

theorem Domain.Neighborhood.Example62.embBit_ne {b b' : Bool} (h : b ≠ b') {X Y : Set ExampleB.Str} (hX : X.Nonempty) : embBit b X ≠ embBit b' Y

B is positive (no empty neighbourhood) and its neighbourhood-shape

classification.

theorem Domain.Neighborhood.Example62.B_nonempty (X : Set ExampleB.Str) : ExampleB.B.mem X → X.Nonempty

Scott's standing assumption ∅ ∉ B: every neighbourhood of B is nonempty (cones contain their generating prefix).

theorem Domain.Neighborhood.Example62.memB_cases {W : Set ExampleB.Str} (hW : ExampleB.B.mem W) : W = Set.univ ∨ (∃ (X : Set ExampleB.Str), ExampleB.B.mem X ∧ W = embBit false X) ∨ ∃ (Y : Set ExampleB.Str), ExampleB.B.mem Y ∧ W = embBit true Y

Example 6.2 — the shape of a B-neighbourhood. Every neighbourhood of B is either the master Σ* = cone [], a 0-copy 0X with X ∈ B, or a 1-copy 1X with X ∈ B.

The sum target B + B and its inversion lemmas.

@[reducible, inline]

abbrev Domain.Neighborhood.Example62.BB : NeighborhoodSystem (Option (ExampleB.Str ⊕ ExampleB.Str))

The right-hand side of Scott's domain equation: the sum system B + B (Exercise 3.18).

Equations

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

theorem Domain.Neighborhood.Example62.sum_mem_inj₀_inv {X : Set ExampleB.Str} (h : BB.mem (inj₀ X)) : ExampleB.B.mem X

theorem Domain.Neighborhood.Example62.sum_mem_inj₁_inv {Y : Set ExampleB.Str} (h : BB.mem (inj₁ Y)) : ExampleB.B.mem Y

theorem Domain.Neighborhood.Example62.sum_mem_nonempty {W : Set (Option (ExampleB.Str ⊕ ExampleB.Str))} (h : BB.mem W) : W.Nonempty

The forward half toBB : |B| → |B + B|.

def Domain.Neighborhood.Example62.toBB (x : ExampleB.B.Element) : BB.Element

Example 6.2 — forward half of B ≅ B + B. An element x of B is sent to the sum element recording, for each branch, whether x reaches the 0-copy 0X (left summand) or the 1-copy 1Y (right summand).

Equations

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

theorem Domain.Neighborhood.Example62.toBB_mem_inj₀ {x : ExampleB.B.Element} {X : Set ExampleB.Str} (hX : ExampleB.B.mem X) : (toBB x).mem (inj₀ X) ↔ x.mem (embBit false X)

theorem Domain.Neighborhood.Example62.toBB_mem_inj₁ {x : ExampleB.B.Element} {Y : Set ExampleB.Str} (hY : ExampleB.B.mem Y) : (toBB x).mem (inj₁ Y) ↔ x.mem (embBit true Y)

The inverse half fromBB : |B + B| → |B|.

def Domain.Neighborhood.Example62.fromBB (s : BB.Element) : ExampleB.B.Element

Example 6.2 — inverse half of B ≅ B + B.

Equations

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

theorem Domain.Neighborhood.Example62.fromBB_mem_embF {s : BB.Element} {X : Set ExampleB.Str} (hX : ExampleB.B.mem X) : (fromBB s).mem (embBit false X) ↔ s.mem (inj₀ X)

theorem Domain.Neighborhood.Example62.fromBB_mem_embT {s : BB.Element} {Y : Set ExampleB.Str} (hY : ExampleB.B.mem Y) : (fromBB s).mem (embBit true Y) ↔ s.mem (inj₁ Y)

The two halves are mutually inverse.

theorem Domain.Neighborhood.Example62.fromBB_toBB (x : ExampleB.B.Element) : fromBB (toBB x) = x

theorem Domain.Neighborhood.Example62.toBB_fromBB (s : BB.Element) : toBB (fromBB s) = s

The domain equation B ≅ B + B.

def Domain.Neighborhood.Example62.bbEquiv : ExampleB.B.Element ≃o BB.Element

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

Equations

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

theorem Domain.Neighborhood.Example62.B_domain_equation : ExampleB.B ≅ᴰ sum ExampleB.B ExampleB.B B_nonempty B_nonempty

Example 6.2 (Scott 1981, PRG-19) — the domain equation B ≅ B + B. Scott's binary-sequence domain B is, as a domain, isomorphic to B + B: a sequence is bottom, or begins with 0, or begins with 1, the two non-bottom cases giving the two summands.