Exercise 2.18 (Scott 1981, PRG-19, §2) — the "spacing" map h : 𝔹 → 𝔹

EXERCISE 2.18. What is the meaning in words of the approximable mapping h : 𝔹 → 𝔹, where h(0x) = 00 h(x) and h(1x) = 10 h(x) for all x ∈ |𝔹|? Is h an isomorphism? Does there exist a map k : 𝔹 → 𝔹 where k ∘ h = I_𝔹, and is k one-one?

Meaning in words. h spaces the sequence out: it copies each input symbol b and inserts a 0 immediately after it. So the input bit b becomes the block b0, and h doubles the length of every sequence, planting a 0 in every odd position (0-indexed positions 1, 3, 5, …).

We follow the Example24.runMap template: a guaranteed-output function on finite prefixes drives the neighbourhood relation X h Y ↔ ∃ σ, X = σΣ* ∧ Y ∈ 𝔹 ∧ (hOut σ)Σ* ⊆ Y.

• hOut σ — the doubling of σ (each b ↦ b0); hMap : ApproximableMap B B.
• kOut τ — the left inverse on prefixes: keep the first bit of every complete pair, drop the inserted 0; kMap : ApproximableMap B B. Key identity: kOut (hOut σ) = σ.
• kMap_comp_hMap — k ∘ h = I_𝔹 (so the required k exists).
• kMap_not_injective — k is not one-one: ↑(0Σ*) and ↑(1Σ*) both map to ⊥ (the first bit of a length-1 prefix is an incomplete pair, hence dropped).
• hMap_not_surjective — h is not an isomorphism: it is not surjective (e.g. ↑(01Σ*) is not in the range, since h only produces sequences with 0 in every odd position). h is injective (it has the left inverse k), so it is injective-but-not-surjective.

Choice-free (#print axioms ⊆ {propext, Quot.sound}): everything is decidable list surgery.

The doubling output hOut and its monotonicity.

def Domain.Neighborhood.Exercise218.hOut : ExampleB.Str → ExampleB.Str

The guaranteed output of h on a finite prefix: each symbol b becomes the block b0.

Equations

• Domain.Neighborhood.Exercise218.hOut [] = []
• Domain.Neighborhood.Exercise218.hOut (b :: t) = b :: false :: Domain.Neighborhood.Exercise218.hOut t

@[simp]

theorem Domain.Neighborhood.Exercise218.hOut_nil : hOut [] = []

@[simp]

theorem Domain.Neighborhood.Exercise218.hOut_cons (b : Bool) (t : ExampleB.Str) : hOut (b :: t) = b :: false :: hOut t

theorem Domain.Neighborhood.Exercise218.hOut_append (σ t : ExampleB.Str) : hOut σ <+: hOut (σ ++ t)

hOut grows under extension: hOut σ <+: hOut (σ ++ t).

theorem Domain.Neighborhood.Exercise218.hOut_mono {σ σ' : ExampleB.Str} (h : σ <+: σ') : hOut σ <+: hOut σ'

Prefix-monotonicity of hOut. σ <+: σ' → hOut σ <+: hOut σ'.

The inverse output kOut and its monotonicity.

def Domain.Neighborhood.Exercise218.kOut : ExampleB.Str → ExampleB.Str

The guaranteed output of k on a finite prefix: keep the first bit of every complete pair, discard the inserted 0. A trailing odd bit is an incomplete pair, hence dropped.

Equations

• Domain.Neighborhood.Exercise218.kOut [] = []
• Domain.Neighborhood.Exercise218.kOut [head] = []
• Domain.Neighborhood.Exercise218.kOut (b :: head :: t) = b :: Domain.Neighborhood.Exercise218.kOut t

@[simp]

theorem Domain.Neighborhood.Exercise218.kOut_nil : kOut [] = []

@[simp]

theorem Domain.Neighborhood.Exercise218.kOut_single (b : Bool) : kOut [b] = []

@[simp]

theorem Domain.Neighborhood.Exercise218.kOut_cons (b c : Bool) (t : ExampleB.Str) : kOut (b :: c :: t) = b :: kOut t

theorem Domain.Neighborhood.Exercise218.kOut_hOut (σ : ExampleB.Str) : kOut (hOut σ) = σ

k inverts h on prefixes. kOut (hOut σ) = σ.

theorem Domain.Neighborhood.Exercise218.kOut_append (σ t : ExampleB.Str) : kOut σ <+: kOut (σ ++ t)

kOut grows under extension: kOut σ <+: kOut (σ ++ t).

theorem Domain.Neighborhood.Exercise218.kOut_mono {σ σ' : ExampleB.Str} (h : σ <+: σ') : kOut σ <+: kOut σ'

Prefix-monotonicity of kOut. σ <+: σ' → kOut σ <+: kOut σ'.

The approximable maps hMap and kMap.

def Domain.Neighborhood.Exercise218.hMap : ApproximableMap ExampleB.B ExampleB.B

Exercise 2.18 — the spacing map h : 𝔹 → 𝔹. X h Y ↔ ∃ σ, X = σΣ* ∧ Y ∈ 𝔹 ∧ (hOut σ)Σ* ⊆ Y. Same shape as Example24.runMap, with the doubling hOut (hOut_mono gives Definition 2.1(iii)).

Equations

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

def Domain.Neighborhood.Exercise218.kMap : ApproximableMap ExampleB.B ExampleB.B

Exercise 2.18 — the left inverse k : 𝔹 → 𝔹. X k Y ↔ ∃ σ, X = σΣ* ∧ Y ∈ 𝔹 ∧ (kOut σ)Σ* ⊆ Y.

Equations

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

theorem Domain.Neighborhood.Exercise218.toElementMap_hMap_cone (σ : ExampleB.Str) : hMap.toElementMap (ExampleB.B.principal ⋯) = ExampleB.B.principal ⋯

The elementwise value of hMap on the finite element ↑(σΣ*) is ↑((hOut σ)Σ*).

theorem Domain.Neighborhood.Exercise218.toElementMap_kMap_cone (σ : ExampleB.Str) : kMap.toElementMap (ExampleB.B.principal ⋯) = ExampleB.B.principal ⋯

The elementwise value of kMap on the finite element ↑(σΣ*) is ↑((kOut σ)Σ*).

k ∘ h = I, k not injective, h not surjective.

theorem Domain.Neighborhood.Exercise218.kMap_comp_hMap : kMap.comp hMap = ApproximableMap.idMap ExampleB.B

Exercise 2.18 — k ∘ h = I_𝔹. The composite recovers the identity: reading kOut (hOut σ) = σ through the cone relations.

theorem Domain.Neighborhood.Exercise218.kMap_not_injective : ¬Function.Injective kMap.toElementMap

Exercise 2.18 — k is not one-one. ↑(0Σ*) and ↑(1Σ*) are distinct finite elements that k collapses to ⊥ (a length-1 prefix is an incomplete pair, so its bit is dropped).

theorem Domain.Neighborhood.Exercise218.hMap_not_surjective : ¬Function.Surjective hMap.toElementMap

Exercise 2.18 — h is not an isomorphism. It is not surjective: ↑(01Σ*) is not in the range (any preimage x satisfies x = k(h(x)), forcing h(x) = ↑(00Σ*) ≠ ↑(01Σ*)).