Exercise 2.16 (Scott 1981, PRG-19, §2) — the prefixing map x ↦ σx is

approximable

In Lecture I (Example 1.B) Scott defined, for each finite string σ ∈ Σ*, the elementwise operation x ↦ σx on |B| (ExampleB.sigmaElt). Exercise 2.16 asks whether this mapping is approximable. It is: the witnessing neighbourhood relation is

X f Y ↔ X, Y ∈ B ∧ σX ⊆ Y,

i.e. "the prefixed input cone σX is at least as sharp as Y." We package it as sigmaMap σ : ApproximableMap B B and show its elementwise action is exactly sigmaElt σ (toElementMap_sigmaMap).

(The second half of 2.16 — that the parity map f : B → T of Example 2.3 is the unique approximable map satisfying f(1x)=true, f(01x)=false, f(00x)=f(x) — is an equational-uniqueness statement left to a later pass.) Constructive (#print axioms ⊆ {propext, Quot.sound}).

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

Prepending a prefix is monotone: X' ⊆ X → σX' ⊆ σX.

def Domain.Neighborhood.Exercise216.sigmaMap (σ : ExampleB.Str) : ApproximableMap ExampleB.B ExampleB.B

Exercise 2.16 — x ↦ σx is approximable. The neighbourhood relation X f Y ↔ σX ⊆ Y (confined to B × B). Definition 2.1: (i) σΔ ⊆ Δ; (ii) the prefixed cone σX is a common lower bound of Y, Y', witnessing Y ∩ Y' ∈ B; (iii) prepend_mono shrinks σX' as X' ⊆ X.

Equations

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

theorem Domain.Neighborhood.Exercise216.toElementMap_sigmaMap (σ : ExampleB.Str) (x : ExampleB.B.Element) : (sigmaMap σ).toElementMap x = ExampleB.sigmaElt σ x

Exercise 2.16. The elementwise action of sigmaMap σ is Scott's σx: (sigmaMap σ)(x) = σx for every x ∈ |B|.