Exercise 6.24 (Scott 1981, PRG-19, §6) — a double fixed point for a system

of domain equations

EXERCISE 6.24. Show that there must exist domains satisfying D ≅ D + (D × E) and E ≅ D + E, by using a double fixed-point method. First decide what the underlying set of tokens should be, and then define D and E by simultaneous fixed points. (Syntactical domains as in 6.23 may very well require several simultaneous equations.)

This is the simultaneous analogue of Exercise 6.20/6.21: there the conclusion was a single Γ with Γ = tok(T({Γ})), so that {Γ} ◁ T({Γ}) and Theorem 6.14 applies; here we produce a pair (Γ_D, Γ_E) of token sets that solve the two coupled token equations simultaneously, so that the two singleton systems sit as subsystems of the two right-hand sides at once — exactly the joint hypothesis the simultaneous form of Theorem 6.14 needs.

Deciding the tokens

Both D and E are taken to be ∅-free neighbourhood systems over the single token type Str = {0,1}* (Scott's uniform category of Exercise 6.19). The two right-hand sides are built from the uniform sum + (ScottSys.sum) and product × (ScottSys.prod), whose master (token set) is in both cases the tagged union {Λ} ∪ 0·(…) ∪ 1·(…). Writing tok(𝒟) = 𝒟.master and {Γ} for the one-neighbourhood system singletonSys Γ, the two token recursions are

• gTok p q = tok((D + E)) = {Λ} ∪ 0p ∪ 1q (for D = {p}, E = {q}),
• fTok p q = tok((D + (D×E))) = {Λ} ∪ 0p ∪ 1(gTok p q),

so fTok p q = gTok p (gTok p q) (the product D × E and the sum D + E have the same tagged master shape).

The double fixed point

The pair map Φ(p, q) = (fTok p q, gTok p q) is iterated from the bottom pair ({Λ}, {Λ}) (pIter); its two component unions

Γ_D = ⋃ₙ (Φⁿ).₁, Γ_E = ⋃ₙ (Φⁿ).₂

solve fTok Γ_D Γ_E = Γ_D and gTok Γ_D Γ_E = Γ_E (fTok_GammaD_GammaE, gTok_GammaD_GammaE). Both fTok/gTok are fully additive (built from insert, embBit, ∪), and — crucially — every token of fTok/gTok references at most one of the two coordinates, so each membership is witnessed at a single finite stage (no directedness merge is needed). This is the elementary token-level continuity that makes the Kleene union a fixed point.

The conclusion ({Γ_D} ◁ D + (D×E) and {Γ_E} ◁ D + E)

Setting D = {Γ_D}, E = {Γ_E}, the fixed-point equations say exactly that Γ_D (resp. Γ_E) is the master of D + (D×E) (resp. D + E), so the singleton systems are subsystems of the two right-hand sides — Dsol_subsystem, Esol_subsystem. These two facts together are the hypotheses of the simultaneous Theorem 6.14, which then yields the required isomorphisms D ≅ D + (D×E) and E ≅ D + E.

Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The two token recursions gTok and fTok

def Domain.Neighborhood.Exercise624.gTok (p q : Set ExampleB.Str) : Set ExampleB.Str

gTok p q = tok((D + E)) for D = {p}, E = {q}: the tagged union {Λ} ∪ 0p ∪ 1q. It is also the master of the product {p} × {q} (sum and product share the master shape over {0,1}*).

Equations

• Domain.Neighborhood.Exercise624.gTok p q = insert [] (Domain.Neighborhood.Example62.embBit false p ∪ Domain.Neighborhood.Example62.embBit true q)

def Domain.Neighborhood.Exercise624.fTok (p q : Set ExampleB.Str) : Set ExampleB.Str

fTok p q = tok((D + (D×E))) for D = {p}, E = {q}: {Λ} ∪ 0p ∪ 1(gTok p q), equivalently gTok p (gTok p q).

Equations

• Domain.Neighborhood.Exercise624.fTok p q = Domain.Neighborhood.Exercise624.gTok p (Domain.Neighborhood.Exercise624.gTok p q)

theorem Domain.Neighborhood.Exercise624.nil_mem_gTok (p q : Set ExampleB.Str) : [] ∈ gTok p q

theorem Domain.Neighborhood.Exercise624.nil_mem_fTok (p q : Set ExampleB.Str) : [] ∈ fTok p q

theorem Domain.Neighborhood.Exercise624.gTok_mono {p p' q q' : Set ExampleB.Str} (hp : p ⊆ p') (hq : q ⊆ q') : gTok p q ⊆ gTok p' q'

gTok is monotone in both arguments.

theorem Domain.Neighborhood.Exercise624.fTok_mono {p p' q q' : Set ExampleB.Str} (hp : p ⊆ p') (hq : q ⊆ q') : fTok p q ⊆ fTok p' q'

fTok is monotone in both arguments.

Token-level continuity over a chain: a membership reaches a single finite

stage

theorem Domain.Neighborhood.Exercise624.mem_gTok_iUnion {a b : ℕ → Set ExampleB.Str} {w : ExampleB.Str} (hw : w ∈ gTok (⋃ (n : ℕ), a n) (⋃ (n : ℕ), b n)) : ∃ (n : ℕ), w ∈ gTok (a n) (b n)

Additivity of gTok. Every token of gTok (⋃ₙ aₙ) (⋃ₙ bₙ) already lies in some gTok aₙ bₙ — each token references at most one coordinate.

theorem Domain.Neighborhood.Exercise624.mem_fTok_iUnion {a b : ℕ → Set ExampleB.Str} {w : ExampleB.Str} (hw : w ∈ fTok (⋃ (n : ℕ), a n) (⋃ (n : ℕ), b n)) : ∃ (n : ℕ), w ∈ fTok (a n) (b n)

Additivity of fTok. Every token of fTok (⋃ₙ aₙ) (⋃ₙ bₙ) already lies in some fTok aₙ bₙ. The nested true-branch (the product copy 0p inside 1(gTok p q)) still references at most one coordinate, so a single finite stage suffices.

The simultaneous Kleene iteration Φⁿ({Λ}, {Λ})

def Domain.Neighborhood.Exercise624.pIter : ℕ → Set ExampleB.Str × Set ExampleB.Str

The pair iteration Φ(p, q) = (fTok p q, gTok p q) from the bottom pair ({Λ}, {Λ}).

Equations

• One or more equations did not get rendered due to their size.
• Domain.Neighborhood.Exercise624.pIter 0 = ({[]}, {[]})

def Domain.Neighborhood.Exercise624.GammaD : Set ExampleB.Str

The first component of the double fixed point, Γ_D = ⋃ₙ (Φⁿ).₁.

Equations

• Domain.Neighborhood.Exercise624.GammaD = ⋃ (n : ℕ), (Domain.Neighborhood.Exercise624.pIter n).1

def Domain.Neighborhood.Exercise624.GammaE : Set ExampleB.Str

The second component of the double fixed point, Γ_E = ⋃ₙ (Φⁿ).₂.

Equations

• Domain.Neighborhood.Exercise624.GammaE = ⋃ (n : ℕ), (Domain.Neighborhood.Exercise624.pIter n).2

theorem Domain.Neighborhood.Exercise624.nil_mem_GammaD : [] ∈ GammaD

theorem Domain.Neighborhood.Exercise624.nil_mem_GammaE : [] ∈ GammaE

theorem Domain.Neighborhood.Exercise624.pIter_fst_subset_GammaD (m : ℕ) : (pIter m).1 ⊆ GammaD

Each stage sits inside the colimit Γ_D (choice-free; avoids Set.subset_iUnion).

theorem Domain.Neighborhood.Exercise624.pIter_snd_subset_GammaE (m : ℕ) : (pIter m).2 ⊆ GammaE

Each stage sits inside the colimit Γ_E (choice-free).

The double fixed point

theorem Domain.Neighborhood.Exercise624.fTok_GammaD_GammaE : fTok GammaD GammaE = GammaD

First equation of the double fixed point: fTok Γ_D Γ_E = Γ_D, i.e. tok(D + (D×E)) = Γ_D for D = {Γ_D}, E = {Γ_E}.

theorem Domain.Neighborhood.Exercise624.gTok_GammaD_GammaE : gTok GammaD GammaE = GammaE

Second equation of the double fixed point: gTok Γ_D Γ_E = Γ_E, i.e. tok(D + E) = Γ_E.

theorem Domain.Neighborhood.Exercise624.exists_double_fixedPoint : ∃ (Γd : Set ExampleB.Str) (Γe : Set ExampleB.Str), [] ∈ Γd ∧ [] ∈ Γe ∧ fTok Γd Γe = Γd ∧ gTok Γd Γe = Γe

The double fixed point (token level). There is a pair of token sets (Γ_D, Γ_E), both containing Λ, that solve the two coupled token equations tok(D + (D×E)) = Γ_D and tok(D + E) = Γ_E simultaneously.

The two solution systems and the simultaneous subsystem facts

def Domain.Neighborhood.Exercise624.Dsol : Exercise619.ScottSys

The solution system D = {Γ_D}.

Equations

• Domain.Neighborhood.Exercise624.Dsol = Domain.Neighborhood.Exercise619.singletonSys Domain.Neighborhood.Exercise624.GammaD Domain.Neighborhood.Exercise624.Dsol._proof_1

def Domain.Neighborhood.Exercise624.Esol : Exercise619.ScottSys

The solution system E = {Γ_E}.

Equations

• Domain.Neighborhood.Exercise624.Esol = Domain.Neighborhood.Exercise619.singletonSys Domain.Neighborhood.Exercise624.GammaE Domain.Neighborhood.Exercise624.Esol._proof_1

def Domain.Neighborhood.Exercise624.Fsol (D E : Exercise619.ScottSys) : Exercise619.ScottSys

The first right-hand side D + (D × E).

Equations

• Domain.Neighborhood.Exercise624.Fsol D E = D.sum (D.prod E)

def Domain.Neighborhood.Exercise624.Gsol (D E : Exercise619.ScottSys) : Exercise619.ScottSys

The second right-hand side D + E.

Equations

• Domain.Neighborhood.Exercise624.Gsol D E = D.sum E

theorem Domain.Neighborhood.Exercise624.master_Fsol : (Fsol Dsol Esol).sys.master = fTok GammaD GammaE

The master (token set) of D + (D×E) is fTok Γ_D Γ_E — definitionally, the sum/product masters expand to the tagged-union shape gTok/fTok.

theorem Domain.Neighborhood.Exercise624.master_Gsol : (Gsol Dsol Esol).sys.master = gTok GammaD GammaE

The master (token set) of D + E is gTok Γ_D Γ_E.

theorem Domain.Neighborhood.Exercise624.Dsol_subsystem : Dsol.sys ◁ (Fsol Dsol Esol).sys

{Γ_D} ◁ D + (D × E). The singleton system D = {Γ_D} is a subsystem of D + (D×E): by the fixed point its only neighbourhood Γ_D is the master of D + (D×E).

theorem Domain.Neighborhood.Exercise624.Esol_subsystem : Esol.sys ◁ (Gsol Dsol Esol).sys

{Γ_E} ◁ D + E. The singleton system E = {Γ_E} is a subsystem of D + E: by the fixed point its only neighbourhood Γ_E is the master of D + E.

theorem Domain.Neighborhood.Exercise624.exists_simultaneous_subsystems : ∃ (D : Exercise619.ScottSys) (E : Exercise619.ScottSys), D.sys ◁ (D.sum (D.prod E)).sys ∧ E.sys ◁ (D.sum E).sys

Exercise 6.24 (object level). By the double fixed-point method there exist ∅-free systems D, E over {0,1}* such that {D} ◁ D + (D×E) and {E} ◁ D + E simultaneously. These two facts are exactly the joint hypothesis of the simultaneous Theorem 6.14, which then yields the required isomorphisms D ≅ D + (D×E) and E ≅ D + E.