Documentation

LeanPool.DomainTheory.Neighborhood.Exercise412

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

Need an approximable f : 𝒟 → 𝒟 have a maximum fixed point? Give an example where there are many fixed points.

No. The identity map I_𝒟 has every element as a fixed point. Taking 𝒟 to be Scott's Example 1.2 (the fork T with ⊥ ⊏ {0}-total, ⊥ ⊏ {1}-total and the two total elements incomparable), I_T has three fixed points ⊥, elemZero, elemOne; the two total ones are maximal and incomparable, so there is no greatest fixed point (no_greatest_fixedPoint) — in particular no maximum. This is the simplest counterexample to "a least fixed point is a maximum fixed point".

Uses Classical.choice only through Example 1.2's finite fin_cases/simp classification, exactly as that file does.

source
@[reducible, inline]
abbrev Domain.Neighborhood.Exercise412.T :
NeighborhoodSystem Example12.Token

Abbreviation for Example 1.2's domain T.

Equations
Instances For
    source
    theorem Domain.Neighborhood.Exercise412.elemOne_not_le_elemZero :
    ¬Example12.neighborhoodSystem.elemOne ≤ Example12.neighborhoodSystem.elemZero

    The two total elements are incomparable: elemOne ⋢ elemZero.

    source
    theorem Domain.Neighborhood.Exercise412.elemZero_not_le_elemOne :
    ¬Example12.neighborhoodSystem.elemZero ≤ Example12.neighborhoodSystem.elemOne

    The two total elements are incomparable: elemZero ⋢ elemOne.

    source
    theorem Domain.Neighborhood.Exercise412.idMap_fixed (x : T.Element) :
    (ApproximableMap.idMap T).toElementMap x = x

    Exercise 4.12 (Scott 1981, PRG-19). Every element is a fixed point of the identity map (so I_T has many fixed points: ⊥, elemZero, elemOne).

    source
    theorem Domain.Neighborhood.Exercise412.no_greatest_fixedPoint :
    ¬∃ (z : T.Element), (ApproximableMap.idMap T).toElementMap z = z ∧ ∀ (x : T.Element), (ApproximableMap.idMap T).toElementMap x = x → x ≤ z

    Exercise 4.12 (Scott 1981, PRG-19). I_T has no greatest (hence no maximum) fixed point: the two total elements elemZero, elemOne are both fixed points, are incomparable, and no element dominates both.