Exercise 4.16 (Scott 1981, PRG-19, Lecture IV) — the optimal fixed point

(For fixed-point nuts.) Scott's step (1): for any non-empty set S of fixed points of a monotone f : |𝒟| → |𝒟|, the greatest lower bound ⋂S (Exercise 1.18 sInf) satisfies

f(⋂S) ⊑ ⋂S (f_sInf_le)

— indeed f(⋂S) ⊑ f(s) = s for each s ∈ S, so f(⋂S) is a lower bound of S. Being a pre-fixed point, ⋂S carries (Exercise 4.13(1)'s monoFix) the least fixed point optimalFix S with

optimalFix S ⊑ ⋂S ⊑ s for every s ∈ S (optimalFix_le),

so optimalFix S is a fixed point lying below every member of S, and it is consistent with each s ∈ S (their common upper bound is s itself, optimalFix_consistent). Taking S to be the set of maximal fixed points (which exist by Exercise 4.15) gives the fixed point that is below all the maximal ones, consistent with all other fixed points — Scott's "optimal" fixed point.

The data (optimalFix) is choice-free; only the appeal to Exercise 4.15 for the supply of maximal fixed points is classical.

theorem Domain.Neighborhood.NeighborhoodSystem.f_sInf_le {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) (S : Set V.Element) (hS : S.Nonempty) (hfix : ∀ s ∈ S, f s = s) : f (V.sInf S hS) ≤ V.sInf S hS

Exercise 4.16(1) (Scott 1981, PRG-19). Scott's formula: for a non-empty set S of fixed points, f(⋂S) ⊑ ⋂S. (f(⋂S) ⊑ f(s) = s for each s ∈ S, then take the glb.)

def Domain.Neighborhood.NeighborhoodSystem.optimalFix {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) (S : Set V.Element) (hS : S.Nonempty) (hfix : ∀ s ∈ S, f s = s) : V.Element

Exercise 4.16 (Scott 1981, PRG-19). The optimal fixed point associated with a non-empty set S of fixed points: the least fixed point sitting below ⋂S (Exercise 4.13(1) applied to the pre-fixed point ⋂S).

Equations

• Domain.Neighborhood.NeighborhoodSystem.optimalFix f hf S hS hfix = Domain.Neighborhood.NeighborhoodSystem.monoFix f ⋯

theorem Domain.Neighborhood.NeighborhoodSystem.optimalFix_isFixed {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) (S : Set V.Element) (hS : S.Nonempty) (hfix : ∀ s ∈ S, f s = s) : f (optimalFix f hf S hS hfix) = optimalFix f hf S hS hfix

optimalFix S is a fixed point.

theorem Domain.Neighborhood.NeighborhoodSystem.optimalFix_le_sInf {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) (S : Set V.Element) (hS : S.Nonempty) (hfix : ∀ s ∈ S, f s = s) : optimalFix f hf S hS hfix ≤ V.sInf S hS

optimalFix S ⊑ ⋂S.

theorem Domain.Neighborhood.NeighborhoodSystem.optimalFix_le {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) (S : Set V.Element) (hS : S.Nonempty) (hfix : ∀ s ∈ S, f s = s) {s : V.Element} (hs : s ∈ S) : optimalFix f hf S hS hfix ≤ s

Exercise 4.16 (Scott 1981, PRG-19). optimalFix S lies below every member of S.

theorem Domain.Neighborhood.NeighborhoodSystem.optimalFix_consistent {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) (S : Set V.Element) (hS : S.Nonempty) (hfix : ∀ s ∈ S, f s = s) {s : V.Element} (hs : s ∈ S) : ∃ (ub : V.Element), optimalFix f hf S hS hfix ≤ ub ∧ s ≤ ub

Exercise 4.16 (Scott 1981, PRG-19). optimalFix S is consistent with every member of S (they share a common upper bound, namely s itself).