Exercise 4.8 (Scott 1981, PRG-19, Lecture IV) — the principle of fixed-point

induction

Suppose f : 𝒟 → 𝒟 and a predicate S ⊆ |𝒟| satisfy

(i) ⊥ ∈ S; (ii) x ∈ S ⟹ f(x) ∈ S; (iii) S is closed under sups of increasing sequences.

Then fix(f) ∈ S. Since fix(f) = ⊔ₙ fⁿ(⊥) (Theorem 4.2(iii)), and f⁰(⊥) = ⊥ ∈ S with the inductive step fⁿ(⊥) ∈ S ⟹ fⁿ⁺¹(⊥) ∈ S from (i)/(ii), every approximant lies in S; the directed union then lies in S by (iii). This is fixed-point induction (fix_induction).

As Scott suggests, we apply it to S = {x ∣ a(x) = b(x)} (fix_induction_eq): if a, b : 𝒟 → 𝒟 are approximable with a(⊥) = b(⊥), f ∘ a = a ∘ f and f ∘ b = b ∘ f, then a(fix f) = b(fix f). (i) is a(⊥) = b(⊥); (ii) uses the commutation a(f x) = f(a x), b(f x) = f(b x); (iii) is continuity (a, b preserve directed unions, toElementMap_iSupDirected).

The induction principle is choice-free (#print axioms ⊆ {propext, Quot.sound}); the equality corollary inherits Classical.choice only through the Element extensionality used to compare the two directed unions.

def Domain.Neighborhood.ApproximableMap.supChain {α : Type u_1} {V : NeighborhoodSystem α} (s : ℕ → V.Element) (hmono : Monotone s) : V.Element

The sup of a monotone ω-chain, realized as a directed union (max-directedness).

Equations

• Domain.Neighborhood.ApproximableMap.supChain s hmono = Domain.Neighborhood.NeighborhoodSystem.iSupDirected s ⋯

theorem Domain.Neighborhood.ApproximableMap.mem_supChain {α : Type u_1} {V : NeighborhoodSystem α} (s : ℕ → V.Element) (hmono : Monotone s) {Z : Set α} : (supChain s hmono).mem Z ↔ ∃ (n : ℕ), (s n).mem Z

theorem Domain.Neighborhood.ApproximableMap.iterElem_succ {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (n : ℕ) : f.iterElem (n + 1) = f.toElementMap (f.iterElem n)

fⁿ⁺¹(⊥) = f(fⁿ(⊥)).

theorem Domain.Neighborhood.ApproximableMap.iterElem_zero {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) : f.iterElem 0 = V.bot

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

The approximants fⁿ(⊥) form a monotone chain whose sup is fix(f).

theorem Domain.Neighborhood.ApproximableMap.fix_induction {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (P : V.Element → Prop) (hbot : P V.bot) (hstep : ∀ (x : V.Element), P x → P (f.toElementMap x)) (hsup : ∀ (s : ℕ → V.Element) (hmono : Monotone s), (∀ (n : ℕ), P (s n)) → P (supChain s hmono)) : P f.fixElement

Exercise 4.8 (Scott 1981, PRG-19) — fixed-point induction. If a predicate P holds at ⊥, is preserved by f, and is closed under sups of monotone chains, then it holds at fix(f).

theorem Domain.Neighborhood.ApproximableMap.fix_induction_eq {α : Type u_1} {V : NeighborhoodSystem α} (f a b : ApproximableMap V V) (hbot : a.toElementMap V.bot = b.toElementMap V.bot) (hfa : f.comp a = a.comp f) (hfb : f.comp b = b.comp f) : a.toElementMap f.fixElement = b.toElementMap f.fixElement

Exercise 4.8 (Scott 1981, PRG-19) — application to S = {x ∣ a(x) = b(x)}. If a(⊥) = b(⊥) and f commutes with both a and b (f ∘ a = a ∘ f, f ∘ b = b ∘ f), then a and b agree at the least fixed point: a(fix f) = b(fix f).