Exercise 4.11 (Scott 1981, PRG-19, Lecture IV) — Plotkin's uniqueness of fix

(Suggested by G. Plotkin.) Regard fix as assigning a fixed-point operator F_𝒟 : (𝒟 → 𝒟) → 𝒟 to each domain 𝒟. Scott asks to show fix is the unique such assignment 𝒟 ↝ F_𝒟 subject to:

• (i) F_𝒟 : (𝒟 → 𝒟) → 𝒟;
• (ii) F_𝒟(f) = f(F_𝒟(f)) for all f : 𝒟 → 𝒟 (each value is a fixed point);
• (iii) (uniformity) whenever f₀ : 𝒟₀ → 𝒟₀, f₁ : 𝒟₁ → 𝒟₁ and h : 𝒟₀ → 𝒟₁ satisfy h(⊥) = ⊥ and h ∘ f₀ = f₁ ∘ h, then h(F_{𝒟₀}(f₀)) = F_{𝒟₁}(f₁).

fix satisfies (iii) (fixElement_uniform): writing fix(f₀) = ⊔ₙ f₀ⁿ(⊥) (Theorem 4.2(iii)), the intertwining h ∘ f₀ = f₁ ∘ h together with h(⊥) = ⊥ gives h(f₀ⁿ(⊥)) = f₁ⁿ(⊥) by induction, and h preserves directed unions, so h(fix f₀) = ⊔ₙ f₁ⁿ(⊥) = fix f₁.

Uniqueness (fix_unique_of_uniform): given any F obeying (ii) and (iii), and any f : 𝒟 → 𝒟, apply (iii) with the inclusion h = ι : 𝒟_{fix f} ↪ 𝒟 of the relativized domain (Exercise 4.10). ι(⊥) = ⊥ (inclMap_bot) and ι ∘ f' = f ∘ ι (inclMap_intertwine, from relMap_toElementMap_embed). Hence ι(F_{𝒟_{fix f}}(f')) = F_𝒟(f). But F_{𝒟_{fix f}}(f') is a fixed point of f' by (ii), and f' has exactly one fixed point (Exercise 4.10, relMap_unique_fixed) — the top point fix f — so the left side is ι(fix f) = fix f. Therefore F_𝒟(f) = fix f.

fix satisfying (i)/(ii) is Theorem 4.2 (fixMap, fixMap_fixed). The uniqueness proof uses only the project's permitted Element.ext; the inclusion data inclMap is choice-free.

fix satisfies the uniformity condition (iii).

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

fⁿ(⊥) ⊑ fix(f): every approximant lies below the least fixed point.

theorem Domain.Neighborhood.ApproximableMap.fixElement_uniform {β : Type u_2} {γ : Type u_3} {W₀ : NeighborhoodSystem β} {W₁ : NeighborhoodSystem γ} (f₀ : ApproximableMap W₀ W₀) (f₁ : ApproximableMap W₁ W₁) (h : ApproximableMap W₀ W₁) (hbot : h.toElementMap W₀.bot = W₁.bot) (hintw : ∀ (x : W₀.Element), h.toElementMap (f₀.toElementMap x) = f₁.toElementMap (h.toElementMap x)) : h.toElementMap f₀.fixElement = f₁.fixElement

Exercise 4.11(iii) (Scott 1981, PRG-19). fix is uniform: if h(⊥) = ⊥ and h ∘ f₀ = f₁ ∘ h, then h(fix f₀) = fix f₁.

The inclusion ι : 𝒟ₐ ↪ 𝒟 of the relativized domain (Exercise 4.10).

def Domain.Neighborhood.ApproximableMap.inclMap {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) : ApproximableMap (relSystem a) V

The inclusion 𝒟ₐ → 𝒟 as an approximable map: an a-neighbourhood X relates to any larger 𝒟-neighbourhood Y ⊇ X. Its elementwise action is embed a (inclMap_toElementMap).

Equations

• Domain.Neighborhood.ApproximableMap.inclMap a = { rel := fun (X Y : Set α) => a.mem X ∧ V.mem Y ∧ X ⊆ Y, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

theorem Domain.Neighborhood.ApproximableMap.inclMap_toElementMap {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (g : (relSystem a).Element) : (inclMap a).toElementMap g = embed a g

The inclusion's elementwise action is embed a (Exercise 4.10).

theorem Domain.Neighborhood.ApproximableMap.inclMap_bot {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) : (inclMap a).toElementMap (relSystem a).bot = V.bot

The inclusion is strict: ι(⊥) = ⊥.

theorem Domain.Neighborhood.ApproximableMap.inclMap_intertwine {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : f.toElementMap a = a) (g : (relSystem a).Element) : (inclMap a).toElementMap ((f.relMap ha).toElementMap g) = f.toElementMap ((inclMap a).toElementMap g)

The inclusion intertwines f' with f: ι ∘ f' = f ∘ ι (from relMap_toElementMap_embed).

Plotkin's uniqueness theorem.

theorem Domain.Neighborhood.fix_unique_of_uniform (F : {β : Type u} → (W : NeighborhoodSystem β) → ApproximableMap W W → W.Element) (hfixed : ∀ {β : Type u} (W : NeighborhoodSystem β) (g : ApproximableMap W W), g.toElementMap (F W g) = F W g) (huniform : ∀ {β γ : Type u} (W₀ : NeighborhoodSystem β) (W₁ : NeighborhoodSystem γ) (g₀ : ApproximableMap W₀ W₀) (g₁ : ApproximableMap W₁ W₁) (h : ApproximableMap W₀ W₁), h.toElementMap W₀.bot = W₁.bot → (∀ (x : W₀.Element), h.toElementMap (g₀.toElementMap x) = g₁.toElementMap (h.toElementMap x)) → h.toElementMap (F W₀ g₀) = F W₁ g₁) {α : Type u} (V : NeighborhoodSystem α) (f : ApproximableMap V V) : F V f = f.fixElement

Exercise 4.11 (Scott 1981, PRG-19) — Plotkin's uniqueness. Any assignment F of a fixed-point operator to every domain satisfying (ii) F_𝒟(f) = f(F_𝒟(f)) and (iii) the uniformity law coincides with fix: F_𝒟(f) = fix(f) for every domain 𝒟 and every f : 𝒟 → 𝒟.