Exercise 2.21 (Scott 1981, PRG-19) — the system 𝒞, total finite sequences,

juxtaposition

The system 𝔹 of 2.3 has as its total elements only the infinite sequences: a finite prefix σ only ever yields the partial element σ⊥ = ↑(σΣ*), which can always be sharpened by a longer prefix. We modify 𝔹 to a system 𝒞 having both finite and infinite sequences as total elements (Scott's hint 𝔹 ⊆ 𝒞).

The idea: keep the cones σΣ* = cone σ of 𝔹 (these give the partial σ⊥ and, in the limit, the infinite total sequences), and add for every finite σ a terminator token — the singleton {σ}. The neighbourhood {σ} asserts "the sequence is exactly σ (terminated)". Because {σ} is a minimal nonempty neighbourhood, ↑{σ} is a total (maximal) element — this is the total finite sequence σ. We thus distinguish:

• Λ = ↑{[]} — the total empty sequence (terminated), and
• ⊥ = ↑Δ = ↑(cone []) — the undefined sequence, with ⊥ ⊏ Λ.

𝒞 = {σΣ*} ∪ {{σ}} is again pairwise nested-or-disjoint (a singleton sits inside a cone exactly when its string extends the cone's prefix; two distinct singletons are disjoint), so it is a neighbourhood system via ofNestedOrDisjoint, and visibly 𝔹 ⊆ 𝒞.

Juxtaposition xy. We build juxtapose : ApproximableMap₂ 𝒞 𝒞 𝒞 realizing the left-to-right-biased concatenation:

• if x extends the prefix σ but is not known to terminate (a cone neighbourhood σΣ* ∈ x), the result only commits to the prefix σ — xy ⊒ σ⊥, independent of y. Hence for an infinite (total) x, xy = x for all y (juxtapose_cone);
• if x is the total finite sequence σ (the terminator {σ} ∈ x), the result is σ followed by y: xy prepends σ to y (juxtapose_singleton_mem).

This is the "strong left-to-right bias" Scott describes: y is consulted only after x is known to have terminated.

The neighbourhood system 𝒞: cones together with terminator singletons.

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

Membership in 𝒞: X is either a cone σΣ* (as in 𝔹) or a terminator singleton {σ}.

Equations

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

theorem Domain.Neighborhood.Exercise221.cone_not_subset_singleton (σ τ : ExampleB.Str) : ¬ExampleB.cone σ ⊆ {τ}

A singleton is never a cone (a cone has at least two elements σ and σ0).

theorem Domain.Neighborhood.Exercise221.cone_ne_singleton (σ τ : ExampleB.Str) : ExampleB.cone σ ≠ {τ}

Cones and singletons are distinct neighbourhoods.

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

Nested-or-disjoint for a cone vs. a terminator singleton: {τ} ⊆ σΣ* iff σ prefix τ, else disjoint. Choice-free (σ <+: τ is decidable).

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

Nested-or-disjoint for a terminator singleton vs. a cone (the mirror of cone_singleton_nd).

theorem Domain.Neighborhood.Exercise221.singleton_singleton_nd (σ τ : ExampleB.Str) : {σ} ⊆ {τ} ∨ {τ} ⊆ {σ} ∨ {σ} ∩ {τ} = ∅

Nested-or-disjoint for two terminator singletons: equal or disjoint.

theorem Domain.Neighborhood.Exercise221.nestedOrDisjoint_C : NestedOrDisjoint memC

𝒞 is pairwise nested-or-disjoint. Cone/cone is the 𝔹 trichotomy; the mixed and singleton/singleton cases are the three lemmas above.

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

The system 𝒞 on Δ = Σ*: cones and terminator singletons.

Equations

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

@[simp]

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

@[simp]

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

theorem Domain.Neighborhood.Exercise221.memC_cone (σ : ExampleB.Str) : C.mem (ExampleB.cone σ)

Every cone is a neighbourhood of 𝒞 — this is the inclusion 𝔹 ⊆ 𝒞.

theorem Domain.Neighborhood.Exercise221.memC_singleton (σ : ExampleB.Str) : C.mem {σ}

Every terminator singleton {σ} is a neighbourhood of 𝒞.

theorem Domain.Neighborhood.Exercise221.memB_imp_memC {X : Set ExampleB.Str} (hX : ExampleB.B.mem X) : C.mem X

𝔹 ⊆ 𝒞. Every neighbourhood of 𝔹 is a neighbourhood of 𝒞.

theorem Domain.Neighborhood.Exercise221.memC_nonempty {W : Set ExampleB.Str} (hW : C.mem W) : W.Nonempty

Every neighbourhood of 𝒞 is nonempty (there is no empty token).

theorem Domain.Neighborhood.Exercise221.subset_singleton_eq {W : Set ExampleB.Str} {σ : ExampleB.Str} (hW : C.mem W) (hsub : W ⊆ {σ}) : W = {σ}

A nonempty 𝒞-neighbourhood contained in a singleton is that singleton.

Total elements: finite sequences ↑{σ}, and ⊥ ⊏ Λ.

def Domain.Neighborhood.Exercise221.singletonElt (σ : ExampleB.Str) : C.Element

The total finite sequence σ as an element of |𝒞|: the principal filter ↑{σ}.

Equations

• Domain.Neighborhood.Exercise221.singletonElt σ = Domain.Neighborhood.Exercise221.C.principal ⋯

def Domain.Neighborhood.Exercise221.Lambda : C.Element

Λ, the total empty sequence (terminated): ↑{[]}.

Equations

• Domain.Neighborhood.Exercise221.Lambda = Domain.Neighborhood.Exercise221.singletonElt []

theorem Domain.Neighborhood.Exercise221.isTotal_singletonElt (σ : ExampleB.Str) : C.IsTotal (singletonElt σ)

Total finite sequences. ↑{σ} is a total (maximal) element of |𝒞|: any element above it must equal it, because {σ} is a minimal nonempty neighbourhood. This is what was false in 𝔹, where finite sequences gave only the partial σ⊥.

theorem Domain.Neighborhood.Exercise221.bot_lt_Lambda : C.bot < Lambda

⊥ ⊏ Λ. The undefined sequence ⊥ = ↑Δ is strictly below the total empty sequence Λ = ↑{[]}: they are distinct because ⊥ contains only Δ, whereas Λ contains {[]} ≠ Δ.

Prepending a string to a 𝒞-neighbourhood.

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

σ{ρ} = {σρ}: prepending σ to a terminator singleton.

theorem Domain.Neighborhood.Exercise221.memC_prepend (σ : ExampleB.Str) {Y : Set ExampleB.Str} (hY : C.mem Y) : C.mem (ExampleB.prepend σ Y)

Prepending preserves 𝒞-membership (cone ↦ cone, singleton ↦ singleton).

theorem Domain.Neighborhood.Exercise221.prepend_subset_cone (σ : ExampleB.Str) (Y : Set ExampleB.Str) : ExampleB.prepend σ Y ⊆ ExampleB.cone σ

σY ⊆ σΣ* = cone σ: prepending σ always lands inside the cone of σ.

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

Prepending is monotone in the suffix set.

Juxtaposition xy as an approximable map of two variables.

def Domain.Neighborhood.Exercise221.juxtapose : ApproximableMap₂ C C C

Juxtaposition xy as an approximable map 𝒞 × 𝒞 → 𝒞.

The relation X, Y j Z reads off the left-to-right bias: if the first input neighbourhood X is a cone σΣ* (x extends σ but is undetermined), the output only commits to the prefix σ (σΣ* ⊆ Z), ignoring Y; if X is a terminator {σ} (x is the total finite sequence σ), the output prepends σ to the second input Y (σY ⊆ Z).

Equations

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

theorem Domain.Neighborhood.Exercise221.juxtapose_cone (σ : ExampleB.Str) (y : C.Element) : juxtapose.toElementMap₂ (C.principal ⋯) y = C.principal ⋯

Left-to-right bias / "x infinite ⟹ xy = x". On a partial input σ⊥ = ↑(σΣ*) the juxtaposition returns σ⊥ itself, independently of y. Since an infinite (total) sequence is the directed union of its finite approximants σ⊥, this says xy = x for total infinite x.

theorem Domain.Neighborhood.Exercise221.juxtapose_singleton_mem (σ : ExampleB.Str) (y : C.Element) {Z : Set ExampleB.Str} : (juxtapose.toElementMap₂ (singletonElt σ) y).mem Z ↔ C.mem Z ∧ ∃ (Y' : Set ExampleB.Str), y.mem Y' ∧ ExampleB.prepend σ Y' ⊆ Z

σy for a total finite x = ↑{σ}. When the first argument is the total finite sequence σ, juxtaposition prepends σ to y: Z ∈ (↑{σ})y iff Z contains σY' for some Y' ∈ y. The coarser cone witnesses σΣ* ∈ ↑{σ} add nothing, since σΔ = σΣ* is itself of the form σY'.