Documentation

LeanPool.DomainTheory.Neighborhood.Exercise407

Exercise 4.7 (Scott 1981, PRG-19, Lecture IV) #

Formula 4.2(iii) gives the least fixed point fix(f) = ⊔ₙ fⁿ(⊥). Suppose instead that a ∈ |𝒟| satisfies a ⊑ f(a). Will there be a fixed point x = f(x) with a ⊑ x?

Yes. Replace ⊥ by a: the chain a ⊑ f(a) ⊑ f²(a) ⊑ … is increasing (monotonicity of f applied to a ⊑ f(a)), hence directed, so its union x = ⊔ₙ fⁿ(a) is a genuine element of |𝒟| (Scott's hint: this is why ⊔ makes sense — directed unions of filters are filters, Exercise 2.11 / iSupDirected). Approximable maps preserve directed unions (toElementMap_iSupDirected), which makes x a fixed point, and a = f⁰(a) ⊑ x by construction. Moreover x is the least fixed point above a (fixAbove_least), the relativized analogue of 4.2(iii).

All constructions are choice-free (#print axioms ⊆ {propext, Quot.sound}).

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

The chain of approximants from a base point a: iterFrom f a n = fⁿ(a).

Equations
Instances For
    source
    @[simp]
    theorem Domain.Neighborhood.ApproximableMap.iterFrom_zero {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (a : V.Element) :
    f.iterFrom a 0 = a
    source
    theorem Domain.Neighborhood.ApproximableMap.iterFrom_succ {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (a : V.Element) (n : ℕ) :
    f.iterFrom a (n + 1) = f.toElementMap (f.iterFrom a n)
    source
    theorem Domain.Neighborhood.ApproximableMap.iterFrom_step {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : a ≤ f.toElementMap a) (n : ℕ) :
    f.iterFrom a n ≤ f.iterFrom a (n + 1)

    One step of the chain: fⁿ(a) ⊑ fⁿ⁺¹(a) (proved choice-free by induction).

    source
    theorem Domain.Neighborhood.ApproximableMap.iterFrom_mono {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : a ≤ f.toElementMap a) {n m : ℕ} (hnm : n ≤ m) :
    f.iterFrom a n ≤ f.iterFrom a m

    When a ⊑ f(a), the chain fⁿ(a) is monotone: n ≤ m ⟹ fⁿ(a) ⊑ fᵐ(a). Proved by induction on n ≤ m (so as to stay choice-free, unlike monotone_nat_of_le_succ).

    source
    def Domain.Neighborhood.ApproximableMap.fixAbove {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : a ≤ f.toElementMap a) :
    V.Element

    The fixed point of f lying above a pre-fixed-point candidate a (with a ⊑ f(a)), constructed as the directed union ⊔ₙ fⁿ(a).

    Equations
    Instances For
      source
      theorem Domain.Neighborhood.ApproximableMap.le_fixAbove {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : a ≤ f.toElementMap a) :
      a ≤ f.fixAbove ha

      a ⊑ fixAbove f ha: the constructed fixed point lies above a (it is the n = 0 term).

      source
      theorem Domain.Neighborhood.ApproximableMap.fixAbove_isFixed {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : a ≤ f.toElementMap a) :
      f.toElementMap (f.fixAbove ha) = f.fixAbove ha

      Exercise 4.7 (Scott 1981, PRG-19). fixAbove f ha is a fixed point: f(x) = x.

      source
      theorem Domain.Neighborhood.ApproximableMap.fixAbove_least {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : a ≤ f.toElementMap a) {z : V.Element} (haz : a ≤ z) (hz : f.toElementMap z ≤ z) :
      f.fixAbove ha ≤ z

      Exercise 4.7 (Scott 1981, PRG-19). fixAbove f ha is the least fixed point above a: any z with a ⊑ z and f(z) ⊑ z lies above it. (Relativized form of 4.2(iii).)