Exercise 6.22 (Scott 1981, PRG-19, §6) — commenting on three domain equations

EXERCISE 6.22. Comment on these domain equations: N ≅ {{0}, {0, Λ}} ⊕ N, M ≅ {{Λ}} + M, N* ≅ N ⊕ (N ⊗ N*).

This is a "comment on" exercise, so the substantive formal content is to recognise each equation as an instance of the fixed-point machinery built in Exercises 6.19–6.21. Every right-hand side is a construct T(X) of the algebra GExpr (constants, identity, +, ×, ⊕, ⊗), whose constants are rooted (contain Λ). Hence by gExists_singleton_subsystem (Exercise 6.21/6.20) there is a token set Γ with Γ = tok(T({Γ})), so {Γ} ◁ T({Γ}) and Theorem 6.14 applies: each equation has a solution.

What the three domains are (the "comment")

• N ≅ {{0},{0,Λ}} ⊕ N. The constant {{0},{0,Λ}} is the two-point domain (a chain {0} ⊏ Δ, i.e. one proper point above the bottom). Folding it under the coalesced sum ⊕ — which identifies the bottoms at each stage — stacks the proper points into a single chain. So N is the domain of vertical natural numbers: a chain ⊥ ⊑ 0 ⊑ 1 ⊑ ⋯ topped by a limit ∞.
• M ≅ {{Λ}} + M. The constant {{Λ}} is the one-point domain 𝟙 (the terminal object). Folding it under the separated sum + — which keeps the two bottoms apart, offering a genuine stop/continue choice at each step — yields the lazy natural numbers: each n is a distinct partial element succⁿ(stop), with ⊥ below every finite stage and one infinite element. The only difference from N is coalesced vs. separated: ⊕ collapses the choice into a chain, + keeps it branching.
• N* ≅ N ⊕ (N ⊗ N*). With the smash product ⊗ (strict pairing: a pair is ⊥ unless both coordinates are proper) and the coalesced ⊕, this is the cons-cell equation X ≅ N ⊕ (N ⊗ X): an element is either a single datum from N or a strict head/tail pair. So N* is the domain of finite and infinite strict sequences (streams) over N.

All three solutions are obtained uniformly below; the only per-equation work is exhibiting the constant systems {{0},{0,Λ}}, {{Λ}} and checking they are ∅-free and rooted. Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The two constant domains

def Domain.Neighborhood.Exercise619.Cnat : ScottSys

The two-point generator {{0},{0,Λ}}. Its tokens are Δ = {0,Λ}, with the one proper neighbourhood {0} sitting strictly below the master {0,Λ} = Δ. As a domain this is the chain {0} ⊏ Δ (one point above the bottom). Here 0 = [false] and Λ = [].

Equations

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

theorem Domain.Neighborhood.Exercise619.nil_mem_Cnat : [] ∈ Cnat.sys.master

Λ ∈ tok(Cnat), so Cnat is a rooted constant.

def Domain.Neighborhood.Exercise619.Cone : ScottSys

The one-point domain {{Λ}} = 𝟙 (the terminal object of Scott's category).

Equations

• Domain.Neighborhood.Exercise619.Cone = Domain.Neighborhood.Exercise619.singletonSys {[]} Domain.Neighborhood.Exercise619.Cone._proof_1

theorem Domain.Neighborhood.Exercise619.nil_mem_Cone : [] ∈ Cone.sys.master

Λ ∈ tok(Cone).

The three domain equations as GExpr constructs

def Domain.Neighborhood.Exercise619.NExpr : GExpr

T(X) = {{0},{0,Λ}} ⊕ X — the right-hand side of N ≅ {{0},{0,Λ}} ⊕ N.

Equations

• Domain.Neighborhood.Exercise619.NExpr = (Domain.Neighborhood.Exercise619.GExpr.const Domain.Neighborhood.Exercise619.Cnat).oplus Domain.Neighborhood.Exercise619.GExpr.var

def Domain.Neighborhood.Exercise619.MExpr : GExpr

T(X) = {{Λ}} + X — the right-hand side of M ≅ {{Λ}} + M.

Equations

• Domain.Neighborhood.Exercise619.MExpr = (Domain.Neighborhood.Exercise619.GExpr.const Domain.Neighborhood.Exercise619.Cone).sum Domain.Neighborhood.Exercise619.GExpr.var

def Domain.Neighborhood.Exercise619.NStarExpr (N : ScottSys) : GExpr

T(X) = N ⊕ (N ⊗ X) — the right-hand side of N* ≅ N ⊕ (N ⊗ N*), parametrised by the (rooted) datum domain N.

Equations

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

theorem Domain.Neighborhood.Exercise619.NExpr_rooted : NExpr.RootedConst

theorem Domain.Neighborhood.Exercise619.MExpr_rooted : MExpr.RootedConst

theorem Domain.Neighborhood.Exercise619.NStarExpr_rooted {N : ScottSys} (hN : [] ∈ N.sys.master) : (NStarExpr N).RootedConst

Each equation has a solution (Γ = tok(T({Γ})), so {Γ} ◁ T({Γ}) and 6.14

applies)

theorem Domain.Neighborhood.Exercise619.N_eq_solution : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ (NExpr.obj (singletonSys Γ h)).sys

N ≅ {{0},{0,Λ}} ⊕ N has a solution. There is Γ (the vertical naturals' token set) with Γ = tok(NExpr({Γ})), so {Γ} ◁ NExpr({Γ}) and Theorem 6.14 applies.

theorem Domain.Neighborhood.Exercise619.M_eq_solution : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ (MExpr.obj (singletonSys Γ h)).sys

M ≅ {{Λ}} + M has a solution (the lazy naturals).

theorem Domain.Neighborhood.Exercise619.NStar_eq_solution (N : ScottSys) (hN : [] ∈ N.sys.master) : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ ((NStarExpr N).obj (singletonSys Γ h)).sys

N* ≅ N ⊕ (N ⊗ N*) has a solution for any rooted datum domain N (the strict streams over N).

theorem Domain.Neighborhood.Exercise619.NStar_over_N_exists : ∃ (N : ScottSys), [] ∈ N.sys.master ∧ ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ ((NStarExpr N).obj (singletonSys Γ h)).sys

Chaining the equations. The solution N to the first equation is itself a rooted domain (Λ ∈ tok(N), since its token set is the fixed point Γ₁ ∋ Λ), so it is a legitimate datum domain for the third: N* exists over the very N produced by N ≅ {{0},{0,Λ}} ⊕ N.