Exercise 5.15 (Scott 1981, PRG-19, Lecture V) — free-semigroup powerset and

Arden's lemma

(For algebraists.) Regard ⟨{0,1}*, Λ, ·⟩ as the free semigroup on two generators. The powerset P{0,1}* is a domain (Exercise 4.17). For a word e set e* = {Λ, e, e², …}.

(1) The least fixed point of z = {e}·z ∪ {e'} is z = e*·{e'}. (2) (David Park) The least solution of x = a·x ∪ b·y ∪ c, y = b·x ∪ a·y ∪ d is x = (a ∪ b·a*·b)*·(c ∪ b·a*·d), where z* = Λ ∪ z*·z.

Following Exercise 4.17, the powerset domain P S of a monoid S is the complete lattice (Set S, ⊆) with pointwise product s·t = {u·v ∣ u ∈ s, v ∈ t} (Set.mul, open Pointwise). Both parts are facts about the Kleene algebra (Set S, ∪, ·, ∅, {1}) and hold for any monoid; we prove them with S a general Monoid and specialise part (1) to S = FreeMonoid Bool = {0,1}*.

Choice discipline

Mathlib's Set-level multiplicative lemmas (mul_assoc, Set.union_mul, Set.mul_union, Set.singleton_mul_singleton), the order lemmas Set.subset_iUnion/Set.iUnion_subset, Set-power (pow_succ'), Submonoid.mem_powers_iff, and Monotone over Set all depend on Classical.choice in this toolchain (they route through Set.image2/CompleteLattice choice-using machinery). Every membership iff (Set.mem_mul, Set.mem_union, Set.mem_one, Set.mem_singleton_iff) and every element-level monoid lemma is choice-free. So we reprove the small slice of Kleene algebra we need (smul_assoc, sunion_mul, smul_union) at the membership level, define star by an explicit recursion (kpow) rather than ⋃ₙ zⁿ, and phrase Arden's lemma without Monotone — keeping everything choice-free (#print axioms ⊆ {propext, Quot.sound}).

A choice-free slice of Kleene algebra on Set S

theorem Domain.Neighborhood.Exercise515.smul_assoc {S : Type u_1} [Monoid S] (a b c : Set S) : a * b * c = a * (b * c)

Associativity of the pointwise product (membership proof, choice-free).

theorem Domain.Neighborhood.Exercise515.sunion_mul {S : Type u_1} [Monoid S] (a b c : Set S) : (a ∪ b) * c = a * c ∪ b * c

Right distributivity (a ∪ b)·c = a·c ∪ b·c (choice-free).

theorem Domain.Neighborhood.Exercise515.smul_union {S : Type u_1} [Monoid S] (a b c : Set S) : a * (b ∪ c) = a * b ∪ a * c

Left distributivity a·(b ∪ c) = a·b ∪ a·c (choice-free).

The star z* = ⋃ₙ zⁿ, by explicit recursion

def Domain.Neighborhood.Exercise515.kpow {S : Type u_1} [Monoid S] (z : Set S) : ℕ → Set S

zⁿ as an iterated pointwise product (left-recursion z^{n+1} = z·zⁿ).

Equations

• Domain.Neighborhood.Exercise515.kpow z 0 = 1
• Domain.Neighborhood.Exercise515.kpow z n.succ = z * Domain.Neighborhood.Exercise515.kpow z n

@[simp]

theorem Domain.Neighborhood.Exercise515.kpow_zero {S : Type u_1} [Monoid S] (z : Set S) : kpow z 0 = 1

@[simp]

theorem Domain.Neighborhood.Exercise515.kpow_succ {S : Type u_1} [Monoid S] (z : Set S) (n : ℕ) : kpow z (n + 1) = z * kpow z n

def Domain.Neighborhood.Exercise515.star {S : Type u_1} [Monoid S] (z : Set S) : Set S

Scott's z*: the set of all finite products of elements of z (including the empty product 1). Defined as {s ∣ ∃ n, s ∈ zⁿ} to stay choice-free (avoiding ⋃ order lemmas).

Equations

• Domain.Neighborhood.Exercise515.star z = {s : S | ∃ (n : ℕ), s ∈ Domain.Neighborhood.Exercise515.kpow z n}

theorem Domain.Neighborhood.Exercise515.mem_star {S : Type u_1} [Monoid S] {z : Set S} {s : S} : s ∈ star z ↔ ∃ (n : ℕ), s ∈ kpow z n

theorem Domain.Neighborhood.Exercise515.star_eq {S : Type u_1} [Monoid S] (z : Set S) : star z = 1 ∪ z * star z

Scott's unfolding z* = Λ ∪ z·z*.

theorem Domain.Neighborhood.Exercise515.star_mul_isFixed {S : Type u_1} [Monoid S] (z v : Set S) : z * (star z * v) ∪ v = star z * v

z*·v is a fixed point of w ↦ z·w ∪ v: the star identity z·(z*·v) ∪ v = z*·v.

theorem Domain.Neighborhood.Exercise515.star_mul_subset_prefixed {S : Type u_1} [Monoid S] (z v x : Set S) (hx : z * x ∪ v ⊆ x) : star z * v ⊆ x

For any prefixed point w₀ of w ↦ z·w ∪ v (i.e. z·w₀ ∪ v ⊆ w₀), the candidate z*·v is below w₀: the induction zⁿ·v ⊆ w₀.

Arden's lemma

def Domain.Neighborhood.Exercise515.G {S : Type u_1} [Monoid S] (z v w : Set S) : Set S

Scott's operator w ↦ z·w ∪ v, whose least fixed point is the least solution of w = z·w ∪ v.

Equations

• Domain.Neighborhood.Exercise515.G z v w = z * w ∪ v

theorem Domain.Neighborhood.Exercise515.arden {S : Type u_1} [Monoid S] (z v : Set S) : Exercise414.lfpSet (G z v) = star z * v

Arden's lemma. The least solution of w = z·w ∪ v in P S is z*·v. (Stated via lfpSet, Exercise 4.14; the proof uses neither Monotone nor ⋃ order lemmas, so it is choice-free.)

Part (1): the single equation z = {e}·z ∪ {e'}

theorem Domain.Neighborhood.Exercise515.mem_kpow_singleton {S : Type u_1} [Monoid S] (e s : S) (n : ℕ) : s ∈ kpow {e} n ↔ s = e ^ n

{e}ⁿ = {eⁿ} at the membership level (choice-free).

theorem Domain.Neighborhood.Exercise515.mem_star_singleton {S : Type u_1} [Monoid S] (e s : S) : s ∈ star {e} ↔ ∃ (n : ℕ), s = e ^ n

{e}* = e* = {Λ, e, e², …}: a point lies in star {e} iff it is some power of e.

theorem Domain.Neighborhood.Exercise515.part1 {S : Type u_1} [Monoid S] (e e' : S) : (Exercise414.lfpSet fun (w : Set S) => {e} * w ∪ {e'}) = star {e} * {e'}

Exercise 5.15(1). The least fixed point of z = {e}·z ∪ {e'} is e*·{e'} (star {e} is e* by mem_star_singleton).

theorem Domain.Neighborhood.Exercise515.part1_freeMonoid (e e' : FreeMonoid Bool) : (Exercise414.lfpSet fun (w : Set (FreeMonoid Bool)) => {e} * w ∪ {e'}) = star {e} * {e'}

The free semigroup {0,1}* of the exercise. Part (1) holds here as a special case.

Part (2): David Park's simultaneous system

def Domain.Neighborhood.Exercise515.parkA {S : Type u_1} [Monoid S] (a b : Set S) : Set S

The "feedback" coefficient A = a ∪ b·a*·b of the eliminated system.

Equations

• Domain.Neighborhood.Exercise515.parkA a b = a ∪ b * Domain.Neighborhood.Exercise515.star a * b

def Domain.Neighborhood.Exercise515.parkC {S : Type u_1} [Monoid S] (a b c d : Set S) : Set S

The "feedback" constant C = c ∪ b·a*·d.

Equations

• Domain.Neighborhood.Exercise515.parkC a b c d = c ∪ b * Domain.Neighborhood.Exercise515.star a * d

def Domain.Neighborhood.Exercise515.parkX {S : Type u_1} [Monoid S] (a b c d : Set S) : Set S

Park's least solution for x: x₀ = (a ∪ b·a*·b)*·(c ∪ b·a*·d).

Equations

• Domain.Neighborhood.Exercise515.parkX a b c d = Domain.Neighborhood.Exercise515.star (Domain.Neighborhood.Exercise515.parkA a b) * Domain.Neighborhood.Exercise515.parkC a b c d

def Domain.Neighborhood.Exercise515.parkY {S : Type u_1} [Monoid S] (a b c d : Set S) : Set S

The accompanying least solution for y: y₀ = a*·(b·x₀ ∪ d).

Equations

• Domain.Neighborhood.Exercise515.parkY a b c d = Domain.Neighborhood.Exercise515.star a * (b * Domain.Neighborhood.Exercise515.parkX a b c d ∪ d)

theorem Domain.Neighborhood.Exercise515.parkX_eq {S : Type u_1} [Monoid S] (a b c d : Set S) : parkX a b c d = a * parkX a b c d ∪ b * parkY a b c d ∪ c

x₀ satisfies the first equation x = a·x ∪ b·y ∪ c.

theorem Domain.Neighborhood.Exercise515.parkY_eq {S : Type u_1} [Monoid S] (a b c d : Set S) : parkY a b c d = b * parkX a b c d ∪ a * parkY a b c d ∪ d

y₀ satisfies the second equation y = b·x ∪ a·y ∪ d.

theorem Domain.Neighborhood.Exercise515.park_solves {S : Type u_1} [Monoid S] (a b c d : Set S) : parkX a b c d = a * parkX a b c d ∪ b * parkY a b c d ∪ c ∧ parkY a b c d = b * parkX a b c d ∪ a * parkY a b c d ∪ d

Exercise 5.15(2), existence. (x₀, y₀) solves David Park's system.

theorem Domain.Neighborhood.Exercise515.park_least {S : Type u_1} [Monoid S] (a b c d : Set S) {x y : Set S} (hx : x = a * x ∪ b * y ∪ c) (hy : y = b * x ∪ a * y ∪ d) : parkX a b c d ⊆ x ∧ parkY a b c d ⊆ y

Exercise 5.15(2), leastness. Any solution (x, y) of the system dominates (x₀, y₀). Hence (x₀, y₀) is the least solution, and x₀ = (a ∪ b·a*·b)*·(c ∪ b·a*·d) as claimed. The proof is Gaussian elimination: solve the second equation for y by arden, substitute, apply arden again.