Exercise 6.19 (Scott 1981, PRG-19, §6) — Part B: the functor algebra

… Now generate all constructs T(X) formed by the constants (that is, T(X) = 𝒟 for a fixed 𝒟), by the identity (T(X) = X), and by sums and products (T₀(X) + T₁(X), etc.). Show that these are all functors, continuous on maps, and monotone and continuous on domains.

This module formalizes Part B: the closed family of constructs T(X) over Scott's uniform category of Exercise 6.19 — neighbourhood systems on Δ ⊆ {0,1}* with ∅ ∉ 𝒟 (the standing hypothesis that makes the token-level sum sumTok/product prodTok of Part A genuine endo-operations) and strict approximable maps.

Contents

• ScottSys — an object of Scott's category: an ∅-free neighbourhood system over Str = {0,1}*.
• The object actions ScottSys.sum/ScottSys.prod (Part A's sumTok/prodTok, repackaged so they stay inside the category) and the constant/identity objects.
• The functorial action on maps: sumMapTok f₀ f₁ : (𝒟₀+𝒟₁) → (ℰ₀+ℰ₁) and prodMapTok f₀ f₁ : (𝒟₀×𝒟₁) → (ℰ₀×ℰ₁), each an approximable map, with strictness preservation (sumMapTok is always strict; prodMapTok is strict when both factors are).
• The bifunctor laws: both actions preserve identities and composition (sumMapTok_id/sumMapTok_comp, prodMapTok_id/prodMapTok_comp).
• The functor-expression algebra FExpr (constants, identity, sum, product), its object action FExpr.obj, its action on maps FExpr.map.

Scott asks to show these constructs are all functors, continuous on maps, and monotone and continuous on domains; each is established here:

• functors — FExpr.map_id (T(I)=I) and FExpr.map_comp (T(g∘f)=T(g)∘T(f)), by induction; plus FExpr.map_isStrict (so T restricts to Scott's strict-map category).
• continuous on maps — FExpr.map_mono (a sharper map gives a sharper image) and FExpr.map_continuous (λf. T(f) preserves directed unions of maps); together these are exactly approximability of λf. T(f) (Exercise 2.13).
• monotone on domains — FExpr.obj_subsystem (D ◁ E ⟹ T(D) ◁ T(E)).
• continuous on domains — FExpr.obj_continuous (λD. T(D) preserves directed unions of subsystems, the form Scott uses in Theorem 6.14).

Because every construct stays over the single token type {0,1}*, the subdomain relation ◁ is between systems on a common carrier, so the domain conditions need no carrier transport (unlike the universe-polymorphic Endofunctor DomainObj form of Definitions 6.8/6.13).

This module also formalizes Exercise 6.20: writing tok(𝒟) = 𝒟.master for the underlying token set and {Γ} for the one-neighbourhood system singletonSys Γ, the function λΓ. tok(T({Γ})) is computed by the token-level recursion mFun T (mFun_eq_master), shown monotone (mFun_mono) and continuous (mFun_continuous) on the domain {Γ ∣ Λ ∈ Γ}. Its least fixed point — the explicit Kleene union ⋃ₙ mFunⁿ({Λ}) — gives a Γ = tok(T({Γ})) (exists_tok_fixedPoint), whence {Γ} ◁ T({Γ}) (exists_singleton_subsystem), exactly the hypothesis Theorem 6.14 needs.

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

Objects of Scott's category: ∅-free systems over {0,1}*

structure Domain.Neighborhood.Exercise619.ScottSys : Type

An object of the Exercise 6.19 category. An ∅-free neighbourhood system over Str = {0,1}* (ne: every neighbourhood is non-empty, Scott's ∅ ∉ 𝒟).

• sys : NeighborhoodSystem ExampleB.Str

  The underlying neighbourhood system on {0,1}*.

• ne (X : Set ExampleB.Str) : self.sys.mem X → X.Nonempty

  ∅ ∉ 𝒟: every neighbourhood is non-empty.

def Domain.Neighborhood.Exercise619.ScottSys.sum (A₀ A₁ : ScottSys) : ScottSys

The sum object 𝒟₀ + 𝒟₁ of Part A, repackaged as an object of the category.

Equations

• A₀.sum A₁ = { sys := Domain.Neighborhood.Exercise619.sumTok A₀.sys A₁.sys ⋯ ⋯, ne := ⋯ }

def Domain.Neighborhood.Exercise619.ScottSys.prod (A₀ A₁ : ScottSys) : ScottSys

The product object 𝒟₀ × 𝒟₁ of Part A, repackaged as an object of the category.

Equations

• A₀.prod A₁ = { sys := Domain.Neighborhood.Exercise619.prodTok A₀.sys A₁.sys, ne := ⋯ }

theorem Domain.Neighborhood.Exercise619.embBit_not_subset_cross {b b' : Bool} (h : b ≠ b') {X Y : Set ExampleB.Str} (hX : X.Nonempty) (hsub : Example62.embBit b X ⊆ Example62.embBit b' Y) : False

A non-empty b-tagged copy can never sit inside a b'-tagged copy for b ≠ b'.

The functorial action of sum on maps

def Domain.Neighborhood.Exercise619.sumMapTok {A₀ A₁ B₀ B₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) : ApproximableMap (A₀.sum A₁).sys (B₀.sum B₁).sys

f₀ + f₁, the action of the sum functor on (approximable) maps. It carries the master to the master (so it is strict), a left copy 0X to 0X' whenever X f₀ X', and a right copy 1Y to 1Y' whenever Y f₁ Y'.

Equations

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

theorem Domain.Neighborhood.Exercise619.sumMapTok_isStrict {A₀ A₁ B₀ B₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) : Exercise510.IsStrict (sumMapTok f₀ f₁)

sumMapTok is strict for any component maps: the master input Λ (the only neighbourhood containing the empty string) relates only to the output master.

The functorial action of product on maps

def Domain.Neighborhood.Exercise619.prodMapTok {A₀ A₁ B₀ B₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) : ApproximableMap (A₀.prod A₁).sys (B₀.prod B₁).sys

f₀ × f₁, the action of the product functor on (approximable) maps. A product neighbourhood {Λ} ∪ 0X ∪ 1Y is sent to {Λ} ∪ 0X' ∪ 1Y' whenever X f₀ X' and Y f₁ Y'.

Equations

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

theorem Domain.Neighborhood.Exercise619.prodMapTok_isStrict {A₀ A₁ B₀ B₁ : ScottSys} {f₀ : ApproximableMap A₀.sys B₀.sys} {f₁ : ApproximableMap A₁.sys B₁.sys} (hf₀ : Exercise510.IsStrict f₀) (hf₁ : Exercise510.IsStrict f₁) : Exercise510.IsStrict (prodMapTok f₀ f₁)

prodMapTok is strict exactly when both components are strict.

The bifunctor laws: identities and composition are preserved

theorem Domain.Neighborhood.Exercise619.sumMapTok_id {A₀ A₁ : ScottSys} : sumMapTok (ApproximableMap.idMap A₀.sys) (ApproximableMap.idMap A₁.sys) = ApproximableMap.idMap (A₀.sum A₁).sys

(I_{𝒟₀} + I_{𝒟₁}) = I_{𝒟₀+𝒟₁}.

theorem Domain.Neighborhood.Exercise619.sumMapTok_comp {A₀ A₁ B₀ B₁ C₀ C₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) (g₀ : ApproximableMap B₀.sys C₀.sys) (g₁ : ApproximableMap B₁.sys C₁.sys) : sumMapTok (g₀.comp f₀) (g₁.comp f₁) = (sumMapTok g₀ g₁).comp (sumMapTok f₀ f₁)

(g₀ ∘ f₀) + (g₁ ∘ f₁) = (g₀ + g₁) ∘ (f₀ + f₁).

theorem Domain.Neighborhood.Exercise619.prodMapTok_id {A₀ A₁ : ScottSys} : prodMapTok (ApproximableMap.idMap A₀.sys) (ApproximableMap.idMap A₁.sys) = ApproximableMap.idMap (A₀.prod A₁).sys

(I_{𝒟₀} × I_{𝒟₁}) = I_{𝒟₀×𝒟₁}.

theorem Domain.Neighborhood.Exercise619.prodMapTok_comp {A₀ A₁ B₀ B₁ C₀ C₁ : ScottSys} (f₀ : ApproximableMap A₀.sys B₀.sys) (f₁ : ApproximableMap A₁.sys B₁.sys) (g₀ : ApproximableMap B₀.sys C₀.sys) (g₁ : ApproximableMap B₁.sys C₁.sys) : prodMapTok (g₀.comp f₀) (g₁.comp f₁) = (prodMapTok g₀ g₁).comp (prodMapTok f₀ f₁)

(g₀ ∘ f₀) × (g₁ ∘ f₁) = (g₀ × g₁) ∘ (f₀ × f₁).

The functor-expression algebra T(X) and the functor laws

"Generate all constructs T(X) formed by the constants (T(X) = 𝒟), by the identity (T(X) = X), and by sums and products."

inductive Domain.Neighborhood.Exercise619.FExpr : Type

The functor-expression algebra. A T(X) built from constants, the identity, and binary sums and products — Scott's closed family of constructs.

• const : ScottSys → FExpr

  The constant functor T(X) = 𝒟 at a fixed object 𝒟.

• var : FExpr

  The identity functor T(X) = X.

• sum : FExpr → FExpr → FExpr

  The sum T₀(X) + T₁(X).

• prod : FExpr → FExpr → FExpr

  The product T₀(X) × T₁(X).

def Domain.Neighborhood.Exercise619.FExpr.obj : FExpr → ScottSys → ScottSys

The action of T on objects.

Equations

• (Domain.Neighborhood.Exercise619.FExpr.const D).obj x✝ = D
• Domain.Neighborhood.Exercise619.FExpr.var.obj x✝ = x✝
• (T₀.sum T₁).obj x✝ = (T₀.obj x✝).sum (T₁.obj x✝)
• (T₀.prod T₁).obj x✝ = (T₀.obj x✝).prod (T₁.obj x✝)

def Domain.Neighborhood.Exercise619.FExpr.map (T : FExpr) {X Y : ScottSys} : ApproximableMap X.sys Y.sys → ApproximableMap (T.obj X).sys (T.obj Y).sys

The action of T on (approximable) maps. Constants act by the identity, the identity functor acts by f itself, and sums/products act by the bifunctorial combinators sumMapTok/prodMapTok.

Equations

• (Domain.Neighborhood.Exercise619.FExpr.const D).map x✝ = Domain.Neighborhood.ApproximableMap.idMap D.sys
• Domain.Neighborhood.Exercise619.FExpr.var.map x✝ = x✝
• (T₀.sum T₁).map x✝ = Domain.Neighborhood.Exercise619.sumMapTok (T₀.map x✝) (T₁.map x✝)
• (T₀.prod T₁).map x✝ = Domain.Neighborhood.Exercise619.prodMapTok (T₀.map x✝) (T₁.map x✝)

theorem Domain.Neighborhood.Exercise619.FExpr.map_isStrict (T : FExpr) {X Y : ScottSys} (f : ApproximableMap X.sys Y.sys) : Exercise510.IsStrict f → Exercise510.IsStrict (T.map f)

Every T preserves strictness (so it restricts to Scott's category of strict maps): T(f) is strict whenever f is (and constants/sums are strict unconditionally).

theorem Domain.Neighborhood.Exercise619.FExpr.map_id (T : FExpr) (X : ScottSys) : T.map (ApproximableMap.idMap X.sys) = ApproximableMap.idMap (T.obj X).sys

Functor law 1 — T(I_X) = I_{T(X)}. Every construct T preserves identities.

theorem Domain.Neighborhood.Exercise619.FExpr.map_comp (T : FExpr) {X Y Z : ScottSys} (f : ApproximableMap X.sys Y.sys) (g : ApproximableMap Y.sys Z.sys) : T.map (g.comp f) = (T.map g).comp (T.map f)

Functor law 2 — T(g ∘ f) = T(g) ∘ T(f). Every construct T preserves composition; together with map_id this shows these are all functors.

Continuous on maps — the monotone half

Scott's continuous on maps (Definition 6.8) requires λf. T(f) to be approximable on the strict function space; here we record its monotonicity (the order half of approximability — a sharper map yields a sharper image), proved compositionally from the bifunctor combinators.

theorem Domain.Neighborhood.Exercise619.sumMapTok_mono {A₀ A₁ B₀ B₁ : ScottSys} {f₀ f₀' : ApproximableMap A₀.sys B₀.sys} {f₁ f₁' : ApproximableMap A₁.sys B₁.sys} (h0 : f₀ ≤ f₀') (h1 : f₁ ≤ f₁') : sumMapTok f₀ f₁ ≤ sumMapTok f₀' f₁'

sumMapTok is monotone in both arguments.

theorem Domain.Neighborhood.Exercise619.prodMapTok_mono {A₀ A₁ B₀ B₁ : ScottSys} {f₀ f₀' : ApproximableMap A₀.sys B₀.sys} {f₁ f₁' : ApproximableMap A₁.sys B₁.sys} (h0 : f₀ ≤ f₀') (h1 : f₁ ≤ f₁') : prodMapTok f₀ f₁ ≤ prodMapTok f₀' f₁'

prodMapTok is monotone in both arguments.

theorem Domain.Neighborhood.Exercise619.FExpr.map_mono (T : FExpr) {X Y : ScottSys} {f f' : ApproximableMap X.sys Y.sys} : f ≤ f' → T.map f ≤ T.map f'

λf. T(f) is monotone. A sharper map f ≤ f' is sent to a sharper image T(f) ≤ T(f') — the monotonicity half of continuous on maps.

Monotone on domains

Scott's monotone on domains (Definition 6.13): a subdomain relation D ◁ E is carried to T(D) ◁ T(E). Because every construct here stays over the single token type {0,1}*, the relation is between systems on a common carrier (no transport needed), and the bifunctor combinators carry ◁ componentwise.

theorem Domain.Neighborhood.Exercise619.sumTok_subsystem {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : (A₀.sum A₁).sys ◁ (B₀.sum B₁).sys

The sum carries the subsystem relation componentwise: 𝒟₀ ◁ ℰ₀ and 𝒟₁ ◁ ℰ₁ give 𝒟₀+𝒟₁ ◁ ℰ₀+ℰ₁.

theorem Domain.Neighborhood.Exercise619.prodTok_subsystem {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : (A₀.prod A₁).sys ◁ (B₀.prod B₁).sys

The product carries the subsystem relation componentwise.

theorem Domain.Neighborhood.Exercise619.FExpr.obj_subsystem (T : FExpr) {X Y : ScottSys} : X.sys ◁ Y.sys → (T.obj X).sys ◁ (T.obj Y).sys

λX. T(X) is monotone on domains. Whenever X ◁ Y we have T(X) ◁ T(Y).

Continuous on domains

Scott's continuous on domains (Definition 6.13): λD. T(D) preserves directed unions of subsystems. Concretely, if U is the union of a non-empty ◁-directed family ℱ of subsystems of U, then every neighbourhood of T(U) already appears in some T(D) with D ∈ ℱ (and conversely). The forward direction is by induction; the products use directedness to merge the two component witnesses into a single D.

theorem Domain.Neighborhood.Exercise619.FExpr.obj_continuous_mp (T : FExpr) {ℱ : Set ScottSys} {U : ScottSys} : DirectedOn (fun (a b : ScottSys) => a.sys ◁ b.sys) ℱ → ℱ.Nonempty → (∀ D ∈ ℱ, D.sys ◁ U.sys) → (∀ (X : Set ExampleB.Str), U.sys.mem X ↔ ∃ D ∈ ℱ, D.sys.mem X) → ∀ {W : Set ExampleB.Str}, (T.obj U).sys.mem W → ∃ D ∈ ℱ, (T.obj D).sys.mem W

Forward direction of continuity on domains: a neighbourhood of T(U) is a neighbourhood of some T(D) with D ∈ ℱ.

theorem Domain.Neighborhood.Exercise619.FExpr.obj_continuous (T : FExpr) {ℱ : Set ScottSys} {U : ScottSys} (hdir : DirectedOn (fun (a b : ScottSys) => a.sys ◁ b.sys) ℱ) (hne : ℱ.Nonempty) (hsub : ∀ D ∈ ℱ, D.sys ◁ U.sys) (hU : ∀ (X : Set ExampleB.Str), U.sys.mem X ↔ ∃ D ∈ ℱ, D.sys.mem X) (W : Set ExampleB.Str) : (T.obj U).sys.mem W ↔ ∃ D ∈ ℱ, (T.obj D).sys.mem W

λD. T(D) is continuous on domains. For a non-empty ◁-directed family ℱ of subsystems of U whose union is U, the neighbourhood family of T(U) is the union of those of the T(D).

Continuous on maps — full directed-sup preservation

Scott's continuous on maps (Definition 6.8): λf. T(f) is approximable, equivalently (Exercise 2.13) it is continuous — monotone (map_mono) and preserving directed unions of maps. If f is the pointwise union of a non-empty directed family gᵢ, then T(f) is the pointwise union of the T(gᵢ). The products use directedness to merge the two component witnesses.

theorem Domain.Neighborhood.Exercise619.FExpr.map_continuous_mp (T : FExpr) {I : Type} {X Y : ScottSys} {g : I → ApproximableMap X.sys Y.sys} {f : ApproximableMap X.sys Y.sys} [Nonempty I] : (∀ (i j : I), ∃ (k : I), g i ≤ g k ∧ g j ≤ g k) → (∀ (A B : Set ExampleB.Str), f.rel A B ↔ ∃ (i : I), (g i).rel A B) → ∀ {A B : Set ExampleB.Str}, (T.map f).rel A B → ∃ (i : I), (T.map (g i)).rel A B

Forward direction of continuity on maps: a related pair of T(f) is already related by some T(gᵢ).

theorem Domain.Neighborhood.Exercise619.FExpr.map_continuous (T : FExpr) {I : Type} [Nonempty I] {X Y : ScottSys} (g : I → ApproximableMap X.sys Y.sys) (f : ApproximableMap X.sys Y.sys) (hdir : ∀ (i j : I), ∃ (k : I), g i ≤ g k ∧ g j ≤ g k) (hf : ∀ (A B : Set ExampleB.Str), f.rel A B ↔ ∃ (i : I), (g i).rel A B) (A B : Set ExampleB.Str) : (T.map f).rel A B ↔ ∃ (i : I), (T.map (g i)).rel A B

λf. T(f) is continuous on maps. For a non-empty directed family gᵢ with pointwise union f, the relation of T(f) is the union of those of the T(gᵢ) — T(f) is approximable.

Exercise 6.20 — λΓ. tok(T({Γ})) is continuous, hence a fixed point exists

For any system 𝒟 let tok(𝒟) be the underlying set of tokens, so that 𝒟 is a system over tok(𝒟). For the category of Exercise 6.19 show that the function λΓ. tok(T({Γ})) is continuous on the domain {Γ ⊆ {0,1}* ∣ Λ ∈ Γ}, where T is any of the functors generated in 6.19. Conclude that there must exist a set Γ = tok(T({Γ})), so that {Γ} ◁ T({Γ}), and so 6.14 applies.

Here tok(𝒟) = 𝒟.master (the master neighbourhood is the token set Δ, since 𝒟 ⊆ 𝒫(Δ)), and {Γ} is the one-neighbourhood system singletonSys Γ with master Γ. The key simplification is that the master of T({Γ}) is computed by a tiny token-level recursion mFun T that needs no NeighborhoodSystem data at all: constants are constant, the identity returns Γ, and both sum and product return {Λ} ∪ 0·(…) ∪ 1·(…) (sumTokMaster = prodTokNbhd on masters). mFun_eq_master identifies mFun T Γ with tok(T({Γ})). The function mFun T is monotone (mFun_mono) and continuous — in fact fully additive — on the powerset of {0,1}* (mFun_continuous), so its restriction to {Γ ∣ Λ ∈ Γ} is continuous on that domain. The least fixed point above the bottom {Λ} is the explicit Kleene union ⋃ₙ mFunⁿ({Λ}) (mIter), giving Γ = tok(T({Γ})) (exists_tok_fixedPoint) and hence {Γ} ◁ T({Γ}) (exists_singleton_subsystem), exactly the hypothesis Theorem 6.14 needs. (For the bottom to stay in the domain we need Λ ∈ tok(C) for the constant systems C; this is recorded by FExpr.RootedConst, and holds automatically for sums and products since their masters contain Λ.)

def Domain.Neighborhood.Exercise619.ScottSys.tok (D : ScottSys) : Set ExampleB.Str

tok(𝒟) — the underlying set of tokens of a system, i.e. its master neighbourhood Δ.

Equations

• D.tok = D.sys.master

def Domain.Neighborhood.Exercise619.singletonSys (Γ : Set ExampleB.Str) (h : Γ.Nonempty) : ScottSys

The one-neighbourhood system {Γ} over {0,1}*: its only neighbourhood is Γ itself, and its master (token set) is Γ. It is ∅-free precisely because Γ is non-empty.

Equations

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

def Domain.Neighborhood.Exercise619.mFun : FExpr → Set ExampleB.Str → Set ExampleB.Str

The token-level master recursion. mFun T Γ computes tok(T({Γ})) purely from Γ, without touching the neighbourhood data of {Γ} (mFun_eq_master): constants are constant, the identity returns Γ, and both sum and product wrap the two component token sets with the tags 0,1 under a common root Λ (sumTokMaster = prodTokNbhd agree on masters).

Equations

• One or more equations did not get rendered due to their size.
• Domain.Neighborhood.Exercise619.mFun (Domain.Neighborhood.Exercise619.FExpr.const C) x✝ = C.sys.master
• Domain.Neighborhood.Exercise619.mFun Domain.Neighborhood.Exercise619.FExpr.var x✝ = x✝

theorem Domain.Neighborhood.Exercise619.mFun_eq_master (T : FExpr) {Γ : Set ExampleB.Str} (h : Γ.Nonempty) : mFun T Γ = (T.obj (singletonSys Γ h)).sys.master

mFun T Γ is exactly the token set tok(T({Γ})) = (T.obj {Γ}).sys.master.

Monotone on the domain

theorem Domain.Neighborhood.Exercise619.insertTag_mono {p q p' q' : Set ExampleB.Str} (hp : p ⊆ p') (hq : q ⊆ q') : insert [] (Example62.embBit false p ∪ Example62.embBit true q) ⊆ insert [] (Example62.embBit false p' ∪ Example62.embBit true q')

Monotonicity of the tagged-union shape shared by sum and product.

theorem Domain.Neighborhood.Exercise619.mFun_mono (T : FExpr) {Γ Γ' : Set ExampleB.Str} (h : Γ ⊆ Γ') : mFun T Γ ⊆ mFun T Γ'

λΓ. tok(T({Γ})) is monotone on the domain.

Continuous on the domain

theorem Domain.Neighborhood.Exercise619.insertTag_continuous {ℱ : Set (Set ExampleB.Str)} {U : Set ExampleB.Str} (hne : ℱ.Nonempty) {p q : Set ExampleB.Str → Set ExampleB.Str} (hp : ∀ (w : ExampleB.Str), w ∈ p U ↔ ∃ Γ ∈ ℱ, w ∈ p Γ) (hq : ∀ (w : ExampleB.Str), w ∈ q U ↔ ∃ Γ ∈ ℱ, w ∈ q Γ) (w : ExampleB.Str) : w ∈ insert [] (Example62.embBit false (p U) ∪ Example62.embBit true (q U)) ↔ ∃ Γ ∈ ℱ, w ∈ insert [] (Example62.embBit false (p Γ) ∪ Example62.embBit true (q Γ))

Continuity (full additivity) of the tagged-union shape shared by sum and product.

theorem Domain.Neighborhood.Exercise619.mFun_continuous (T : FExpr) {ℱ : Set (Set ExampleB.Str)} {U : Set ExampleB.Str} (_hdir : DirectedOn (fun (x1 x2 : Set ExampleB.Str) => x1 ⊆ x2) ℱ) (hne : ℱ.Nonempty) (hU : ∀ (w : ExampleB.Str), w ∈ U ↔ ∃ Γ ∈ ℱ, w ∈ Γ) (w : ExampleB.Str) : w ∈ mFun T U ↔ ∃ Γ ∈ ℱ, w ∈ mFun T Γ

λΓ. tok(T({Γ})) is continuous on the domain {Γ ∣ Λ ∈ Γ}. For a non-empty ⊆-directed family ℱ with union U, the token set of T({U}) is the union of those of the T({Γ}). (The proof in fact establishes full additivity — directedness is not needed for the master level — but the statement is the directed-sup form Scott calls continuous.)

A fixed point Γ = tok(T({Γ})) — so {Γ} ◁ T({Γ}) and 6.14 applies

def Domain.Neighborhood.Exercise619.FExpr.RootedConst : FExpr → Prop

Λ ∈ tok(C) for every constant C occurring in T. This is what keeps the bottom {Λ} and the whole Kleene chain inside the domain {Γ ∣ Λ ∈ Γ}; sums and products satisfy it for free.

Equations

• (Domain.Neighborhood.Exercise619.FExpr.const C).RootedConst = ([] ∈ C.sys.master)
• Domain.Neighborhood.Exercise619.FExpr.var.RootedConst = True
• (a.sum b).RootedConst = (a.RootedConst ∧ b.RootedConst)
• (a.prod b).RootedConst = (a.RootedConst ∧ b.RootedConst)

theorem Domain.Neighborhood.Exercise619.mFun_nil_mem (T : FExpr) : T.RootedConst → ∀ {Γ : Set ExampleB.Str}, [] ∈ Γ → [] ∈ mFun T Γ

If Λ ∈ Γ then Λ ∈ tok(T({Γ})) — so λΓ. tok(T({Γ})) is an endofunction of the domain.

def Domain.Neighborhood.Exercise619.mIter (T : FExpr) : ℕ → Set ExampleB.Str

The Kleene iteration mFunⁿ({Λ}) whose union is the least fixed point above {Λ}.

Equations

• Domain.Neighborhood.Exercise619.mIter T 0 = {[]}
• Domain.Neighborhood.Exercise619.mIter T n.succ = Domain.Neighborhood.Exercise619.mFun T (Domain.Neighborhood.Exercise619.mIter T n)

theorem Domain.Neighborhood.Exercise619.nil_mem_mIter (T : FExpr) (hT : T.RootedConst) (n : ℕ) : [] ∈ mIter T n

theorem Domain.Neighborhood.Exercise619.mIter_mono_step (T : FExpr) (hT : T.RootedConst) (n : ℕ) : mIter T n ⊆ mIter T (n + 1)

theorem Domain.Neighborhood.Exercise619.mIter_mono (T : FExpr) (hT : T.RootedConst) {m n : ℕ} (hmn : m ≤ n) : mIter T m ⊆ mIter T n

theorem Domain.Neighborhood.Exercise619.mFun_iter_fixed (T : FExpr) (hT : T.RootedConst) : mFun T (⋃ (n : ℕ), mIter T n) = ⋃ (n : ℕ), mIter T n

The Kleene union is a fixed point of λΓ. tok(T({Γ})).

theorem Domain.Neighborhood.Exercise619.exists_tok_fixedPoint (T : FExpr) (hT : T.RootedConst) : ∃ (Γ : Set ExampleB.Str), [] ∈ Γ ∧ mFun T Γ = Γ

The conclusion of Exercise 6.20 (token level). For any construct T whose constants contain Λ, there is a set Γ with Λ ∈ Γ and Γ = tok(T({Γ})).

theorem Domain.Neighborhood.Exercise619.exists_singleton_subsystem (T : FExpr) (hT : T.RootedConst) : ∃ (Γ : Set ExampleB.Str) (h : Γ.Nonempty), (singletonSys Γ h).sys ◁ (T.obj (singletonSys Γ h)).sys

The conclusion of Exercise 6.20 (object level): {Γ} ◁ T({Γ}), so Theorem 6.14 applies. From the fixed point Γ = tok(T({Γ})), the one-neighbourhood system {Γ} is a subsystem of T({Γ}): they share the master Γ, and Γ is a (the master) neighbourhood of T({Γ}).