Exercise 5.14 (Scott 1981, PRG-19, Lecture V) — the graph model Pω

Using the pairing function of Exercise 5.13, code finite sequences by [n₀, …, n_k] = num(n₀, [n₁, …, n_k]) and define

fun(u)(x) = {m ∣ ∃ n₀ … n_{k-1} ∈ x, [n₀+1, …, n_{k-1}+1, 0, m] ∈ u}, graph(f) = {[n₀+1, …, n_{k-1}+1, 0, m] ∣ m ∈ f({n₀, …, n_{k-1}})}.

Show fun ∘ graph = λf.f (for continuous f) and graph ∘ fun ⊇ λx.x.

Following Exercises 4.17 and 5.13, the power-set domain Pω is modelled by the complete lattice (Set ℕ, ⊆).

The coding

The decisive device is the tag tag [n₀, …, n_{k-1}] m = [n₀+1, …, n_{k-1}+1, 0, m] = num(n₀+1, … num(n_{k-1}+1, num(0, m))…), defined by

tag [] m = num 0 m, tag (n :: ns) m = num (n+1) (tag ns m).

It is a bijection (List ℕ) × ℕ ≃ ℕ: injectivity (tag_injective) is an induction using num_injective, and surjectivity (tag_surjective) is strong induction on the value, decreasing because num (n+1) b > b (num_succ_left_gt) — the head's first coordinate is either 0 (stop, emit m) or ≥ 1 (peel one entry and recurse on a strictly smaller code).

The maps

With entries ns = {n ∣ n ∈ ns} the finite set of entries of a list:

• Fun u x = {m ∣ ∃ ns, (∀ n ∈ ns, n ∈ x) ∧ tag ns m ∈ u},
• Graph f = {c ∣ ∃ ns m, c = tag ns m ∧ m ∈ f (entries ns)}.

fun ∘ graph = id holds only for continuous maps, captured by IsApprox f := Monotone f ∧ (finite approximation). We prove:

• Fun_Graph : Fun (Graph f) x = f x for IsApprox f — the reflexive equation fun ∘ graph = λf.f;
• id_le_Graph_Fun : u ⊆ Graph (Fun u) — the inclusion graph ∘ fun ⊇ λx.x (genuinely ⊇, since reorderings/duplications of a list with the same entries give other codes in Graph (Fun u));
• Fun_isApprox : every Fun u is itself IsApprox, so fun lands in the continuous maps.

Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

A strict lower bound for num

theorem Domain.Neighborhood.Exercise514.num_succ_left_gt (n b : ℕ) : b < Exercise513.num (n + 1) b

num (n+1) b strictly exceeds its second argument: this is what makes the decode recursion terminate. num (n+1) b = T(n+1+b) + b ≥ (n+b+1) + b > b.

The tag: coding (List ℕ) × ℕ as ℕ

def Domain.Neighborhood.Exercise514.tag : List ℕ → ℕ → ℕ

tag [n₀, …, n_{k-1}] m = [n₀+1, …, n_{k-1}+1, 0, m], built from the pairing function num.

Equations

• Domain.Neighborhood.Exercise514.tag [] x✝ = Domain.Neighborhood.Exercise513.num 0 x✝
• Domain.Neighborhood.Exercise514.tag (n :: ns) x✝ = Domain.Neighborhood.Exercise513.num (n + 1) (Domain.Neighborhood.Exercise514.tag ns x✝)

@[simp]

theorem Domain.Neighborhood.Exercise514.tag_nil (m : ℕ) : tag [] m = Exercise513.num 0 m

@[simp]

theorem Domain.Neighborhood.Exercise514.tag_cons (n : ℕ) (ns : List ℕ) (m : ℕ) : tag (n :: ns) m = Exercise513.num (n + 1) (tag ns m)

theorem Domain.Neighborhood.Exercise514.tag_injective {ns₁ ns₂ : List ℕ} {m₁ m₂ : ℕ} : tag ns₁ m₁ = tag ns₂ m₂ → ns₁ = ns₂ ∧ m₁ = m₂

The tag is one-one, jointly in both arguments (induction on the list + num_injective).

theorem Domain.Neighborhood.Exercise514.tag_surjective (c : ℕ) : ∃ (ns : List ℕ) (m : ℕ), tag ns m = c

The tag is onto: every c : ℕ decodes as some tag ns m. Strong induction on c, decreasing via num_succ_left_gt.

The maps fun and graph

def Domain.Neighborhood.Exercise514.entries (ns : List ℕ) : Set ℕ

The finite set of entries of a list, as a subset of ℕ.

Equations

• Domain.Neighborhood.Exercise514.entries ns = {n : ℕ | n ∈ ns}

@[simp]

theorem Domain.Neighborhood.Exercise514.mem_entries {n : ℕ} {ns : List ℕ} : n ∈ entries ns ↔ n ∈ ns

def Domain.Neighborhood.Exercise514.Fun (u x : Set ℕ) : Set ℕ

fun(u)(x) — apply the "function coded by u" to argument x.

Equations

• Domain.Neighborhood.Exercise514.Fun u x = {m : ℕ | ∃ (ns : List ℕ), (∀ n ∈ ns, n ∈ x) ∧ Domain.Neighborhood.Exercise514.tag ns m ∈ u}

def Domain.Neighborhood.Exercise514.Graph (f : Set ℕ → Set ℕ) : Set ℕ

graph(f) — the code of the function f.

Equations

• Domain.Neighborhood.Exercise514.Graph f = {c : ℕ | ∃ (ns : List ℕ) (m : ℕ), c = Domain.Neighborhood.Exercise514.tag ns m ∧ m ∈ f (Domain.Neighborhood.Exercise514.entries ns)}

def Domain.Neighborhood.Exercise514.IsApprox (f : Set ℕ → Set ℕ) : Prop

A map f : Pω → Pω is approximable (continuous) when it is monotone and every output is already produced by a finite subset of the input. The finite subsets of x are exactly the entries ns with all entries in x.

Monotonicity is phrased as an explicit ⊆-implication rather than Monotone f: on Set ℕ the order ≤ resolves through the CompleteLattice instance whose construction uses Classical.choice, so the Monotone-based statement would not be choice-free. The two are definitionally equal.

Equations

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

theorem Domain.Neighborhood.Exercise514.Fun_Graph {f : Set ℕ → Set ℕ} (hf : IsApprox f) (x : Set ℕ) : Fun (Graph f) x = f x

fun ∘ graph = λf.f for continuous f: Fun (Graph f) x = f x.

theorem Domain.Neighborhood.Exercise514.id_le_Graph_Fun (u : Set ℕ) : u ⊆ Graph (Fun u)

graph ∘ fun ⊇ λx.x: u ⊆ Graph (Fun u).

theorem Domain.Neighborhood.Exercise514.Fun_isApprox (u : Set ℕ) : IsApprox (Fun u)

Every Fun u is itself approximable, so fun really lands in the continuous maps.