Exercise 5.12 (Scott 1981, PRG-19, §5) — the while combinator

Given a domain D, a predicate p : D → T (into the truth domain of Example 1.2) and an update f : D → D, Scott's while-loop

while p do f

is the function D → D that keeps applying f while p holds. It is characterised as the least solution w : D → D of the recursion

w(x) = cond(p(x), w(f(x)), x).

We realise this semantically inside the approximable-map framework: the right-hand side, read as a function of the unknown w, is an approximable operator

Wop : (D → D) → (D → D),   Wop(w) = λx. cond(p(x), w(f(x)), x),

built from the conditional cond of Exercise 3.26, evaluation eval, the projections, pairing and composition. The loop is then whileFix = fixElement Wop, the least fixed point of Wop (Theorem 4.1), and whileMap = toApproxMap whileFix : D → D the approximable function it denotes.

We prove:

• whileMap_rec — the defining recursion w(x) = cond(p(x), w(f(x)), x);
• whileMap_true — if p(x) = true then w(x) = w(f(x)) (loop body runs);
• whileMap_false — if p(x) = false then w(x) = x (loop exits);
• whileMap_bot — if p(x) = ⊥ then w(x) = ⊥ (divergent test diverges);
• whileMap_least — leastness: any w' satisfying the recursion dominates whileMap.

Everything is choice-free in spirit; the only classical input is inherited from cond/T (Example 1.2) and the project's Element.ext / ext_of_toElementMap machinery.

def Domain.Neighborhood.Exercise512.bodyMap {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) : ApproximableMap (prod (funSpace V V) V) V

The body of the loop as a two-argument map M : (D → D) × D → D, M(w, x) = cond(p(x), w(f(x)), x). It is assembled from cond, eval, the projections, pairing and composition, hence approximable.

Equations

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

theorem Domain.Neighborhood.Exercise512.bodyMap_apply {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) (w : (funSpace V V).Element) (x : V.Element) : (bodyMap V p f).toElementMap (pair w x) = (Exercise326.cond V).toElementMap (pair (p.toElementMap x) (pair ((toApproxMap w).toElementMap (f.toElementMap x)) x))

Value of the loop body: M(w, x) = cond(p(x), w(f(x)), x).

def Domain.Neighborhood.Exercise512.Wop {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) : ApproximableMap (funSpace V V) (funSpace V V)

The loop operator Wop : (D → D) → (D → D), Wop(w) = λx. cond(p(x), w(f(x)), x).

Equations

• Domain.Neighborhood.Exercise512.Wop V p f = Domain.Neighborhood.curry (Domain.Neighborhood.Exercise512.bodyMap V p f)

theorem Domain.Neighborhood.Exercise512.Wop_apply {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) (w : (funSpace V V).Element) (x : V.Element) : (toApproxMap ((Wop V p f).toElementMap w)).toElementMap x = (Exercise326.cond V).toElementMap (pair (p.toElementMap x) (pair ((toApproxMap w).toElementMap (f.toElementMap x)) x))

Wop(w)(x) = cond(p(x), w(f(x)), x).

def Domain.Neighborhood.Exercise512.whileFix {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) : (funSpace V V).Element

The while-loop element of the function space D → D: the least fixed point of Wop.

Equations

• Domain.Neighborhood.Exercise512.whileFix V p f = (Domain.Neighborhood.Exercise512.Wop V p f).fixElement

def Domain.Neighborhood.Exercise512.whileMap {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) : ApproximableMap V V

The approximable function while p do f : D → D denoted by whileFix.

Equations

• Domain.Neighborhood.Exercise512.whileMap V p f = Domain.Neighborhood.toApproxMap (Domain.Neighborhood.Exercise512.whileFix V p f)

theorem Domain.Neighborhood.Exercise512.whileMap_rec {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) (x : V.Element) : (whileMap V p f).toElementMap x = (Exercise326.cond V).toElementMap (pair (p.toElementMap x) (pair ((whileMap V p f).toElementMap (f.toElementMap x)) x))

Exercise 5.12 (Scott 1981, PRG-19). The defining recursion of the while-loop: w(x) = cond(p(x), w(f(x)), x).

theorem Domain.Neighborhood.Exercise512.whileMap_true {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) {x : V.Element} (hx : p.toElementMap x = Example23.trueElt) : (whileMap V p f).toElementMap x = (whileMap V p f).toElementMap (f.toElementMap x)

If the test holds (p(x) = true), the loop runs the body: w(x) = w(f(x)).

theorem Domain.Neighborhood.Exercise512.whileMap_false {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) {x : V.Element} (hx : p.toElementMap x = Example23.falseElt) : (whileMap V p f).toElementMap x = x

If the test fails (p(x) = false), the loop exits: w(x) = x.

theorem Domain.Neighborhood.Exercise512.whileMap_bot {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) {x : V.Element} (hx : p.toElementMap x = Example23.botElt) : (whileMap V p f).toElementMap x = V.bot

If the test diverges (p(x) = ⊥), the loop diverges: w(x) = ⊥.

theorem Domain.Neighborhood.Exercise512.whileMap_least {α : Type u_1} (V : NeighborhoodSystem α) (p : ApproximableMap V Exercise326.TD) (f : ApproximableMap V V) (w' : (funSpace V V).Element) (hw' : ∀ (x : V.Element), (toApproxMap w').toElementMap x = (Exercise326.cond V).toElementMap (pair (p.toElementMap x) (pair ((toApproxMap w').toElementMap (f.toElementMap x)) x))) : whileFix V p f ≤ w'

Leastness. Any w' satisfying the while-recursion w'(x) = cond(p(x), w'(f(x)), x) dominates the least solution whileMap.