Lecture V (§5) — Proposition 5.4 (Scott 1981, PRG-19)

Let x, y, and τ(x, y) have the same type 𝒟, and let g range over (𝒟 → 𝒟). Then the equation

λx. !y. τ(x, y) = !g. λx. τ(x, g(x))

is true.

In this framework τ : 𝒟 × 𝒟 → 𝒟 is an approximable map. We model the two sides directly:

• the left side λx. !y. τ(x, y) is pfix τ := fix ∘ curry(τ), the approximable map sending x to the least fixed point of the section y ↦ τ(x, y) (this is !y.τ(x,y), manifestly approximable by Theorem 4.2 — exactly Scott's appeal to 5.1 that "f is a function");
• the right side !g. λx. τ(x, g(x)) is the least fixed point (recOp τ).fixElement of the approximable operator recOp τ := curry(τ ∘ ⟨p₁, eval⟩) on the function space, which sends a map g to λx. τ(x, g(x)).

The proof is Scott's: pfix τ is a fixed point of recOp τ (so !g.… ⊑ pfix τ), and conversely the value (recOp τ).fixElement (x) is a fixed point of the section y ↦ τ(x, y) (so pfix τ (x) ⊑ (recOp τ).fixElement (x) for every x). Everything is at the level of |𝒟| and the function space, so the data (pfix, recOp) is choice-free (#print axioms ⊆ {propext, Quot.sound}); the final map equality goes through the permitted ext_of_toElementMap.

def Domain.Neighborhood.ApproximableMap.section₂ {α : Type u_1} {V : NeighborhoodSystem α} (τ : ApproximableMap (prod V V) V) (x : V.Element) : ApproximableMap V V

The section y ↦ τ(x, y) of τ : 𝒟 × 𝒟 → 𝒟 at a fixed x, as an approximable endomap of 𝒟 (the curried τ applied to x).

Equations

• τ.section₂ x = Domain.Neighborhood.toApproxMap ((Domain.Neighborhood.curry τ).toElementMap x)

theorem Domain.Neighborhood.ApproximableMap.section₂_apply {α : Type u_1} {V : NeighborhoodSystem α} (τ : ApproximableMap (prod V V) V) (x y : V.Element) : (τ.section₂ x).toElementMap y = τ.toElementMap (pair x y)

def Domain.Neighborhood.ApproximableMap.pfix {α : Type u_1} {V : NeighborhoodSystem α} (τ : ApproximableMap (prod V V) V) : ApproximableMap V V

The left-hand side λx. !y. τ(x, y) of Proposition 5.4: fix ∘ curry(τ).

Equations

• τ.pfix = (Domain.Neighborhood.fixMap V).comp (Domain.Neighborhood.curry τ)

theorem Domain.Neighborhood.ApproximableMap.pfix_apply {α : Type u_1} {V : NeighborhoodSystem α} (τ : ApproximableMap (prod V V) V) (x : V.Element) : τ.pfix.toElementMap x = (τ.section₂ x).fixElement

pfix τ (x) = !y. τ(x, y), the least fixed point of the section at x.

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

The operator λg. λx. τ(x, g(x)) of Proposition 5.4, as an approximable endomap of the function space (𝒟 → 𝒟): recOp τ := curry(τ ∘ ⟨p₁, eval⟩).

Equations

• τ.recOp = Domain.Neighborhood.curry (τ.comp (Domain.Neighborhood.paired (Domain.Neighborhood.proj₁ (Domain.Neighborhood.funSpace V V) V) (Domain.Neighborhood.evalMap V V)))

theorem Domain.Neighborhood.ApproximableMap.recOp_apply {α : Type u_1} {V : NeighborhoodSystem α} (τ : ApproximableMap (prod V V) V) (φ : (funSpace V V).Element) (x : V.Element) : (toApproxMap (τ.recOp.toElementMap φ)).toElementMap x = τ.toElementMap (pair x ((toApproxMap φ).toElementMap x))

recOp τ (g) (x) = τ(x, g(x)).

theorem Domain.Neighborhood.ApproximableMap.pfix_isFixed {α : Type u_1} {V : NeighborhoodSystem α} (τ : ApproximableMap (prod V V) V) (x : V.Element) : τ.toElementMap (pair x (τ.pfix.toElementMap x)) = τ.pfix.toElementMap x

pfix τ is a fixed point of recOp τ (pointwise: τ(x, pfix τ x) = pfix τ x).

theorem Domain.Neighborhood.ApproximableMap.pfix_eq_fixElement_recOp {α : Type u_1} {V : NeighborhoodSystem α} (τ : ApproximableMap (prod V V) V) : τ.pfix = toApproxMap τ.recOp.fixElement

Proposition 5.4 (Scott 1981, PRG-19). λx. !y. τ(x, y) = !g. λx. τ(x, g(x)).