Lecture IV (§4) — fixed points and recursion: Theorems 4.1 and 4.2

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture IV, Fixed points and recursion. The heart of the matter is the Fixed-point Theorem:

• Theorem 4.1 — every approximable mapping f : 𝒟 → 𝒟 has a least element x ∈ |𝒟| with f(x) = x. Scott constructs x = {X ∈ 𝒟 ∣ Δ fⁿ X for some n}, the family of neighbourhoods reachable from the master Δ along finitely many f-steps. We model the n-fold composition fⁿ by iterMap f n (f⁰ = I_𝒟, f^{n+1} = f ∘ fⁿ) and the fixed point by fixElement f. The fixed-point equation is toElementMap_fixElement; minimality among pre-fixed points (f(z) ⊆ z ⟹ x ⊆ z) is fixElement_le_of_toElementMap_le.

• Theorem 4.2 — the operator fix : (𝒟 → 𝒟) → 𝒟 is itself approximable. We build it as fixMap V : ApproximableMap (funSpace V V) V via the extension-from-finite-elements principle (Exercise 2.8, ofMono), sending the finite element ↑F to fix(↑F) where ↑F = leastMap is the least map of the neighbourhood F (here toApproxMap (↑F)). The defining computation fixMap.toElementMap φ = fix(toApproxMap φ) is Scott's equation (∗) fix(f) = ⋃ {fix(↑F) ∣ f ∈ [F]} (fixMap_toElementMap), whose non-trivial half — every finite f-chain factors through one finite approximant F ∈ φ — is exists_principal_iterMap. Then (i) fix(f) = f(fix(f)) (fixMap_fixed); (ii) f(x) ⊆ x ⟹ fix(f) ⊆ x (fixMap_least); (iii) fix(f) = ⊔ₙ fⁿ(⊥) (fixMap_eq_iSup, with iterElem_eq_iterate giving the faithful ⊔ₙ fⁿ(⊥) form); and uniqueness (fixMap_unique).

All data constructions (iterMap, fixElement, iterElem, fixMap) are choice-free (#print axioms ⊆ {propext, Quot.sound}); the uniqueness lemma fixMap_unique pulls Classical.choice only through the project's ext_of_toElementMap, as permitted.

The iterated map fⁿ.

def Domain.Neighborhood.ApproximableMap.iterMap {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : ℕ → ApproximableMap V V

Theorem 4.1 (Scott 1981, PRG-19). The n-fold composition fⁿ of an endomap with itself: f⁰ = I_𝒟 and f^{n+1} = f ∘ fⁿ.

Equations

• f.iterMap 0 = Domain.Neighborhood.ApproximableMap.idMap V
• f.iterMap n.succ = f.comp (f.iterMap n)

@[simp]

theorem Domain.Neighborhood.ApproximableMap.iterMap_zero {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : f.iterMap 0 = idMap V

@[simp]

theorem Domain.Neighborhood.ApproximableMap.iterMap_succ {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.iterMap (n + 1) = f.comp (f.iterMap n)

theorem Domain.Neighborhood.ApproximableMap.comp_mono {α : Type u_1} {V : NeighborhoodSystem α} {f g a b : ApproximableMap V V} (hfg : f ≤ g) (hab : a ≤ b) : f.comp a ≤ g.comp b

Composition is monotone in both arguments.

theorem Domain.Neighborhood.ApproximableMap.iterMap_mono_map {α : Type u_1} {V : NeighborhoodSystem α} {f g : ApproximableMap V V} (hfg : f ≤ g) (n : ℕ) : f.iterMap n ≤ g.iterMap n

The iterate is monotone in the map: f ⊑ g ⟹ fⁿ ⊑ gⁿ (Scott's "fⁿ ⊆ gⁿ").

theorem Domain.Neighborhood.ApproximableMap.iter_comm {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.comp (f.iterMap n) = (f.iterMap n).comp f

f commutes with its own iterate: f ∘ fⁿ = fⁿ ∘ f. Proved by induction using associativity and the identity laws.

theorem Domain.Neighborhood.ApproximableMap.rel_master_succ {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {n : ℕ} {X : Set α} (h : (f.iterMap n).rel V.master X) : (f.iterMap (n + 1)).rel V.master X

Scott's "a sequence for an X ∈ x can always be extended": if Δ fⁿ X, then Δ f^{n+1} X (prepend a Δ-step, using Δ f Δ).

theorem Domain.Neighborhood.ApproximableMap.rel_master_mono {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {n m : ℕ} (hnm : n ≤ m) {X : Set α} (h : (f.iterMap n).rel V.master X) : (f.iterMap m).rel V.master X

Monotonicity of the reachability relation in the number of steps: n ≤ m and Δ fⁿ X imply Δ fᵐ X.

Theorem 4.1 — the least fixed point.

def Domain.Neighborhood.ApproximableMap.fixElement {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : V.Element

Theorem 4.1 (Scott 1981, PRG-19). The least fixed point of f, Scott's x = {X ∈ 𝒟 ∣ Δ fⁿ X for some n}. The three filter conditions are exactly Scott's: Δ ∈ x (the n = 0 witness I_𝒟); closure under intersection follows from intersectivity (inter_right) of the single iterate f^{max n m} reached by extending the shorter chain; upward closure is mono.

Equations

• f.fixElement = { mem := fun (X : Set α) => ∃ (n : ℕ), (f.iterMap n).rel V.master X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.ApproximableMap.mem_fixElement {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {X : Set α} : f.fixElement.mem X ↔ ∃ (n : ℕ), (f.iterMap n).rel V.master X

theorem Domain.Neighborhood.ApproximableMap.toElementMap_fixElement {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : f.toElementMap f.fixElement = f.fixElement

Theorem 4.1 (Scott 1981, PRG-19). fixElement f is a fixed point: f(x) = x. f(x) ⊆ x appends an f-step (Δ f^{n+1} X from Δ fⁿ X' f X); x ⊆ f(x) reads off the last step of the chain (the empty chain forces X = Δ, handled by master_mem/master_rel).

theorem Domain.Neighborhood.ApproximableMap.fixElement_le_of_toElementMap_le {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {z : V.Element} (hz : f.toElementMap z ≤ z) : f.fixElement ≤ z

Theorem 4.1 (Scott 1981, PRG-19). fixElement f is the least pre-fixed point: if f(z) ⊆ z, then x ⊆ z. (Scott's induction: Δ ∈ z, and X ∈ z, X f Y give Y ∈ f(z) ⊆ z, so Δ fⁿ X implies X ∈ z.) In particular x is the least element with f(x) = x.

theorem Domain.Neighborhood.ApproximableMap.fixElement_mono {α : Type u_1} {V : NeighborhoodSystem α} {f g : ApproximableMap V V} (hfg : f ≤ g) : f.fixElement ≤ g.fixElement

The least fixed point is monotone in the map: f ⊑ g ⟹ fix(f) ⊑ fix(g) (immediate from iterMap_mono_map; underlies the approximability of fix in 4.2).

Theorem 4.2(iii) — the iterates fⁿ(⊥).

def Domain.Neighborhood.ApproximableMap.iterElem {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : V.Element

The n-th approximant fⁿ(⊥) of the least fixed point.

Equations

• f.iterElem n = (f.iterMap n).toElementMap V.bot

theorem Domain.Neighborhood.ApproximableMap.mem_iterElem {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) {X : Set α} : (f.iterElem n).mem X ↔ (f.iterMap n).rel V.master X

Y ∈ fⁿ(⊥) ↔ Δ fⁿ Y: the n-th approximant is the family of neighbourhoods reachable from Δ in exactly the n steps recorded by fⁿ.

theorem Domain.Neighborhood.ApproximableMap.iterElem_mono {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {n m : ℕ} (hnm : n ≤ m) : f.iterElem n ≤ f.iterElem m

The approximants form an increasing chain: n ≤ m ⟹ fⁿ(⊥) ⊑ fᵐ(⊥).

theorem Domain.Neighborhood.ApproximableMap.iterElem_eq_iterate {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.iterElem n = f.toElementMap^[n] V.bot

fⁿ(⊥) agrees with the iterated elementwise function (f(·))^[n] ⊥ — Scott's fⁿ(⊥).

theorem Domain.Neighborhood.ApproximableMap.fixElement_eq_iSupDirected {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : f.fixElement = NeighborhoodSystem.iSupDirected f.iterElem ⋯

Theorem 4.2(iii) (Scott 1981, PRG-19). fix(f) = ⊔ₙ fⁿ(⊥), here as the directed union of the increasing chain of approximants.

Theorem 4.2 — the approximable fixed-point operator fix.

def Domain.Neighborhood.fixMap {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (funSpace V V) V

Theorem 4.2 (Scott 1981, PRG-19). The fixed-point operator fix : (𝒟 → 𝒟) → 𝒟 as an approximable mapping. Built by the extension principle (Exercise 2.8, ofMono): on the finite element ↑F it returns fix(↑F), where ↑F = toApproxMap (principal hF) is the least map of the neighbourhood F (Proposition 3.9). Monotonicity of ↑F ↦ fix(↑F) is fixElement_mono composed with the order-iso funSpaceEquiv.

Equations

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

theorem Domain.Neighborhood.fixMap_toElementMap_principal {α : Type u_1} (V : NeighborhoodSystem α) {W : Set (ApproximableMap V V)} (hW : (funSpace V V).mem W) : (fixMap V).toElementMap ((funSpace V V).principal hW) = (toApproxMap ((funSpace V V).principal hW)).fixElement

On a finite element ↑F, fix returns fix(↑F) (the least fixed point of the least map of F).

theorem Domain.Neighborhood.exists_principal_iterMap {α : Type u_1} (V : NeighborhoodSystem α) (φ : (funSpace V V).Element) (n : ℕ) (X : Set α) : ((toApproxMap φ).iterMap n).rel V.master X → ∃ (W : Set (ApproximableMap V V)) (hw : φ.mem W), ((toApproxMap ((funSpace V V).principal ⋯)).iterMap n).rel V.master X

Theorem 4.2 (Scott 1981, PRG-19) — Scott's equation (∗), hard half. A finite f-chain Δ (toApproxMap φ)ⁿ X factors through a single finite approximant F ∈ φ: there is a neighbourhood W ∈ φ whose least map already realizes the same chain Δ (↑W)ⁿ X. The witness W is accumulated as the intersection of the (finitely many) step-neighbourhoods used by the chain, which lies in φ because φ is a filter.

theorem Domain.Neighborhood.fixMap_toElementMap {α : Type u_1} (V : NeighborhoodSystem α) (φ : (funSpace V V).Element) : (fixMap V).toElementMap φ = (toApproxMap φ).fixElement

Theorem 4.2 (Scott 1981, PRG-19) — Scott's equation (∗). The elementwise action of fix is the least fixed point of the corresponding map: fix.toElementMap φ = fix(toApproxMap φ). The forward inclusion (⊆ x) is exists_principal_iterMap; the reverse is monotonicity of fix along ↑W ⊑ toApproxMap φ.

theorem Domain.Neighborhood.fixMap_fixed {α : Type u_1} (V : NeighborhoodSystem α) (φ : (funSpace V V).Element) : (toApproxMap φ).toElementMap ((fixMap V).toElementMap φ) = (fixMap V).toElementMap φ

Theorem 4.2(i) (Scott 1981, PRG-19). fix(f) = f(fix(f)): the value of fix is a fixed point of the argument. (Equivalently eval(f, fix(f)) = fix(f) by evalMap_apply.)

theorem Domain.Neighborhood.fixMap_least {α : Type u_1} (V : NeighborhoodSystem α) (φ : (funSpace V V).Element) {z : V.Element} (hz : (toApproxMap φ).toElementMap z ≤ z) : (fixMap V).toElementMap φ ≤ z

Theorem 4.2(ii) (Scott 1981, PRG-19). f(x) ⊆ x ⟹ fix(f) ⊆ x: fix lands in the least pre-fixed point.

theorem Domain.Neighborhood.fixMap_eq_iSup {α : Type u_1} (V : NeighborhoodSystem α) (φ : (funSpace V V).Element) : (fixMap V).toElementMap φ = NeighborhoodSystem.iSupDirected (toApproxMap φ).iterElem ⋯

Theorem 4.2(iii) (Scott 1981, PRG-19). fix(f) = ⊔ₙ fⁿ(⊥) (as a directed union).

theorem Domain.Neighborhood.fixMap_toElementMap_toFilter {α : Type u_1} (V : NeighborhoodSystem α) (f : ApproximableMap V V) : (fixMap V).toElementMap (toFilter f) = f.fixElement

fix applied to (the filter of) an approximable map f returns the least fixed point of f. This is the bridge to the "for any f : 𝒟 → 𝒟" form of Theorem 4.2, using the Theorem 3.10 isomorphism toApproxMap (toFilter f) = f.

theorem Domain.Neighborhood.fixMap_unique {α : Type u_1} (V : NeighborhoodSystem α) (fax : ApproximableMap (funSpace V V) V) (h_fix : ∀ (φ : (funSpace V V).Element), (toApproxMap φ).toElementMap (fax.toElementMap φ) = fax.toElementMap φ) (h_least : ∀ (φ : (funSpace V V).Element) (z : V.Element), (toApproxMap φ).toElementMap z ≤ z → fax.toElementMap φ ≤ z) : fax = fixMap V

Theorem 4.2 (Scott 1981, PRG-19) — uniqueness. Any approximable operator fax satisfying (i) and (ii) coincides with fix. (Scott: from (i)(ii) one proves fix(f) ⊆ fax(f) and fax(f) ⊆ fix(f).)