Example 2.3 (Scott 1981, PRG-19, §2) — the parity map f : B → T

Scott's first approximable mapping. Reading a binary sequence left to right, count the number n of 0's seen before the first 1; the output is true if n is even, false if n is odd, and ⊥ while the input is still an unbroken string of 0's (which has consistent extensions of both parities). Concretely

f(0ⁿ1⊥) = true if n even, false if n odd; f(0^∞) = ⊥.

Here B is the binary system (ExampleB) and T is the two-token domain of Example 1.2, whose two total elements we use as true/false and whose unique partial element is ⊥.

We model the relation by a parity scanner scan : Σ* → Option Bool: scan returns none while no 1 has appeared and some b (with b the parity-of-leading-zeros) once the first 1 is found. The neighbourhood relation is

X f Y ↔ ∃ σ, X = σΣ* ∧ Y ∈ valElt (scan σ),

where valElt none = ⊥, valElt (some true) = true, valElt (some false) = false. The cone σΣ* has a unique generating prefix (cone_injective), so this is well defined, and scan is stable under extension (scan_append), which is exactly the monotonicity (Def 2.1(iii)).

Definition 2.1(i)–(iii) all check out, giving parityMap : ApproximableMap B T. (The B-side reasoning is choice-free; parityMap nonetheless pulls Classical.choice through the concrete codomain T of Example 1.2, whose simp/fin_cases proofs already do — pre-existing and harmless.)

@[reducible, inline]

abbrev Domain.Neighborhood.Example23.T : NeighborhoodSystem Example12.Token

The two-token codomain T of Example 1.2.

Equations

• Domain.Neighborhood.Example23.T = Domain.Neighborhood.Example12.neighborhoodSystem

def Domain.Neighborhood.Example23.trueElt : T.Element

Scott's true: the total element {Δ, {0}} of T.

Equations

• Domain.Neighborhood.Example23.trueElt = Domain.Neighborhood.Example12.neighborhoodSystem.elemZero

def Domain.Neighborhood.Example23.falseElt : T.Element

Scott's false: the total element {Δ, {1}} of T.

Equations

• Domain.Neighborhood.Example23.falseElt = Domain.Neighborhood.Example12.neighborhoodSystem.elemOne

def Domain.Neighborhood.Example23.botElt : T.Element

Scott's ⊥: the unique partial element {Δ} of T.

Equations

• Domain.Neighborhood.Example23.botElt = Domain.Neighborhood.Example12.neighborhoodSystem.bot

def Domain.Neighborhood.Example23.valElt : Option Bool → T.Element

The codomain element selected by a parity reading: none ↦ ⊥, some true ↦ true, some false ↦ false.

Equations

• Domain.Neighborhood.Example23.valElt none = Domain.Neighborhood.Example23.botElt
• Domain.Neighborhood.Example23.valElt (some true) = Domain.Neighborhood.Example23.trueElt
• Domain.Neighborhood.Example23.valElt (some false) = Domain.Neighborhood.Example23.falseElt

theorem Domain.Neighborhood.Example23.botElt_le (x : T.Element) : botElt ≤ x

⊥ approximates every element of T (the local {Δ} form, proved directly).

def Domain.Neighborhood.Example23.scan : ExampleB.Str → Option Bool

The parity scanner. scan σ = none while σ is an unbroken run of 0's; once a 1 appears, scan σ = some b with b = true iff an even number of 0's preceded it. A leading 0 flips the parity of the rest; a leading 1 fixes parity true (zero preceding zeros).

Equations

• Domain.Neighborhood.Example23.scan [] = none
• Domain.Neighborhood.Example23.scan (true :: tail) = some true
• Domain.Neighborhood.Example23.scan (false :: t) = Option.map (fun (x : Bool) => !x) (Domain.Neighborhood.Example23.scan t)

@[simp]

theorem Domain.Neighborhood.Example23.scan_nil : scan [] = none

@[simp]

theorem Domain.Neighborhood.Example23.scan_true (t : ExampleB.Str) : scan (true :: t) = some true

@[simp]

theorem Domain.Neighborhood.Example23.scan_false (t : ExampleB.Str) : scan (false :: t) = Option.map (fun (x : Bool) => !x) (scan t)

theorem Domain.Neighborhood.Example23.scan_append {σ : ExampleB.Str} {b : Bool} (h : scan σ = some b) (t : ExampleB.Str) : scan (σ ++ t) = some b

Stability of the scan under extension. Once scan σ has committed to a parity some b, every extension σ ++ t keeps that value. This is the engine of monotonicity for parityMap.

theorem Domain.Neighborhood.Example23.valElt_scan_mono {σ σ' : ExampleB.Str} (h : σ <+: σ') : valElt (scan σ) ≤ valElt (scan σ')

Monotonicity of the parity value. A longer prefix σ <+: σ' yields a (weakly) more defined value: valElt (scan σ) ⊑ valElt (scan σ'). If scan σ = none then valElt = ⊥ ⊑ _; otherwise the value is fixed by scan_append.

def Domain.Neighborhood.Example23.parityMap : ApproximableMap ExampleB.B T

Example 2.3 — the parity mapping f : B → T. X f Y iff X is the cone σΣ* of some prefix σ and Y is approximated by the parity verdict valElt (scan σ). Definition 2.1: (i) the empty prefix scans to none = ⊥, and ⊥ contains Δ_T; (ii) for a fixed cone the verdict is a single filter (cones have a unique prefix), closed under ∩; (iii) extending the prefix only sharpens the verdict (valElt_scan_mono).

Equations

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