Exercise 4.17 (Scott 1981, PRG-19, Lecture IV) — least solution in a monoid

power-set

(For algebraists.) Let ⟨S, 1, ·⟩ be a monoid (a semi-group with unit). Then P S is a domain — in fact a complete lattice (Exercise 4.14). For a, b ∈ S, what is the least x ∈ P S with

x = {1} ∪ {a, b} ∪ x · x, where x · y = {t · u ∣ t ∈ x, u ∈ y}?

Answer. The least solution is the submonoid generated by {a, b} — i.e. the set of all finite products of as and bs (including the empty product 1):

lfpSet (F a b) = ⟨{a, b}⟩ (= Submonoid.closure {a, b}).

The operator F a b x = {1} ∪ {a, b} ∪ x · x is monotone (pointwise · is monotone), so by Exercise 4.14 (the dual Knaster–Tarski over the complete lattice P S) its least fixed point lfpSet (F a b) exists; we identify it with the submonoid closure (lfpSet_eq_closure): a fixed point of F is exactly a submonoid containing {a, b}, and the least such is the closure.

Need the fixed point be unique? No. In any monoid the whole set Set.univ is also a fixed point (F a b univ = univ, since s = 1 · s ∈ univ · univ). So whenever the monoid is not generated by {a, b} there are at least two fixed points: taking S = ℕ (under ·) and a = b = 1, the least solution is {1} while Set.univ is another (fixedPoint_not_unique).

The constructions are choice-free (#print axioms ⊆ {propext, Quot.sound}), inheriting lfpSet from Exercise 4.14.

def Domain.Neighborhood.Exercise417.F {S : Type u_1} [Monoid S] (a b : S) (x : Set S) : Set S

Scott's operator F(x) = {1} ∪ {a, b} ∪ x · x on P S.

Equations

• Domain.Neighborhood.Exercise417.F a b x = {1} ∪ {a, b} ∪ x * x

theorem Domain.Neighborhood.Exercise417.F_monotone {S : Type u_1} [Monoid S] (a b : S) : Monotone (F a b)

theorem Domain.Neighborhood.Exercise417.base_subset_F {S : Type u_1} [Monoid S] (a b : S) (x : Set S) : {1} ∪ {a, b} ⊆ F a b x

{1} ∪ {a, b} ⊆ F a b x.

theorem Domain.Neighborhood.Exercise417.self_mul_subset_F {S : Type u_1} [Monoid S] (a b : S) (x : Set S) : x * x ⊆ F a b x

theorem Domain.Neighborhood.Exercise417.one_mem_F {S : Type u_1} [Monoid S] (a b : S) (x : Set S) : 1 ∈ F a b x

theorem Domain.Neighborhood.Exercise417.a_mem_F {S : Type u_1} [Monoid S] (a b : S) (x : Set S) : a ∈ F a b x

theorem Domain.Neighborhood.Exercise417.b_mem_F {S : Type u_1} [Monoid S] (a b : S) (x : Set S) : b ∈ F a b x

The least solution.

theorem Domain.Neighborhood.Exercise417.leastSolution_eq {S : Type u_1} [Monoid S] (a b : S) : F a b (Exercise414.lfpSet (F a b)) = Exercise414.lfpSet (F a b)

The least solution lfpSet (F a b) indeed solves Scott's equation x = {1} ∪ {a, b} ∪ x · x.

def Domain.Neighborhood.Exercise417.preFixSubmonoid {S : Type u_1} [Monoid S] (a b : S) {x : Set S} (hx : F a b x ⊆ x) : Submonoid S

A pre-fixed point of F is a submonoid containing {a, b}: it contains 1 and is closed under multiplication and contains a, b. Packaged as the submonoid with that carrier.

Equations

• Domain.Neighborhood.Exercise417.preFixSubmonoid a b hx = { carrier := x, mul_mem' := ⋯, one_mem' := ⋯ }

theorem Domain.Neighborhood.Exercise417.lfpSet_eq_closure {S : Type u_1} [Monoid S] (a b : S) : Exercise414.lfpSet (F a b) = ↑(Submonoid.closure {a, b})

Exercise 4.17 (Scott 1981, PRG-19). The least solution of x = {1} ∪ {a, b} ∪ x · x is the submonoid generated by {a, b} (all finite products of as and bs, including 1).

Non-uniqueness.

theorem Domain.Neighborhood.Exercise417.F_univ {S : Type u_1} [Monoid S] (a b : S) : F a b Set.univ = Set.univ

In any monoid, Set.univ is a fixed point of F a b: s = 1 · s ∈ univ · univ.

theorem Domain.Neighborhood.Exercise417.F_one_one_singleton : F 1 1 {1} = {1}

{1} is a fixed point of F 1 1: {1} ∪ {1, 1} ∪ {1}·{1} = {1}.

theorem Domain.Neighborhood.Exercise417.fixedPoint_not_unique : ∃ (x : Set ℕ) (y : Set ℕ), F 1 1 x = x ∧ F 1 1 y = y ∧ x ≠ y

Exercise 4.17 (Scott 1981, PRG-19). The fixed point need not be unique: over S = ℕ (under ·) with a = b = 1, both {1} (the least solution) and Set.univ solve the equation, and they are distinct.