Exercise 5.11 (Scott 1981, PRG-19, §5) — D^∞ as stacks; stack combinators

Regarding D^∞ = iterSys D (Exercise 3.16) as (bottomless) stacks of elements of D, Scott asks for combinators with the obvious meanings

head : D^∞ → D,      tail : D^∞ → D^∞,      push : D × D^∞ → D^∞,

then for diag : D → D^∞ with diag(x) = ⟨x⟩ₙ (every component equal to x), defined by the recursion diag(x) = push(x, diag(x)), and finally a combinator

map : (D → D)^∞ × D → D^∞,      map(⟨fₙ⟩, x) = ⟨fₙ(x)⟩ₙ.

We build head, tail, push from the order-isomorphism iterProdIso : D^∞ ≅ D × D^∞ of Exercise 3.16 (so unfold = ofIso iterProdIso, fold = ofIso iterProdIso.symm), and obtain the stack laws

• head_push : head(push(x, s)) = x,
• tail_push : tail(push(x, s)) = s,
• push_head_tail : push(head z, tail z) = z,

together with the component readings head z = z₀ and (tail z)ₙ = zₙ₊₁.

diag and map are defined as least fixed points (Theorem 4.1/4.2); for diag we prove Scott's emphasised property that all components equal x (component_diag), and for map that the n-th component is fₙ(x) (component_map).

The only classical input is what is inherited from iterProdIso / fixMap and the project's Element.ext machinery.

unfold/fold from the isomorphism D^∞ ≅ D × D^∞.

def Domain.Neighborhood.Exercise511.unfold {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (iterSys V) (prod V (iterSys V))

unfold : D^∞ → D × D^∞, the forward direction of iterProdIso.

Equations

• Domain.Neighborhood.Exercise511.unfold V = Domain.Neighborhood.ApproximableMap.ofIso (Domain.Neighborhood.iterProdIso V)

def Domain.Neighborhood.Exercise511.fold {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (prod V (iterSys V)) (iterSys V)

fold : D × D^∞ → D^∞, the inverse direction of iterProdIso.

Equations

• Domain.Neighborhood.Exercise511.fold V = Domain.Neighborhood.ApproximableMap.ofIso (Domain.Neighborhood.iterProdIso V).symm

theorem Domain.Neighborhood.Exercise511.iterProdIso_apply {α : Type u_1} (V : NeighborhoodSystem α) (z : (iterSys V).Element) : (iterProdIso V) z = pair (component z 0) (ofSeq fun (n : ℕ) => component z (n + 1))

iterProdIso reads a stack as its head together with the tail sequence.

theorem Domain.Neighborhood.Exercise511.unfold_fold {α : Type u_1} (V : NeighborhoodSystem α) (p : (prod V (iterSys V)).Element) : (unfold V).toElementMap ((fold V).toElementMap p) = p

theorem Domain.Neighborhood.Exercise511.fold_unfold {α : Type u_1} (V : NeighborhoodSystem α) (z : (iterSys V).Element) : (fold V).toElementMap ((unfold V).toElementMap z) = z

The stack combinators.

def Domain.Neighborhood.Exercise511.head {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (iterSys V) V

head : D^∞ → D, the top of the stack.

Equations

• Domain.Neighborhood.Exercise511.head V = (Domain.Neighborhood.proj₀ V (Domain.Neighborhood.iterSys V)).comp (Domain.Neighborhood.Exercise511.unfold V)

def Domain.Neighborhood.Exercise511.tail {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (iterSys V) (iterSys V)

tail : D^∞ → D^∞, the stack with its top removed.

Equations

• Domain.Neighborhood.Exercise511.tail V = (Domain.Neighborhood.proj₁ V (Domain.Neighborhood.iterSys V)).comp (Domain.Neighborhood.Exercise511.unfold V)

def Domain.Neighborhood.Exercise511.push {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (prod V (iterSys V)) (iterSys V)

push : D × D^∞ → D^∞, prepend an element to a stack.

Equations

• Domain.Neighborhood.Exercise511.push V = Domain.Neighborhood.Exercise511.fold V

@[simp]

theorem Domain.Neighborhood.Exercise511.head_apply {α : Type u_1} (V : NeighborhoodSystem α) (z : (iterSys V).Element) : (head V).toElementMap z = component z 0

@[simp]

theorem Domain.Neighborhood.Exercise511.tail_apply {α : Type u_1} (V : NeighborhoodSystem α) (z : (iterSys V).Element) : (tail V).toElementMap z = ofSeq fun (n : ℕ) => component z (n + 1)

theorem Domain.Neighborhood.Exercise511.component_tail {α : Type u_1} (V : NeighborhoodSystem α) (z : (iterSys V).Element) (n : ℕ) : component ((tail V).toElementMap z) n = component z (n + 1)

(tail z)ₙ = zₙ₊₁.

theorem Domain.Neighborhood.Exercise511.head_push {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) (s : (iterSys V).Element) : (head V).toElementMap ((push V).toElementMap (pair x s)) = x

Stack law. head(push(x, s)) = x.

theorem Domain.Neighborhood.Exercise511.tail_push {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) (s : (iterSys V).Element) : (tail V).toElementMap ((push V).toElementMap (pair x s)) = s

Stack law. tail(push(x, s)) = s.

theorem Domain.Neighborhood.Exercise511.push_head_tail {α : Type u_1} (V : NeighborhoodSystem α) (z : (iterSys V).Element) : (push V).toElementMap (pair ((head V).toElementMap z) ((tail V).toElementMap z)) = z

Stack law. push(head z, tail z) = z (a stack is its top pushed onto its tail).

diag : D → D^∞, the constant stack ⟨x⟩ₙ, by recursion `diag(x) =

push(x, diag(x))`.

def Domain.Neighborhood.Exercise511.diag {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap V (iterSys V)

diag : D → D^∞, defined as the least fixed point of s ↦ push(x, s).

Equations

• Domain.Neighborhood.Exercise511.diag V = (Domain.Neighborhood.fixMap (Domain.Neighborhood.iterSys V)).comp (Domain.Neighborhood.curry (Domain.Neighborhood.Exercise511.push V))

theorem Domain.Neighborhood.Exercise511.diag_rec {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) : (diag V).toElementMap x = (push V).toElementMap (pair x ((diag V).toElementMap x))

Exercise 5.11 (Scott 1981, PRG-19). The recursion diag(x) = push(x, diag(x)).

theorem Domain.Neighborhood.Exercise511.component_diag {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) (n : ℕ) : component ((diag V).toElementMap x) n = x

Exercise 5.11 (Scott 1981, PRG-19). Scott's emphasised property: all components of diag(x) equal x, i.e. diag(x) = ⟨x⟩ₙ.

map : (D → D)^∞ × D → D^∞, map(⟨fₙ⟩, x) = ⟨fₙ(x)⟩ₙ, by recursion.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise511.Arg {α : Type u_1} (V : NeighborhoodSystem α) : NeighborhoodSystem (ℕ × ApproximableMap V V ⊕ α)

The argument domain of map: a stack of functions paired with a point, (D → D)^∞ × D.

Equations

• Domain.Neighborhood.Exercise511.Arg V = Domain.Neighborhood.prod (Domain.Neighborhood.iterSys (Domain.Neighborhood.funSpace V V)) V

def Domain.Neighborhood.Exercise511.mapBody {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (prod (funSpace (Arg V) (iterSys V)) (Arg V)) (iterSys V)

The body of the map recursion as a two-argument map M(W, ⟨s, x⟩) = push((head s)(x), W(tail s, x)), from which map = fix(curry M).

Equations

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

theorem Domain.Neighborhood.Exercise511.mapBody_apply {α : Type u_1} (V : NeighborhoodSystem α) (W : (funSpace (Arg V) (iterSys V)).Element) (s : (iterSys (funSpace V V)).Element) (x : V.Element) : (mapBody V).toElementMap (pair W (pair s x)) = (push V).toElementMap (pair ((toApproxMap ((head (funSpace V V)).toElementMap s)).toElementMap x) ((toApproxMap W).toElementMap (pair ((tail (funSpace V V)).toElementMap s) x)))

def Domain.Neighborhood.Exercise511.mapOp {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (funSpace (Arg V) (iterSys V)) (funSpace (Arg V) (iterSys V))

The map recursion operator R(W) = λ⟨s, x⟩. push((head s)(x), W(tail s, x)).

Equations

• Domain.Neighborhood.Exercise511.mapOp V = Domain.Neighborhood.curry (Domain.Neighborhood.Exercise511.mapBody V)

def Domain.Neighborhood.Exercise511.mapMap {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (Arg V) (iterSys V)

map : (D → D)^∞ × D → D^∞, the least fixed point of mapOp.

Equations

• Domain.Neighborhood.Exercise511.mapMap V = Domain.Neighborhood.toApproxMap (Domain.Neighborhood.Exercise511.mapOp V).fixElement

theorem Domain.Neighborhood.Exercise511.map_rec {α : Type u_1} (V : NeighborhoodSystem α) (s : (iterSys (funSpace V V)).Element) (x : V.Element) : (mapMap V).toElementMap (pair s x) = (push V).toElementMap (pair ((toApproxMap ((head (funSpace V V)).toElementMap s)).toElementMap x) ((mapMap V).toElementMap (pair ((tail (funSpace V V)).toElementMap s) x)))

Exercise 5.11 (Scott 1981, PRG-19). The recursion defining map: map(s, x) = push((head s)(x), map(tail s, x)).

theorem Domain.Neighborhood.Exercise511.component_map {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) (n : ℕ) (s : (iterSys (funSpace V V)).Element) : component ((mapMap V).toElementMap (pair s x)) n = (toApproxMap (component s n)).toElementMap x

Exercise 5.11 (Scott 1981, PRG-19). The n-th component of map(s, x) is (component s n)(x), i.e. map(⟨fₙ⟩, x) = ⟨fₙ(x)⟩ₙ.