Exercise 4.25 (Scott 1981, PRG-19, Lecture IV) — the unary sequence domain C₁

"Perhaps the domains N and C are not exactly analogous?" C (Example 4.4) was built over the two-letter alphabet {0,1}. Scott asks to build the analogue C₁ over {1}* — finite strings of 1s, which we encode by their length n ∈ ℕ (so 1ⁿ ↔ n). The neighbourhoods are the tails and the singletons:

C₁ = {{1ᵐ ∣ m ≥ n} ∣ n ∈ ℕ} ∪ {{1ⁿ} ∣ n ∈ ℕ} (tail n = {m ∣ n ≤ m}, {n}).

This is again a nested-or-disjoint system (ofNestedOrDisjoint): the tails form a descending chain and a singleton is either inside a tail or disjoint from it. The total elements are the finite strings 1ⁿ (oneElem n = ↑{n}) and the partial elements 1ⁿ⊥ ("at least n ones", oneBot n = ↑(tail n)).

The structure analogous to C is the single successor x ↦ 1x (consMap, prepending a 1, i.e. shifting the length up by one), with consMap_oneElem/consMap_oneBot. Crucially — and this is Scott's point that N and C are not analogous — C₁ is not flat like N: the successor has a genuine infinite fixed point 1^∞ = 1·1^∞ (infElt, infElt_eq), the limit ⊔ₙ 1ⁿ⊥ of the tails, which has no counterpart among the elements ⊥, 0̂, 1̂, 2̂, … of the flat domain N. So C₁ is the genuine unary analogue of C (= C₂), distinct from N.

Finally, the systems are related by approximable maps: e.g. relateNToC1 : N → C₁ sends the numeral n̂ to the finite string 1ⁿ and is strict (⊥ ↦ ⊥) — the natural "length ↦ unary expansion" map (relateNToC1_natElem, relateNToC1_bot).

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

Tails, singletons, and the shift.

def Domain.Neighborhood.Exercise425.tail (n : ℕ) : Set ℕ

The tail tail n = {1ᵐ ∣ m ≥ n} = {m ∣ n ≤ m} (the partial information "at least n ones").

Equations

• Domain.Neighborhood.Exercise425.tail n = {m : ℕ | n ≤ m}

def Domain.Neighborhood.Exercise425.shift (X : Set ℕ) : Set ℕ

Shifting a set up by one length: shift X = {m + 1 ∣ m ∈ X} (the token action of prepending a 1).

Equations

• Domain.Neighborhood.Exercise425.shift X = {k : ℕ | ∃ m ∈ X, k = m + 1}

theorem Domain.Neighborhood.Exercise425.tail_zero : tail 0 = Set.univ

@[simp]

theorem Domain.Neighborhood.Exercise425.mem_tail {n k : ℕ} : k ∈ tail n ↔ n ≤ k

theorem Domain.Neighborhood.Exercise425.shift_tail (n : ℕ) : shift (tail n) = tail (n + 1)

1·(1ⁿ⊥) = 1ⁿ⁺¹⊥: shifting a tail.

theorem Domain.Neighborhood.Exercise425.shift_singleton (n : ℕ) : shift {n} = {n + 1}

1·{1ⁿ} = {1ⁿ⁺¹}: shifting a singleton.

theorem Domain.Neighborhood.Exercise425.shift_mono {X X' : Set ℕ} (h : X' ⊆ X) : shift X' ⊆ shift X

The neighbourhood system C₁.

def Domain.Neighborhood.Exercise425.memC1 (X : Set ℕ) : Prop

Membership in C₁: a neighbourhood is a tail tail n or a singleton {n}.

Equations

• Domain.Neighborhood.Exercise425.memC1 X = ((∃ (n : ℕ), X = Domain.Neighborhood.Exercise425.tail n) ∨ ∃ (n : ℕ), X = {n})

theorem Domain.Neighborhood.Exercise425.memC1_tail (n : ℕ) : memC1 (tail n)

theorem Domain.Neighborhood.Exercise425.memC1_singleton (n : ℕ) : memC1 {n}

theorem Domain.Neighborhood.Exercise425.memC1_univ : memC1 Set.univ

theorem Domain.Neighborhood.Exercise425.memC1_shift {X : Set ℕ} (hX : memC1 X) : memC1 (shift X)

Shifting keeps us inside C₁ (shift (tail n) = tail (n+1), shift {n} = {n+1}).

theorem Domain.Neighborhood.Exercise425.singleton_tail_nd (n k : ℕ) : {k} ⊆ tail n ∨ tail n ⊆ {k} ∨ {k} ∩ tail n = ∅

A singleton and a tail are nested or disjoint.

theorem Domain.Neighborhood.Exercise425.nestedOrDisjoint : NestedOrDisjoint memC1

Any two neighbourhoods of C₁ are nested or disjoint.

def Domain.Neighborhood.Exercise425.C1 : NeighborhoodSystem ℕ

Exercise 4.25 (Scott 1981, PRG-19). The unary sequence system C₁ on Δ = {1}* ≅ ℕ.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise425.C1_mem {X : Set ℕ} : C1.mem X ↔ memC1 X

@[simp]

theorem Domain.Neighborhood.Exercise425.C1_master : C1.master = Set.univ

Elements: 1ⁿ (total) and 1ⁿ⊥ (partial).

def Domain.Neighborhood.Exercise425.oneBot (n : ℕ) : C1.Element

The partial element 1ⁿ⊥ = ↑(tail n) ("at least n ones").

Equations

• Domain.Neighborhood.Exercise425.oneBot n = Domain.Neighborhood.Exercise425.C1.principal ⋯

def Domain.Neighborhood.Exercise425.oneElem (n : ℕ) : C1.Element

The total element 1ⁿ = ↑{n} (the finite string of exactly n ones).

Equations

• Domain.Neighborhood.Exercise425.oneElem n = Domain.Neighborhood.Exercise425.C1.principal ⋯

The successor x ↦ 1x.

def Domain.Neighborhood.Exercise425.consMap : ApproximableMap C1 C1

Exercise 4.25 — the successor x ↦ 1x (analogous to the two successors of C). The approximable map prepending a 1, i.e. shifting the length: X (1x) Y ↔ shift X ⊆ Y.

Equations

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

theorem Domain.Neighborhood.Exercise425.consMap_oneBot (n : ℕ) : consMap.toElementMap (oneBot n) = oneBot (n + 1)

1·(1ⁿ⊥) = 1ⁿ⁺¹⊥.

theorem Domain.Neighborhood.Exercise425.consMap_oneElem (n : ℕ) : consMap.toElementMap (oneElem n) = oneElem (n + 1)

1·(1ⁿ) = 1ⁿ⁺¹.

The infinite element 1^∞ = 1·1^∞.

def Domain.Neighborhood.Exercise425.infElt : C1.Element

Exercise 4.25 — the infinite unary sequence 1^∞. Unlike the flat domain N (whose only elements are ⊥ and the numerals n̂), C₁ has a genuine infinite element: the least fixed point of the successor x ↦ 1x, satisfying 1^∞ = 1·1^∞ (infElt_eq). This is what distinguishes the non-flat C₁ (the true analogue of C) from N.

Equations

• Domain.Neighborhood.Exercise425.infElt = Domain.Neighborhood.Exercise425.consMap.fixElement

theorem Domain.Neighborhood.Exercise425.infElt_eq : consMap.toElementMap infElt = infElt

1^∞ = 1·1^∞: the infinite sequence is fixed by the successor.

An approximable map relating N and C₁.

def Domain.Neighborhood.Exercise425.relateNToC1 : ApproximableMap Example43.N C1

Exercise 4.25 — relating N and C₁. The "length ↦ unary expansion" map N → C₁ sending the numeral n̂ to the finite string 1ⁿ and ⊥ to ⊥ (strict). Built from the strict-lift combinator constLiftN of Example 4.3.

Equations

• Domain.Neighborhood.Exercise425.relateNToC1 = Domain.Neighborhood.Example43.constLiftN Domain.Neighborhood.Exercise425.C1 Domain.Neighborhood.Exercise425.oneElem

theorem Domain.Neighborhood.Exercise425.relateNToC1_natElem (n : ℕ) : relateNToC1.toElementMap (Example43.natElem n) = oneElem n

relateNToC1(n̂) = 1ⁿ.

theorem Domain.Neighborhood.Exercise425.relateNToC1_bot : relateNToC1.toElementMap Example43.N.bot = C1.bot

relateNToC1(⊥) = ⊥.