<p>You might be interested in <strong>bounded synchronization delay expressions</strong>.
See [1] for details on these expressions.
To sum up, they are equivalent to star-free expressions, but instead of using complement, they restrict the use of the Kleene star to certain languages: the <em>prefix codes with bounded synchronization delay</em>.</p>

<p>This way, you can have your characterization: <span class="math-container">$L(r_1)=L(r_2)$</span> iff we can prove <span class="math-container">$r_1=r_2$</span> using the axioms of Kleene Algebra, the only difference being that <span class="math-container">$r_1$</span> and <span class="math-container">$r_2$</span> are more constrained on the use of Kleene star, and only represent star-free languages.</p>

<p>On the other hand, axiomatization of regular expressions with complement has been done in [2], so after careful verification, you could possibly use this to axiomatize star-free expressions directly.</p>

<p>[1] <em>Diekert, V.; Kufleitner, M.</em>, <a href="http://dx.doi.org/10.1007/978-3-642-30642-6_10" rel="noreferrer"><strong>Bounded synchronization delay in omega-rational expressions</strong></a>, Hirsch, Edward A. (ed.) et al., Computer science – theory and applications. 7th international computer science symposium in Russia, CSR 2012.</p>

<p>[2] 
<em>Salomaa, A.; Tixier, V.</em>, <a href="http://dx.doi.org/10.1109/TC.1968.227424" rel="noreferrer"><strong>Two complete axiom systems for the extended language of regular expressions</strong></a>, IEEE Trans. Comput. 17, 700-701 (1968). <a href="https://zbmath.org/?q=an:0174.29001" rel="noreferrer">ZBL0174.29001</a>.</p>

CC BY-SA 4.0
2020-04-23T14:22:25.783Z
2020-04-23T14:32:41.430Z
2020-04-23T14:32:41.430Z
Denis
<p>TLDR: Is there a notion of Kleene Algebra for star-free regular expressions?</p>

<p><strong>Kleene Algebras</strong> are algebraic structures that are equivalent to regular expressions. A Kleene Algebra is an idempotent semiring (non-commutative multiplication) with an extra unary operation <span class="math-container">$*$</span> that satisfies that following equations:
<span class="math-container">\begin{align}
&amp;1+x\cdot x^* = x^* \\ &amp;1+x^*\cdot x = x^* \\ &amp;z+xy\le y \implies x^*\cdot z\le y \\ &amp;z+yx\le y \implies z\cdot x^*\le y
\end{align}</span>
where <span class="math-container">$x\le y$</span> means there exists <span class="math-container">$z$</span> such that <span class="math-container">$x+z=y$</span>. Equivalence with regular expressions formally means, given regular expressions <span class="math-container">$r_1$</span> and <span class="math-container">$r_2$</span>, <span class="math-container">$\mathcal{L}(r_1)=\mathcal{L}(r_2)$</span> iff we can prove <span class="math-container">$r_1=r_2$</span> using the axioms of Kleene Algebra.</p>

<p><strong>Star-free regular expressions</strong> are regular expressions without the Kleene star but with the ability to take complements i.e. <span class="math-container">$$r_1,r_2::= \emptyset\mid a,b,c\in A\mid r_1\cup r_2\mid r_1\cap r_2\mid r_1\cdot r_2\mid (r_1)^c$$</span> where <span class="math-container">$A$</span> is the set of alphabets. Observe that complementation restores some Kleene star powers but not all: <span class="math-container">$A^*=(\emptyset)^c$</span> while <span class="math-container">$(aa)^*$</span> has no star-free form. </p>

<p>I was wondering how to tweak Kleene Algebra so that we capture exactly star-free expressions. While coming up with equation templates for the complementation operation the challenge is to get an equation for <span class="math-container">$(r_1\cdot r_2)^c$</span> because the rest of the interleaving of operations is taken care of by De Morgan's laws. Also, since Kleene Algebras do not explicitly talk about the alphabet set, I guess <span class="math-container">$a^c$</span> should be considered a normal form.</p>

<regular-language><algebra><regular-expressions><first-order-logic>
Kleene Algebra for star-free regular expressions
Faustus
# Kleene Algebra for star-free regular expressions

(Asked by: username_0 on 2020-04-23)

TLDR: Is there a notion of Kleene Algebra for star-free regular expressions?

**Kleene Algebras** are algebraic structures that are equivalent to regular expressions. A Kleene Algebra is an idempotent semiring (non-commutative multiplication) with an extra unary operation $\*$ that satisfies that following equations:
\begin{align}
&1+x\cdot x^\* = x^\* \\ &1+x^\*\cdot x = x^\* \\ &z+xy\le y \implies x^\*\cdot z\le y \\ &z+yx\le y \implies z\cdot x^\*\le y
\end{align}
where $x\le y$ means there exists $z$ such that $x+z=y$. Equivalence with regular expressions formally means, given regular expressions $r\_1$ and $r\_2$, $\mathcal{L}(r\_1)=\mathcal{L}(r\_2)$ iff we can prove $r\_1=r\_2$ using the axioms of Kleene Algebra.

**Star-free regular expressions** are regular expressions without the Kleene star but with the ability to take complements i.e. $$r\_1,r\_2::= \emptyset\mid a,b,c\in A\mid r\_1\cup r\_2\mid r\_1\cap r\_2\mid r\_1\cdot r\_2\mid (r\_1)^c$$ where $A$ is the set of alphabets. Observe that complementation restores some Kleene star powers but not all: $A^\*=(\emptyset)^c$ while $(aa)^\*$ has no star-free form.

I was wondering how to tweak Kleene Algebra so that we capture exactly star-free expressions. While coming up with equation templates for the complementation operation the challenge is to get an equation for $(r\_1\cdot r\_2)^c$ because the rest of the interleaving of operations is taken care of by De Morgan's laws. Also, since Kleene Algebras do not explicitly talk about the alphabet set, I guess $a^c$ should be considered a normal form.

**Tags:** regular-language, algebra, regular-expressions, first-order-logic


---

## 1 answers

### Answer by username_1 on 2020-04-23. Score: 7 | Accepted answer

You might be interested in **bounded synchronization delay expressions**.
See [1] for details on these expressions.
To sum up, they are equivalent to star-free expressions, but instead of using complement, they restrict the use of the Kleene star to certain languages: the *prefix codes with bounded synchronization delay*.

This way, you can have your characterization: $L(r\_1)=L(r\_2)$ iff we can prove $r\_1=r\_2$ using the axioms of Kleene Algebra, the only difference being that $r\_1$ and $r\_2$ are more constrained on the use of Kleene star, and only represent star-free languages.

On the other hand, axiomatization of regular expressions with complement has been done in [2], so after careful verification, you could possibly use this to axiomatize star-free expressions directly.

[1] *Diekert, V.; Kufleitner, M.*, [**Bounded synchronization delay in omega-rational expressions**](http://dx.doi.org/10.1007/978-3-642-30642-6_10), Hirsch, Edward A. (ed.) et al., Computer science – theory and applications. 7th international computer science symposium in Russia, CSR 2012.

[2]
*Salomaa, A.; Tixier, V.*, [**Two complete axiom systems for the extended language of regular expressions**](http://dx.doi.org/10.1109/TC.1968.227424), IEEE Trans. Comput. 17, 700-701 (1968). [ZBL0174.29001](https://zbmath.org/?q=an:0174.29001).


---

