Example 4.4 (Scott 1981, PRG-19, §4) — the domain C of binary sequences

Scott's domain C of finite or infinite binary sequences (pages 61–64), a generalization of the natural-number domain N of Example 4.3. Over the tokens Σ* = List Bool (Scott's Σ = {0,1}, Λ = []), recall the cones cone σ = σΣ* of Example 1.B. The system C adds the singletons:

C = {σΣ* ∣ σ ∈ Σ*} ∪ {{σ} ∣ σ ∈ Σ*}.

The total elements correspond to finite or infinite sequences: σ = ↑{σ} (strElem σ, the finite sequence σ completed) and σ⊥ = ↑σΣ* (strBot σ, the partial element "starts with σ"). C is again nested-or-disjoint, so it is a neighbourhood system (ofNestedOrDisjoint).

We equip C with the two successors x ↦ 0x and x ↦ 1x (consMap false, consMap true), prepending a bit, with their action on the finite/partial elements (consMap_strElem, consMap_strBot). As Scott's illustration that recursion now lives inside |C|, we then define the alternating sequence a = 01a as the least fixed point of x ↦ 0(1x) (altElt, altElt_eq), using the Fixed-point Theorem 4.1.

The remaining structure maps Scott lists for ⟨C, Λ, 0, 1, tail, empty, zero, one⟩ — the predecessor analogue tail (tail(0x) = tail(1x) = x, tail(Λ) = ⊥) and the three tests empty, zero, one : C → T — are exactly the parts Scott leaves as exercises ("It is left to the reader to show that tail exists as an approximable mapping"; "it is an exercise to show these are approximable", Exercise 4.19); they are out of scope for this module.

The data constructions (C, consMap) are choice-free (#print axioms ⊆ {propext, Quot.sound}).

Prepending a bit: set-level lemmas (reused from Example 1.B).

theorem Domain.Neighborhood.Example44.prepend_singleton (σ τ : ExampleB.Str) : ExampleB.prepend σ {τ} = {σ ++ τ}

σ{τ} = {στ}: prepending σ to a singleton is the singleton of the concatenation.

theorem Domain.Neighborhood.Example44.prepend_mono (σ : ExampleB.Str) {X X' : Set ExampleB.Str} (h : X' ⊆ X) : ExampleB.prepend σ X' ⊆ ExampleB.prepend σ X

Prepending is monotone in its set argument.

The neighbourhood system C.

def Domain.Neighborhood.Example44.memC (X : Set ExampleB.Str) : Prop

Membership in C: a neighbourhood is a cone σΣ* or a singleton {σ}.

Equations

• Domain.Neighborhood.Example44.memC X = ((∃ (σ : Domain.Neighborhood.ExampleB.Str), X = Domain.Neighborhood.ExampleB.cone σ) ∨ ∃ (σ : Domain.Neighborhood.ExampleB.Str), X = {σ})

theorem Domain.Neighborhood.Example44.memC_cone (σ : ExampleB.Str) : memC (ExampleB.cone σ)

theorem Domain.Neighborhood.Example44.memC_singleton (σ : ExampleB.Str) : memC {σ}

theorem Domain.Neighborhood.Example44.singleton_subset_cone {σ τ : ExampleB.Str} : {τ} ⊆ ExampleB.cone σ ↔ σ <+: τ

{τ} ⊆ σΣ* iff σ is an initial segment of τ.

theorem Domain.Neighborhood.Example44.singleton_cone_nd (σ τ : ExampleB.Str) : {τ} ⊆ ExampleB.cone σ ∨ ExampleB.cone σ ⊆ {τ} ∨ {τ} ∩ ExampleB.cone σ = ∅

A singleton and a cone are nested-or-disjoint.

theorem Domain.Neighborhood.Example44.nestedOrDisjoint : NestedOrDisjoint memC

Any two neighbourhoods of C are nested or disjoint.

def Domain.Neighborhood.Example44.C : NeighborhoodSystem ExampleB.Str

Example 4.4 (Scott 1981, PRG-19). The neighbourhood system C of finite or infinite binary sequences on Δ = Σ*.

Equations

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

@[simp]

theorem Domain.Neighborhood.Example44.C_mem {X : Set ExampleB.Str} : C.mem X ↔ memC X

@[simp]

theorem Domain.Neighborhood.Example44.C_master : C.master = Set.univ

Elements of C: σ (total) and σ⊥ (partial).

def Domain.Neighborhood.Example44.strBot (σ : ExampleB.Str) : C.Element

Scott's partial element σ⊥ = ↑σΣ* ("the sequence starts with σ").

Equations

• Domain.Neighborhood.Example44.strBot σ = Domain.Neighborhood.Example44.C.principal ⋯

def Domain.Neighborhood.Example44.strElem (σ : ExampleB.Str) : C.Element

Scott's total element σ = ↑{σ} (the finite sequence σ, completed).

Equations

• Domain.Neighborhood.Example44.strElem σ = Domain.Neighborhood.Example44.C.principal ⋯

The successor maps x ↦ bx.

theorem Domain.Neighborhood.Example44.memC_prepend (σ : ExampleB.Str) {X : Set ExampleB.Str} (hX : memC X) : memC (ExampleB.prepend σ X)

Prepending the bit b (or, generally, a prefix σ) to a neighbourhood of C lands back in C: σ(τΣ*) = (στ)Σ* and σ{τ} = {στ}.

theorem Domain.Neighborhood.Example44.prepend_subset_self : True

σX ⊆ X along the prefix order: a prepended neighbourhood is contained in any neighbourhood it refines. (Used only via prepend_mono; kept implicit.)

def Domain.Neighborhood.Example44.consMap (b : Bool) : ApproximableMap C C

Example 4.4 — the successors x ↦ bx. The approximable map prepending the bit b: X (bx) Y ↔ bX ⊆ Y. Approximable because bX is again a neighbourhood (memC_prepend) and prepending is monotone.

Equations

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

theorem Domain.Neighborhood.Example44.consMap_strBot (b : Bool) (σ : ExampleB.Str) : (consMap b).toElementMap (strBot σ) = strBot (b :: σ)

bx on a partial element: b(σ⊥) = (bσ)⊥.

theorem Domain.Neighborhood.Example44.consMap_strElem (b : Bool) (σ : ExampleB.Str) : (consMap b).toElementMap (strElem σ) = strElem (b :: σ)

bx on a total element: b(σ) = (bσ) (prepend the bit to a finite sequence).

A fixed-point element: the alternating sequence a = 01a.

def Domain.Neighborhood.Example44.altElt : C.Element

Example 4.4 — an element defined by a fixed-point equation. Scott's a = 01a, the infinite sequence that alternates 0s and 1s. We take the least fixed point of x ↦ 0(1x) (= consMap 0 ∘ consMap 1), which exists by the Fixed-point Theorem 4.1.

Equations

• Domain.Neighborhood.Example44.altElt = ((Domain.Neighborhood.Example44.consMap false).comp (Domain.Neighborhood.Example44.consMap true)).fixElement

theorem Domain.Neighborhood.Example44.altElt_eq : (consMap false).toElementMap ((consMap true).toElementMap altElt) = altElt

a = 0(1a): altElt satisfies Scott's defining equation.