Exercise 4.9 (Scott 1981, PRG-19, Lecture IV) — the operator Ψ and `fix =

fix(Ψ)`

Scott asks for an approximable operator

Ψ : ((𝒟 → 𝒟) → 𝒟) → ((𝒟 → 𝒟) → 𝒟) with Ψ(θ)(f) = f(θ(f)),

and then to prove that fix : (𝒟 → 𝒟) → 𝒟 is the least fixed point of Ψ — the true equation fix = fix(λF λf. f(F(f))) (cf. the text following Exercise 4.9).

Construction. Writing G = (𝒟 → 𝒟) and E = (G → 𝒟), the term λF λf. f(F(f)) is built from the cartesian-closed combinators: Ψ = curry Φ where Φ : E × G → 𝒟 is Φ = eval_{𝒟,𝒟} ∘ ⟨π_G, eval_{G,𝒟}⟩, sending ⟨F, f⟩ ↦ f(F(f)). Approximability is automatic (bigPsi); the defining equation Ψ(θ)(f) = f(θ(f)) is bigPsi_apply (Theorem 3.12's curry β-rule plus the eval/projection laws).

fix = fix(Ψ). Representing fix as the element toFilter (fixMap V) ∈ |E|:

• bigPsi_fix — Ψ(fix) = fix: indeed Ψ(fix)(f) = f(fix(f)) = f(fix f) = fix f = fix(f) since fix(f) = fix f is a fixed point of f (Theorem 4.1);
• bigPsi_least — if Ψ(θ) ⊑ θ then fix ⊑ θ: pointwise, Ψ(θ)(f) = f(θ(f)) ⊑ θ(f) makes θ(f) a pre-fixed point of f, so fix f ⊑ θ(f) (Theorem 4.1's minimality), i.e. fix(f) ⊑ θ(f);
• fix_eq_fixElement_bigPsi — combining the two, fix = fix(Ψ) (= fixElement Ψ, Theorem 4.1's canonical least fixed point).

The operator data bigPsi is choice-free; equalities of elements/operators go through the project's permitted Element.ext / ext_of_toElementMap.

def Domain.Neighborhood.bigPsi {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (funSpace (funSpace V V) V) (funSpace (funSpace V V) V)

Exercise 4.9 (Scott 1981, PRG-19). The approximable operator Ψ = λF λf. f(F(f)) on the higher-order domain E = ((𝒟 → 𝒟) → 𝒟), built as curry (eval ∘ ⟨π_G, eval⟩).

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.bigPsi_apply {α : Type u_1} (V : NeighborhoodSystem α) (θ : (funSpace (funSpace V V) V).Element) (f : (funSpace V V).Element) : (toApproxMap ((bigPsi V).toElementMap θ)).toElementMap f = (toApproxMap f).toElementMap ((toApproxMap θ).toElementMap f)

Exercise 4.9 (Scott 1981, PRG-19). The defining equation Ψ(θ)(f) = f(θ(f)).

theorem Domain.Neighborhood.toApproxMap_toFilter_fixMap {α : Type u_1} (V : NeighborhoodSystem α) : toApproxMap (toFilter (fixMap V)) = fixMap V

fix, as the element of E = ((𝒟 → 𝒟) → 𝒟) corresponding to the operator fixMap, unfolds under toApproxMap back to fixMap (the funSpace round-trip).

theorem Domain.Neighborhood.bigPsi_fix {α : Type u_1} (V : NeighborhoodSystem α) : (bigPsi V).toElementMap (toFilter (fixMap V)) = toFilter (fixMap V)

Exercise 4.9 (Scott 1981, PRG-19). fix is a fixed point of Ψ: Ψ(fix) = fix.

theorem Domain.Neighborhood.bigPsi_least {α : Type u_1} (V : NeighborhoodSystem α) (θ : (funSpace (funSpace V V) V).Element) (hθ : (bigPsi V).toElementMap θ ≤ θ) : toFilter (fixMap V) ≤ θ

Exercise 4.9 (Scott 1981, PRG-19). fix is the least pre-fixed point of Ψ: any θ with Ψ(θ) ⊑ θ satisfies fix ⊑ θ.

theorem Domain.Neighborhood.fix_eq_fixElement_bigPsi {α : Type u_1} (V : NeighborhoodSystem α) : toFilter (fixMap V) = (bigPsi V).fixElement

Exercise 4.9 (Scott 1981, PRG-19). fix = fix(Ψ): fix is the least fixed point of Ψ, i.e. coincides with Theorem 4.1's canonical least fixed point fixElement Ψ.