# How to show that only this regular expression solves this equation

Consider the equation

$$x=v\cdot x + w$$

where $$x$$ is a variable regular expression, $$v, w$$ are fixed regular expressions, $$v$$ has no variables inside it, and $$w$$ has no $$x$$ inside it.

It is easy to show that $$x=v^*\cdot w$$ solves this equation:

$$v\cdot v^*\cdot w+w=(v\cdot v^*+1)\cdot w=v^*\cdot w$$.

But how to show that there are no other solutions?

As already noted, you run into problems if you formulate everything in terms of equations. This idea stems from the 1960's literature - and is wrong. The right way to formulate this emerged in the 1990's, which is as a system of inequations, with the least solution being the one sought for. In effect, it's a non-numeric form of optimization, though neither the literature of the time (nor since) has explicitly laid it out that way.

Textbooks, apparently have not come up to speed on this, if we're still seeing this formulated in terms of equations.

So, for your problem, the system is a single inequation: $$x ≥ v x + w.$$ Since the variable is on both sides of the inequation, then it's a fixed-point system: a system of the form $$x ≥ φ(x)$$ where one seeks out a fixed point of $$x ↦ φ(x)$$. The least fixed point is referred to as $$μx·φ(x)$$. Correspondingly, the expression you're looking for is $$μx·(v x + w).$$

For Kleene algebras, one of its fundamental properties is that if $$x ≥ vx$$ then $$x ≥ v^* x$$, and indeed the two are equivalent. Another fundamental property is that $$a + b$$ is the least upper bound of $$\{a,b\}$$, so that $$x ≥ v x + w$$ is equivalent to $$x ≥ v x,\quad x ≥ w,$$ and, in turn, to $$x ≥ v^* x,\quad x ≥ w.$$

Another fundamental property, also a consequence of "+" being the least upper bound operator, and of distributivity, which is that if $$a ≥ b$$ then $$c a ≥ c b$$. For, assume $$a ≥ b$$. Then $$a = a + b$$. Thus $$c a = c (a + b) = c a + c b$$. From this, it follows that $$c a ≥ c b$$.

Therefore, from $$x ≥ v^* x$$ and $$x ≥ w$$ follows $$x ≥ v^* w$$. Therefore, $$v^* w$$ is a lower bound to all fixed-point solutions to $$x ≥ v x + w$$.

Another fundamental property of Kleene algebras is the identity $$a^* ≥ 1 + a a^*$$. From this, we may write $$v^* w ≥ (1 + v v^*) w = w + v v^* w,$$ which shows that $$v^* w$$ is a solution, for $$x$$, to $$x ≥ v x + w$$. Therefore, $$v^* w$$ is the least fixed point solution, and we have $$μx·(v x + w) = v^* w.$$

The defining properties of semirings, along with the identity $$a = a + a$$ (idempotency - which makes the semiring an idempotent semiring, sometimes also called a dioid), along with the properties $$a^* ≥ 1 + a a^*,\quad x ≥ a x → x ≥ a^* x,\quad x ≥ x b → x ≥ x b^*,$$ where the relation $$≥$$ is the partial ordering inherited from the dioid (defined by $$a ≥ b$$ if and only if $$a = a + b$$), provides a complete axiomatization for regular expressions and a (weak) axiomatization for Kleene algebra.

The axioms are strong enough, for instance, to prove Parikh's Theorem in a purely algebraic manner; in particular to show that - when the Kleene algebra is commutative (i.e. satisfies $$ab = ba$$), then $$μx·φ(x)$$ = $$φ'(φ(0))^* φ(0)$$, where $$φ(x)$$ is any Kleene algebraic expression formed out of $$x$$, with derivatives defined such that $$d(x^*)/dx = x^*$$. For commutative Kleene algebras, the star behaves like the exponential: $$(a + b)^* = a^* b^*$$ and $$0^* = 1$$.

However, the axioms are not strong enough to encapsulate the property that from $$x ≥ p o^n q$$ for $$n = 0, 1, 2, ⋯$$ should follow $$x ≥ p o^* q$$ (the *-continuity property). That property turns out to be important if you want to solve non-linear fixed point systems when the Kleene algebra is non-commutative. That's the way of dealing with context-free languages/grammars and translation grammars algebraically. For that, you need both *-continuity and the stronger (still) property that if $$x ≥ p φ^n(0) q$$, for $$n = 0, 1, 2, ⋯$$, where $$φ^0(y) = y$$, $$φ^{n+1}(y) = φ(φ^n(y))$$, for $$n = 0, 1, 2, ⋯$$, then $$x ≥ p (μy·φ(y)) q$$. That's called μ-continuity. For μ-continuous Kleene algebras, you have fixed-point closure and you can even devise an algebra and a calculus for context-free expressions - ultimately based on the Chomsky-Schützenberger Theorem. That's a recently-published development, (2023, in LNCS 13869, 122-139).

• Thanks for this, which I found very interesting. Can you provide a reference for the formalization which you say emerged in the 1990s? I see that Wikipedia refers to a survey by Dexter Kozen from 1990, “On Kleene Algebras and Closed Semirings”.
– MJD
Apr 1 at 3:05
• Very good! That's the precursor that involved the *-continuity property, which he found first before he found the other, weaker, axiomatization. I know it was peer-reviewed around 1995, but apparently he open-accessed his own copy over here A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Apr 1 at 11:52
• Thanks very much!
– MJD
Apr 1 at 12:04

This is not true. If $$v$$ contains the empty word, then the solutions are the languages of the form $$v^*z$$ with $$w \subseteq z$$.