Exercise 6.23 (Scott 1981, PRG-19, §6) — the syntactic domain of expressions

EXERCISE 6.23. Construe the initial solution to Exp ≅ N ⊕ ((Exp × Exp) + (Exp × Exp)) as a "syntactical domain" of expressions generated from infinitely many "variables" by means of two binary "operation symbols". Given an algebra D with two operations u : D×D → D and v : D×D → D, show how any strict map s : N → D determines a unique map val(s) : Exp → D that can be regarded as the "evaluation of an expression".

The right-hand functor is T(X) = N ⊕ ((X×X) + (X×X)), i.e. in the algebra GExpr of Exercise 6.21, Texp N = .oplus (.const N) (.sum (.prod .var .var) (.prod .var .var)). Reading the structure map k : T(Exp) → Exp of an algebra through the universal properties of ⊕, +, ×:

• the ⊕ N summand gives a strict variable map s : N → Exp (the "infinitely many variables" are the tokens / points of N);
• the two (Exp × Exp) summands, combined by +, give two binary operation symbols u, v : Exp × Exp → Exp.

So an algebra of this functor is exactly a domain D with a strict s : N → D and two binary operations u, v : D×D → D, and the unique homomorphism val(s) : Exp → D is Scott's "evaluation of an expression": it sends a variable to its value under s, and an u/v-node to the u/v of the values of its two subexpressions.

This module (Phase 1 — the domain Exp itself)

Following Scott's standing restriction in Exercises 6.19–6.23 to ∅-free systems over {0,1}* and strict maps (ScottSys), and following the structure of Theorem 6.14 (the initial solution is the iterated colimit 𝒟 = ⋃ₙ Tⁿ({Γ})), we build the concrete solution domain for any rooted GExpr functor T:

• gFix T = ⋃ₙ gFunⁿ({Λ}) — the token set (Exercise 6.20/6.21 fixed point Γ = tok(T({Γ})));
• gTower T n = Tⁿ({Γ}) — the iterated-functor tower of ∅-free systems over Str;
• gColim T = ⋃ₙ Tⁿ({Γ}) — the colimit system, with gColim_obj_eq : T(gColim) = gColim (the structure map is the identity, since the two systems are literally equal — no carrier transport is needed because ScottSys keeps the token type fixed at Str).

Instantiating at Texp N gives Exp N := gColim (Texp N) together with the domain-equation isomorphism Exp ≅ N ⊕ ((Exp×Exp)+(Exp×Exp)) (Exp_structure_eq). The algebra decomposition (s, u, v) and the unique evaluation homomorphism val(s) (initiality) are developed in later phases.

Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}); the colimit is genuine data built without Classical.choice (the generator Γ is the explicit Kleene union, not an existential witness).

The generator Γ = ⋃ₙ gFunⁿ({Λ}) (the Exercise 6.20/6.21 fixed point, as

data)

def Domain.Neighborhood.Exercise619.gFix (T : GExpr) : Set ExampleB.Str

The fixed-point token set Γ = tok(T({Γ})), as the explicit Kleene union ⋃ₙ gIter T n (no Classical.choice).

Equations

• Domain.Neighborhood.Exercise619.gFix T = ⋃ (n : ℕ), Domain.Neighborhood.Exercise619.gIter T n

theorem Domain.Neighborhood.Exercise619.gFix_nil_mem (T : GExpr) : [] ∈ gFix T

theorem Domain.Neighborhood.Exercise619.gFix_nonempty (T : GExpr) : (gFix T).Nonempty

theorem Domain.Neighborhood.Exercise619.gFix_fixed (T : GExpr) (hT : T.RootedConst) : gFun T (gFix T) = gFix T

Γ = tok(T({Γ})) at the token level: gFun T Γ = Γ.

The iterated-functor tower Tⁿ({Γ})

def Domain.Neighborhood.Exercise619.gGen (T : GExpr) : ScottSys

The one-point generator {Γ} as an object of the category.

Equations

• Domain.Neighborhood.Exercise619.gGen T = Domain.Neighborhood.Exercise619.singletonSys (Domain.Neighborhood.Exercise619.gFix T) ⋯

@[simp]

theorem Domain.Neighborhood.Exercise619.gGen_master (T : GExpr) : (gGen T).sys.master = gFix T

theorem Domain.Neighborhood.Exercise619.gBase (T : GExpr) (hT : T.RootedConst) : (gGen T).sys ◁ (T.obj (gGen T)).sys

{Γ} ◁ T({Γ}) — Scott's hypothesis for Theorem 6.14, the base of the tower. (This is the content of gExists_singleton_subsystem, here at the explicit generator Γ = gFix T.)

def Domain.Neighborhood.Exercise619.gTower (T : GExpr) : ℕ → ScottSys

The tower Tⁿ({Γ}) of ∅-free systems over Str: T⁰({Γ}) = {Γ}, Tⁿ⁺¹({Γ}) = T(Tⁿ({Γ})).

Equations

• Domain.Neighborhood.Exercise619.gTower T 0 = Domain.Neighborhood.Exercise619.gGen T
• Domain.Neighborhood.Exercise619.gTower T n.succ = T.obj (Domain.Neighborhood.Exercise619.gTower T n)

@[simp]

theorem Domain.Neighborhood.Exercise619.gTower_zero (T : GExpr) : gTower T 0 = gGen T

@[simp]

theorem Domain.Neighborhood.Exercise619.gTower_succ (T : GExpr) (n : ℕ) : gTower T (n + 1) = T.obj (gTower T n)

theorem Domain.Neighborhood.Exercise619.gChain (T : GExpr) (hT : T.RootedConst) (n : ℕ) : (gTower T n).sys ◁ (gTower T (n + 1)).sys

The basic chain step Tⁿ({Γ}) ◁ Tⁿ⁺¹({Γ}). Base: gBase. Step: T is monotone on domains (obj_subsystem).

theorem Domain.Neighborhood.Exercise619.gTower_master (T : GExpr) (hT : T.RootedConst) (n : ℕ) : (gTower T n).sys.master = gFix T

Every level of the tower has the same master Δ = Γ.

theorem Domain.Neighborhood.Exercise619.gTower_le (T : GExpr) (hT : T.RootedConst) {n m : ℕ} (h : n ≤ m) : (gTower T n).sys ◁ (gTower T m).sys

The tower is a ◁-chain: Tⁿ({Γ}) ◁ Tᵐ({Γ}) whenever n ≤ m.

The colimit 𝒟 = ⋃ₙ Tⁿ({Γ})

def Domain.Neighborhood.Exercise619.gColim (T : GExpr) (hT : T.RootedConst) : ScottSys

The colimit system 𝒟 = ⋃ₙ Tⁿ({Γ}) as an ∅-free system over Str. A set is a neighbourhood exactly when it is a neighbourhood of some level; closure under consistent intersection uses that the tower is a chain (any finite collection sits inside one level).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_gColim (T : GExpr) (hT : T.RootedConst) {X : Set ExampleB.Str} : (gColim T hT).sys.mem X ↔ ∃ (n : ℕ), (gTower T n).sys.mem X

@[simp]

theorem Domain.Neighborhood.Exercise619.gColim_master (T : GExpr) (hT : T.RootedConst) : (gColim T hT).sys.master = gFix T

theorem Domain.Neighborhood.Exercise619.gTower_sub_colim (T : GExpr) (hT : T.RootedConst) (n : ℕ) : (gTower T n).sys ◁ (gColim T hT).sys

Each level of the tower is a subdomain of the colimit: Tⁿ({Γ}) ◁ 𝒟.

The structure isomorphism T(𝒟) = 𝒟

theorem Domain.Neighborhood.Exercise619.ScottSys.ext {A B : ScottSys} (h : A.sys = B.sys) : A = B

Two objects of the category with the same underlying system are equal (the ∅-freeness field is a Prop).

theorem Domain.Neighborhood.Exercise619.gColim_obj_sys_eq (T : GExpr) (hT : T.RootedConst) : (T.obj (gColim T hT)).sys = (gColim T hT).sys

T(𝒟) = 𝒟 at the level of neighbourhood systems. Membership: continuity on domains (obj_continuous) along the directed tower turns T(⋃ₙ Tⁿ({Γ})) into ⋃ₙ Tⁿ⁺¹({Γ}), which has the same neighbourhoods as ⋃ₙ Tⁿ({Γ}) (the extra n=0 level T⁰({Γ}) is absorbed by the chain step). Master: both are Γ (gTower_master through obj_subsystem of Tⁿ({Γ}) ◁ 𝒟).

theorem Domain.Neighborhood.Exercise619.gColim_obj_eq (T : GExpr) (hT : T.RootedConst) : T.obj (gColim T hT) = gColim T hT

The structure isomorphism T(𝒟) ≅ 𝒟 is the identity (the two objects are literally equal).

The functor of Exercise 6.23 and the syntactic domain Exp

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

The functor T(X) = N ⊕ ((X×X) + (X×X)) of Exercise 6.23, as a GExpr over the variable domain N. The ⊕ N carries the variables, and the two (X×X) summands (combined by +) carry the two binary operation symbols.

Equations

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

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

Texp N is rooted iff the variable domain N is (Λ ∈ tok(N), automatic for the fixed-point solutions of 6.19–6.22).

def Domain.Neighborhood.Exercise619.Exp (N : ScottSys) (hN : [] ∈ N.sys.master) : ScottSys

The syntactic domain of expressions Exp = ⋃ₙ Texpⁿ({Γ}), the initial solution of Exp ≅ N ⊕ ((Exp×Exp)+(Exp×Exp)).

Equations

• Domain.Neighborhood.Exercise619.Exp N hN = Domain.Neighborhood.Exercise619.gColim (Domain.Neighborhood.Exercise619.Texp N) ⋯

theorem Domain.Neighborhood.Exercise619.Exp_structure_eq (N : ScottSys) (hN : [] ∈ N.sys.master) : (Texp N).obj (Exp N hN) = Exp N hN

The domain equation Exp ≅ N ⊕ ((Exp×Exp)+(Exp×Exp)), realised as an equality of systems (the structure map is the identity). This is the "construe the initial solution" half of Exercise 6.23.

Phase 2 — the strict-map category, the endofunctor T, and the algebra

Exp

Following Scott (and Exercise 6.17's StrictDomainObj), but over the fixed token type Str: the objects are ScottSys (∅-free systems over Str), the morphisms are strict approximable maps. Because every object lives over Str, all carrier equalities are rfl and there is no HEq transport (the obstruction that made the abstract Theorem 6.14 unusable). The functor Texp N then becomes a genuine Endofunctor of this category, and the colimit Exp of Phase 1 — together with the structure equality T(Exp) = Exp — is a T-algebra.

@[implicit_reducible]

instance Domain.Neighborhood.Exercise619.instCategoryScottSys : Category ScottSys

The category of ∅-free domains over Str and strict maps. Morphisms are strict approximable maps (StrictMap); identities and associative composition are Theorem 2.5, with strictness preserved by isStrict_idMap/isStrict_comp. The fixed carrier Str is what removes all the carrier-transport HEq that burdens the abstract Endofunctor DomainObj.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.ScottSys.id_val (A : ScottSys) : ↑(Category.id A) = ApproximableMap.idMap A.sys

@[simp]

theorem Domain.Neighborhood.Exercise619.ScottSys.comp_val {A B C : ScottSys} (g : Category.Hom B C) (f : Category.Hom A B) : ↑(g ⊚ f) = (↑g).comp ↑f

def Domain.Neighborhood.Exercise619.gFunctorMap (T : GExpr) {X Y : ScottSys} (f : Exercise510.StrictMap X.sys Y.sys) : Exercise510.StrictMap (T.obj X).sys (T.obj Y).sys

The morphism action of gFunctor T: a strict f is sent to the strict map T(f). (Typed via StrictMap, which is defeq to the category's Hom; this avoids the class-projection that blocks the anonymous .1 on Category.Hom.)

Equations

• Domain.Neighborhood.Exercise619.gFunctorMap T f = ⟨T.map ↑f, ⋯⟩

def Domain.Neighborhood.Exercise619.gFunctor (T : GExpr) : Endofunctor ScottSys

Every GExpr is an Endofunctor of the strict-map category. On objects it is GExpr.obj; on a strict map f it is the strict map T(f) (GExpr.map_isStrict). Functoriality is GExpr.map_id and GExpr.map_comp (the latter needs g strict — automatic here, since every morphism of this category is strict).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.gFunctor_obj (T : GExpr) (X : ScottSys) : (gFunctor T).obj X = T.obj X

@[simp]

theorem Domain.Neighborhood.Exercise619.gFunctorMap_val (T : GExpr) {X Y : ScottSys} (f : Exercise510.StrictMap X.sys Y.sys) : ↑(gFunctorMap T f) = T.map ↑f

def Domain.Neighborhood.Exercise619.TexpF (N : ScottSys) : Endofunctor ScottSys

The endofunctor T(X) = N ⊕ ((X×X) + (X×X)) of Exercise 6.23.

Equations

• Domain.Neighborhood.Exercise619.TexpF N = Domain.Neighborhood.Exercise619.gFunctor (Domain.Neighborhood.Exercise619.Texp N)

def Domain.Neighborhood.Exercise619.isoOfObjEq {Obj : Type u_1} [Category Obj] {X Y : Obj} (h : X = Y) : Iso X Y

The identity isomorphism in any category induced by an object equality.

Equations

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

def Domain.Neighborhood.Exercise619.ExpIso (N : ScottSys) (hN : [] ∈ N.sys.master) : Iso ((TexpF N).obj (Exp N hN)) (Exp N hN)

The structure isomorphism T(Exp) ≅ Exp. Since Phase 1 proved T(Exp) = Exp as objects (Exp_structure_eq), this is the identity isomorphism.

Equations

• Domain.Neighborhood.Exercise619.ExpIso N hN = Domain.Neighborhood.Exercise619.isoOfObjEq ⋯

def Domain.Neighborhood.Exercise619.ExpAlg (N : ScottSys) (hN : [] ∈ N.sys.master) : TAlgebra (TexpF N)

Exp as a T-algebra with structure map the isomorphism T(Exp) ≅ Exp (the identity, since T(Exp) = Exp). This realises Scott's "construe the initial solution as a syntactic domain of expressions": Exp is an algebra of T(X) = N ⊕ ((X×X)+(X×X)).

Equations

• Domain.Neighborhood.Exercise619.ExpAlg N hN = { carrier := Domain.Neighborhood.Exercise619.Exp N hN, str := (Domain.Neighborhood.Exercise619.ExpIso N hN).hom }

Phase 3 — the evaluation homomorphism val(s) (existence)

Given any algebra B = (D, k) of T(X) = N ⊕ ((X×X)+(X×X)) — i.e. a domain D carrying (through the universal properties of ⊕,+,×) a strict variable map s : N → D and two binary operations u, v : D×D → D — we build a T-algebra homomorphism val : Exp → D. This is Scott's "evaluation of an expression".

Since Phase 1's structure map i : T(Exp) → Exp is the identity (Exp_structure_eq), the homomorphism equation val ∘ i = k ∘ T(val) is the fixed-point equation val = k ∘ T(val) ∘ j (j = i⁻¹). We solve it directly by the Kleene iteration valₙ (val₀ = ⊥, valₙ₊₁ = k ∘ T(valₙ) ∘ j) and take val = ⋃ₙ valₙ. The fixed-point property uses continuity on maps (GExpr.map_continuous: T(⋃ valₙ) = ⋃ T(valₙ)); no projection machinery is needed for existence. (Uniqueness — initiality — is the remaining Phase 4.)

def Domain.Neighborhood.Exercise619.algStr {N : ScottSys} (B : TAlgebra (TexpF N)) : ApproximableMap ((Texp N).obj B.carrier).sys B.carrier.sys

The structure map of an algebra B, as a raw approximable map (its strictness is algStr_strict). The ascription to StrictMap forces the categorical Hom to its underlying subtype.

Equations

• Domain.Neighborhood.Exercise619.algStr B = ↑B.str

theorem Domain.Neighborhood.Exercise619.algStr_strict {N : ScottSys} (B : TAlgebra (TexpF N)) : Exercise510.IsStrict (algStr B)

def Domain.Neighborhood.Exercise619.expInv (N : ScottSys) (hN : [] ∈ N.sys.master) : ApproximableMap (Exp N hN).sys ((Texp N).obj (Exp N hN)).sys

The inverse j = i⁻¹ : Exp → T(Exp) of the structure isomorphism, as a raw map.

Equations

• Domain.Neighborhood.Exercise619.expInv N hN = ↑(Domain.Neighborhood.Exercise619.ExpIso N hN).inv

theorem Domain.Neighborhood.Exercise619.expInv_strict (N : ScottSys) (hN : [] ∈ N.sys.master) : Exercise510.IsStrict (expInv N hN)

def Domain.Neighborhood.Exercise619.expHom (N : ScottSys) (hN : [] ∈ N.sys.master) : ApproximableMap ((Texp N).obj (Exp N hN)).sys (Exp N hN).sys

The structure map i : T(Exp) → Exp as a raw map (the identity, since T(Exp) = Exp).

Equations

• Domain.Neighborhood.Exercise619.expHom N hN = ↑(Domain.Neighborhood.Exercise619.ExpIso N hN).hom

theorem Domain.Neighborhood.Exercise619.expInv_comp_expHom (N : ScottSys) (hN : [] ∈ N.sys.master) : (expInv N hN).comp (expHom N hN) = ApproximableMap.idMap ((Texp N).obj (Exp N hN)).sys

j ∘ i = I_{T(Exp)} at the raw level (from the iso's hom_inv_id).

theorem Domain.Neighborhood.Exercise619.expHom_comp_expInv (N : ScottSys) (hN : [] ∈ N.sys.master) : (expHom N hN).comp (expInv N hN) = ApproximableMap.idMap (Exp N hN).sys

i ∘ j = I_Exp at the raw level (from the iso's inv_hom_id).

def Domain.Neighborhood.Exercise619.descRel {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) : ℕ → ApproximableMap (Exp N hN).sys B.carrier.sys

The Kleene iterates valₙ : Exp → D of the operator λh. k ∘ T(h) ∘ j. val₀ = ⊥, valₙ₊₁ = k ∘ T(valₙ) ∘ j.

Equations

• One or more equations did not get rendered due to their size.
• Domain.Neighborhood.Exercise619.descRel hN B 0 = Domain.Neighborhood.constMap (Domain.Neighborhood.Exercise619.Exp N hN).sys B.carrier.sys.bot

@[simp]

theorem Domain.Neighborhood.Exercise619.descRel_succ {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (n : ℕ) : descRel hN B (n + 1) = (algStr B).comp (((Texp N).map (descRel hN B n)).comp (expInv N hN))

theorem Domain.Neighborhood.Exercise619.descRel_isStrict {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (n : ℕ) : Exercise510.IsStrict (descRel hN B n)

Every iterate is strict.

theorem Domain.Neighborhood.Exercise619.constBot_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ApproximableMap V₀ V₁) : constMap V₀ V₁.bot ≤ g

The constant ⊥ map is below every approximable map (it relates each domain neighbourhood only to the codomain master, which every map produces by monotonicity from master_rel).

theorem Domain.Neighborhood.Exercise619.descRel_le_succ {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (n : ℕ) : descRel hN B n ≤ descRel hN B (n + 1)

The iterates increase: valₙ ≤ valₙ₊₁.

theorem Domain.Neighborhood.Exercise619.descRel_mono {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) {i j : ℕ} (h : i ≤ j) : descRel hN B i ≤ descRel hN B j

The iterates form a ≤-chain.

theorem Domain.Neighborhood.Exercise619.descDir {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (i j : ℕ) : ∃ (k : ℕ), (∀ (X Y : Set ExampleB.Str), (descRel hN B i).rel X Y → (descRel hN B k).rel X Y) ∧ ∀ (X Y : Set ExampleB.Str), (descRel hN B j).rel X Y → (descRel hN B k).rel X Y

Directedness witness for the union (any two iterates are dominated by the later one).

def Domain.Neighborhood.Exercise619.descMap {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) : ApproximableMap (Exp N hN).sys B.carrier.sys

The evaluation map val = ⋃ₙ valₙ as an approximable map.

Equations

• Domain.Neighborhood.Exercise619.descMap hN B = Domain.Neighborhood.ApproximableMap.iSupMap (Domain.Neighborhood.Exercise619.descRel hN B) ⋯

theorem Domain.Neighborhood.Exercise619.descMap_rel {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) {A E : Set ExampleB.Str} : (descMap hN B).rel A E ↔ ∃ (n : ℕ), (descRel hN B n).rel A E

theorem Domain.Neighborhood.Exercise619.descMap_isStrict {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) : Exercise510.IsStrict (descMap hN B)

val is strict (a union of strict maps).

theorem Domain.Neighborhood.Exercise619.descDirLe {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (i j : ℕ) : ∃ (k : ℕ), descRel hN B i ≤ descRel hN B k ∧ descRel hN B j ≤ descRel hN B k

Directedness of the iterates in ≤-form (for map_continuous).

theorem Domain.Neighborhood.Exercise619.descMap_is_sup {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (A E : Set ExampleB.Str) : (descMap hN B).rel A E ↔ ∃ (n : ℕ), (descRel hN B n).rel A E

val is the relational union of the iterates (the hypothesis for map_continuous).

theorem Domain.Neighborhood.Exercise619.descMap_fix {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) : descMap hN B = (algStr B).comp (((Texp N).map (descMap hN B)).comp (expInv N hN))

The fixed-point equation val = k ∘ T(val) ∘ j. Forward: an iterate valₙ is, after the recursion, k ∘ T(valₙ₋₁) ∘ j, and T(valₙ₋₁) ⊆ T(val) by continuity on maps. Backward: a witness factoring through T(valₙ) lands in valₙ₊₁.

theorem Domain.Neighborhood.Exercise619.descComm {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) : (descMap hN B).comp (expHom N hN) = (algStr B).comp ((Texp N).map (descMap hN B))

The homomorphism square val ∘ i = k ∘ T(val) at the raw level (conjugating the fixed-point equation by i, using j ∘ i = I).

def Domain.Neighborhood.Exercise619.descAlgHom {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) : AlgHom (ExpAlg N hN) B

The evaluation homomorphism val(s) : Exp → D as a T-algebra homomorphism — Scott's existence of the evaluation map.

Equations

• Domain.Neighborhood.Exercise619.descAlgHom hN B = { hom := ⟨Domain.Neighborhood.Exercise619.descMap hN B, ⋯⟩, comm := ⋯ }

theorem Domain.Neighborhood.Exercise619.algHom_fix {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (g : AlgHom (ExpAlg N hN) B) : ↑g.hom = (algStr B).comp (((Texp N).map ↑g.hom).comp (expInv N hN))

Every homomorphism g : Exp → D is a fixed point of the operator λh. k ∘ T(h) ∘ j. This is the homomorphism square g ∘ i = k ∘ T(g) (g.comm) rearranged by i ∘ j = I.

theorem Domain.Neighborhood.Exercise619.descRel_le_algHom {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (g : AlgHom (ExpAlg N hN) B) (n : ℕ) : descRel hN B n ≤ ↑g.hom

descAlgHom is the least homomorphism: val ≤ g for every homomorphism g : Exp → D. The Kleene iterates valₙ lie below any fixed point g (induction: val₀ = ⊥ ≤ g, and the operator is monotone with g its own fixed point), so their union val does too. This is the easy half of initiality; the matching g ≤ val (so g = val) is the projection-chain argument of Phase 4.

theorem Domain.Neighborhood.Exercise619.descMap_le_algHom {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (g : AlgHom (ExpAlg N hN) B) : descMap hN B ≤ ↑g.hom

Phase 4 — uniqueness of val(s) and initiality of Exp

Scott proves homomorphisms out of the iterated colimit are unique by showing they are determined on the finite elements: the projection chain ρₙ = iₙ ∘ jₙ (Proposition 6.12's pair for Texpⁿ({Γ}) ◁ Exp) satisfies T(ρₙ) = ρₙ₊₁ and ⋃ₙ ρₙ = I_Exp, so any homomorphism g equals ⋃ₙ g ∘ ρₙ, a sequence that is forced by the recursion (independent of g). The crux is the concrete "monotone on domains" content (Definition 6.13): the functor Texp carries the canonical 6.12 projection pair of D ◁ E to that of T(D) ◁ T(E) — here a genuine equality of maps over Str (no HEq carrier transport, the whole point of staying in ScottSys).

This section establishes that crux as GExpr.map_inj/GExpr.map_proj (by induction over the six functor constructors), then mirrors Theorem 6.14's uniqueness argument concretely.

Proposition 6.12 helpers: the projection pair is strict, and trivial on `D

◁ D`

theorem Domain.Neighborhood.Exercise619.Subsystem.inj_isStrict {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : Exercise510.IsStrict h.inj

The injection i : D → E of a subsystem is strict: i sends Δ_D only to Δ_E.

theorem Domain.Neighborhood.Exercise619.Subsystem.proj_isStrict {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : Exercise510.IsStrict h.proj

The projection j : E → D of a subsystem is strict.

theorem Domain.Neighborhood.Exercise619.Subsystem.self_inj {α : Type u_1} {D : NeighborhoodSystem α} (h : D ◁ D) : h.inj = ApproximableMap.idMap D

On D ◁ D (e.g. Subsystem.refl), the injection is the identity (both relations are X ∈ D ∧ Y ∈ D ∧ X ⊆ Y).

theorem Domain.Neighborhood.Exercise619.Subsystem.self_proj {α : Type u_1} {D : NeighborhoodSystem α} (h : D ◁ D) : h.proj = ApproximableMap.idMap D

On D ◁ D, the projection is the identity.

The functor carries projection pairs: the token-level lemmas

theorem Domain.Neighborhood.Exercise619.sumMapTok_inj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : sumMapTok h0.inj h1.inj = ⋯.inj

Sum carries the injection. (i₀ + i₁) = i for the sum subsystem: both relate W ↦ W' iff W ∈ 𝒟₀+𝒟₁, W' ∈ ℰ₀+ℰ₁, W ⊆ W'.

theorem Domain.Neighborhood.Exercise619.sumMapTok_proj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : sumMapTok h0.proj h1.proj = ⋯.proj

Sum carries the projection.

theorem Domain.Neighborhood.Exercise619.prodMapTok_inj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : prodMapTok h0.inj h1.inj = ⋯.inj

Product carries the injection.

theorem Domain.Neighborhood.Exercise619.prodMapTok_proj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : prodMapTok h0.proj h1.proj = ⋯.proj

Product carries the projection.

theorem Domain.Neighborhood.Exercise619.oplusMapTok_inj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : oplusMapTok h0.inj h1.inj = ⋯.inj

Coalesced sum carries the injection.

theorem Domain.Neighborhood.Exercise619.oplusMapTok_proj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : oplusMapTok h0.proj h1.proj = ⋯.proj

Coalesced sum carries the projection.

theorem Domain.Neighborhood.Exercise619.otimesMapTok_inj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : otimesMapTok h0.inj h1.inj = ⋯.inj

Smash product carries the injection.

theorem Domain.Neighborhood.Exercise619.otimesMapTok_proj {A₀ A₁ B₀ B₁ : ScottSys} (h0 : A₀.sys ◁ B₀.sys) (h1 : A₁.sys ◁ B₁.sys) : otimesMapTok h0.proj h1.proj = ⋯.proj

Smash product carries the projection.

The crux (Definition 6.13, concrete): T carries the 6.12 projection pair

This is the monotone on domains content of Definition 6.13, but here a genuine equality of maps over the single token type Str (no HEq carrier transport): the functor T = GExpr sends the injection/projection of D ◁ E to the injection/projection of T(D) ◁ T(E). Proved by induction over the six constructors using the token-level lemmas just established.

theorem Domain.Neighborhood.Exercise619.GExpr.map_inj (T : GExpr) {X Y : ScottSys} (h : X.sys ◁ Y.sys) : T.map h.inj = ⋯.inj

T(i) = i' — the functor carries the injection of D ◁ E to that of T(D) ◁ T(E).

theorem Domain.Neighborhood.Exercise619.GExpr.map_proj (T : GExpr) {X Y : ScottSys} (h : X.sys ◁ Y.sys) : T.map h.proj = ⋯.proj

T(j) = j' — the functor carries the projection of D ◁ E to that of T(D) ◁ T(E).

The identity structure isomorphism, relationally

theorem Domain.Neighborhood.Exercise619.isoOfObjEq_hom_rel {X Y : ScottSys} (e : X = Y) {A E : Set ExampleB.Str} : (↑(isoOfObjEq e).hom).rel A E ↔ X.sys.mem A ∧ Y.sys.mem E ∧ A ⊆ E

The forward map of the identity iso isoOfObjEq e is the inclusion X ↪ Y (= idMap across the object equality e).

theorem Domain.Neighborhood.Exercise619.isoOfObjEq_inv_rel {X Y : ScottSys} (e : X = Y) {A E : Set ExampleB.Str} : (↑(isoOfObjEq e).inv).rel A E ↔ Y.sys.mem A ∧ X.sys.mem E ∧ A ⊆ E

The inverse map of the identity iso isoOfObjEq e.

theorem Domain.Neighborhood.Exercise619.expHom_rel {N : ScottSys} (hN : [] ∈ N.sys.master) {A E : Set ExampleB.Str} : (expHom N hN).rel A E ↔ ((Texp N).obj (Exp N hN)).sys.mem A ∧ (Exp N hN).sys.mem E ∧ A ⊆ E

Relational description of the structure map i = expHom (the identity T(Exp) = Exp).

theorem Domain.Neighborhood.Exercise619.expInv_rel {N : ScottSys} (hN : [] ∈ N.sys.master) {A E : Set ExampleB.Str} : (expInv N hN).rel A E ↔ (Exp N hN).sys.mem A ∧ ((Texp N).obj (Exp N hN)).sys.mem E ∧ A ⊆ E

Relational description of the inverse structure map j = expInv.

The projection chain ρₙ = iₙ ∘ jₙ and ⋃ₙ ρₙ = I_Exp

theorem Domain.Neighborhood.Exercise619.expSub {N : ScottSys} (hN : [] ∈ N.sys.master) (n : ℕ) : (gTower (Texp N) n).sys ◁ (Exp N hN).sys

The subdomain Texpⁿ({Γ}) ◁ Exp (Proposition 6.12's pair lives here).

def Domain.Neighborhood.Exercise619.rho {N : ScottSys} (hN : [] ∈ N.sys.master) (n : ℕ) : ApproximableMap (Exp N hN).sys (Exp N hN).sys

ρₙ = iₙ ∘ jₙ : Exp → Exp, the retraction onto Texpⁿ({Γ}).

Equations

• Domain.Neighborhood.Exercise619.rho hN n = ⋯.inj.comp ⋯.proj

theorem Domain.Neighborhood.Exercise619.rho_rel {N : ScottSys} (hN : [] ∈ N.sys.master) (n : ℕ) {A E : Set ExampleB.Str} : (rho hN n).rel A E ↔ (Exp N hN).sys.mem A ∧ (Exp N hN).sys.mem E ∧ ∃ (z : Set ExampleB.Str), (gTower (Texp N) n).sys.mem z ∧ A ⊆ z ∧ z ⊆ E

Scott's relational description A ρₙ E ↔ ∃ z ∈ Texpⁿ({Γ}), A ⊆ z ⊆ E.

theorem Domain.Neighborhood.Exercise619.rho_mono {N : ScottSys} (hN : [] ∈ N.sys.master) {n m : ℕ} (h : n ≤ m) {A E : Set ExampleB.Str} (hr : (rho hN n).rel A E) : (rho hN m).rel A E

ρₙ ⊆ ρₘ for n ≤ m.

def Domain.Neighborhood.Exercise619.iSupRho {N : ScottSys} (hN : [] ∈ N.sys.master) : ApproximableMap (Exp N hN).sys (Exp N hN).sys

The pointwise union ⋃ₙ ρₙ.

Equations

• Domain.Neighborhood.Exercise619.iSupRho hN = Domain.Neighborhood.ApproximableMap.iSupMap (Domain.Neighborhood.Exercise619.rho hN) ⋯

theorem Domain.Neighborhood.Exercise619.iSupRho_eq_id {N : ScottSys} (hN : [] ∈ N.sys.master) : iSupRho hN = ApproximableMap.idMap (Exp N hN).sys

⋃ₙ ρₙ = I_Exp (Scott's key identity).

theorem Domain.Neighborhood.Exercise619.rho_zero_rel {N : ScottSys} (hN : [] ∈ N.sys.master) {A E : Set ExampleB.Str} : (rho hN 0).rel A E ↔ (Exp N hN).sys.mem A ∧ E = (Exp N hN).sys.master

ρ₀ = ⊥ (the generator {Γ} is one-point): ρ₀ relates A only to the master.

The crux equation ρₙ₊₁ = i ∘ T(ρₙ) ∘ j

theorem Domain.Neighborhood.Exercise619.map_rho_eq {N : ScottSys} (hN : [] ∈ N.sys.master) (n : ℕ) : (Texp N).map (rho hN n) = ⋯.inj.comp ⋯.proj

T(ρₙ) = T(iₙ) ∘ T(jₙ) = i'ₙ ∘ j'ₙ, the projection pair of T(Texpⁿ{Γ}) ◁ T(Exp).

theorem Domain.Neighborhood.Exercise619.key_rho {N : ScottSys} (hN : [] ∈ N.sys.master) (n : ℕ) : rho hN (n + 1) = (expHom N hN).comp (((Texp N).map (rho hN n)).comp (expInv N hN))

ρₙ₊₁ = i ∘ T(ρₙ) ∘ j (Scott's T(ρₙ) = ρₙ₊₁, conjugated by the structure iso).

g-independence of g ∘ ρₙ and uniqueness

theorem Domain.Neighborhood.Exercise619.gcomp_rho_zero {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (g : AlgHom (ExpAlg N hN) B) : (↑g.hom).comp (rho hN 0) = descRel hN B 0

The base of the recursion: g ∘ ρ₀ = ⊥ = val₀, independent of g.

theorem Domain.Neighborhood.Exercise619.gcomp_rho_succ {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (g : AlgHom (ExpAlg N hN) B) (n : ℕ) : (↑g.hom).comp (rho hN (n + 1)) = (algStr B).comp (((Texp N).map ((↑g.hom).comp (rho hN n))).comp (expInv N hN))

The fixed-point recursion gₙ₊₁ = k ∘ T(gₙ) ∘ j (key_rho + the homomorphism square).

theorem Domain.Neighborhood.Exercise619.gcomp_rho_eq {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (g : AlgHom (ExpAlg N hN) B) (n : ℕ) : (↑g.hom).comp (rho hN n) = descRel hN B n

g ∘ ρₙ = val₀ₙ: every homomorphism g agrees with the canonical Kleene iterate after the n-th projection — the sequence is forced by the recursion, independent of g.

theorem Domain.Neighborhood.Exercise619.descMap_eq_algHom {N : ScottSys} (hN : [] ∈ N.sys.master) (B : TAlgebra (TexpF N)) (g : AlgHom (ExpAlg N hN) B) : ↑g.hom = descMap hN B

The underlying map of any homomorphism g : Exp → D is val = descMap. Hence descAlgHom is the unique homomorphism.

theorem Domain.Neighborhood.Exercise619.algHom_ext {N : ScottSys} {A C : TAlgebra (TexpF N)} {g g' : AlgHom A C} (h : g.hom = g'.hom) : g = g'

Two algebra homomorphisms with equal underlying maps are equal.

def Domain.Neighborhood.Exercise619.ExpInitial {N : ScottSys} (hN : [] ∈ N.sys.master) : IsInitial (ExpAlg N hN)

Exercise 6.23 (Scott 1981, PRG-19) — Exp is the initial T-algebra. For every algebra B = (D, s, u, v) there is a unique homomorphism val(s) : Exp → D — Scott's evaluation of an expression. Existence is descAlgHom (Phase 3); uniqueness is the projection-chain argument.

Equations

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