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

The least fixed point of λx, y. ⟨τ(x, y), σ(x, y)⟩ is the pair with coordinates

!x. τ(x, !y. σ(x, y)) and !y. σ(!x. τ(x, y), y).

This is Bekić's theorem: the least solution of the simultaneous system x = τ(x, y), y = σ(x, y) is computed coordinatewise by nested least fixed points.

In this framework τ : 𝒟₀ × 𝒟₁ → 𝒟₀ and σ : 𝒟₀ × 𝒟₁ → 𝒟₁ are approximable, and the pair-valued map is F = ⟨τ, σ⟩ = paired τ σ : 𝒟₀ × 𝒟₁ → 𝒟₀ × 𝒟₁ whose least fixed point F.fixElement (Thm 4.1) is the least solution Scott invokes in his hint. We build:

• secFixX τ : 𝒟₁ → 𝒟₀, the approximable map y ↦ !x. τ(x, y) (fix ∘ curry(τ ∘ swap));
• outerOp τ σ : 𝒟₁ → 𝒟₁, the approximable map y ↦ σ(!x. τ(x, y), y);
• ystar = (outerOp τ σ).fixElement = !y. σ(!x. τ(x, y), y) and xstar = secFixX τ (ystar) = !x. τ(x, ystar).

The theorem fixElement_paired_eq states F.fixElement = ⟨xstar, ystar⟩, proved exactly as Scott: ⟨xstar, ystar⟩ is a fixed-point pair (so F.fixElement ⊑ ⟨xstar, ystar⟩), and from the least solution ⟨a, b⟩ one derives !x.τ(x,b) ⊑ a, hence outerOp(b) ⊑ b, hence ystar ⊑ b, hence xstar ⊑ a. All data is choice-free; the proof uses only the order on |𝒟ᵢ| and the universal properties of fixElement.

def Domain.Neighborhood.ApproximableMap.sectionX {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) (y : V₁.Element) : ApproximableMap V₀ V₀

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

Equations

• τ.sectionX y = Domain.Neighborhood.toApproxMap ((Domain.Neighborhood.curry (τ.comp (Domain.Neighborhood.swapC V₁ V₀))).toElementMap y)

theorem Domain.Neighborhood.ApproximableMap.sectionX_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) (y : V₁.Element) (x : V₀.Element) : (τ.sectionX y).toElementMap x = τ.toElementMap (pair x y)

def Domain.Neighborhood.ApproximableMap.secFixX {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) : ApproximableMap V₁ V₀

The approximable map y ↦ !x. τ(x, y): fix ∘ curry(τ ∘ swap).

Equations

• τ.secFixX = (Domain.Neighborhood.fixMap V₀).comp (Domain.Neighborhood.curry (τ.comp (Domain.Neighborhood.swapC V₁ V₀)))

theorem Domain.Neighborhood.ApproximableMap.secFixX_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) (y : V₁.Element) : τ.secFixX.toElementMap y = (τ.sectionX y).fixElement

theorem Domain.Neighborhood.ApproximableMap.secFixX_isFixed {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) (y : V₁.Element) : τ.toElementMap (pair (τ.secFixX.toElementMap y) y) = τ.secFixX.toElementMap y

!x. τ(x, y) is a fixed point of the section: τ(!x.τ(x,y), y) = !x.τ(x,y).

def Domain.Neighborhood.ApproximableMap.outerOp {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) (σ : ApproximableMap (prod V₀ V₁) V₁) : ApproximableMap V₁ V₁

The outer operator y ↦ σ(!x. τ(x, y), y).

Equations

• τ.outerOp σ = σ.comp (Domain.Neighborhood.paired τ.secFixX (Domain.Neighborhood.ApproximableMap.idMap V₁))

theorem Domain.Neighborhood.ApproximableMap.outerOp_apply {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) (σ : ApproximableMap (prod V₀ V₁) V₁) (y : V₁.Element) : (τ.outerOp σ).toElementMap y = σ.toElementMap (pair (τ.secFixX.toElementMap y) y)

theorem Domain.Neighborhood.ApproximableMap.fixElement_paired_eq {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (τ : ApproximableMap (prod V₀ V₁) V₀) (σ : ApproximableMap (prod V₀ V₁) V₁) : (paired τ σ).fixElement = pair (τ.secFixX.toElementMap (τ.outerOp σ).fixElement) (τ.outerOp σ).fixElement

Proposition 5.3 (Scott 1981, PRG-19). Bekić's theorem: the least fixed point of F = ⟨τ, σ⟩ is the pair ⟨!x.τ(x, !y.σ(x,y)-coordinate), !y.σ(!x.τ(x,y), y)⟩. Here the second coordinate is ystar = (outerOp τ σ).fixElement and the first is xstar = secFixX τ (ystar).