# Kleene Algebra for star-free regular expressions

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.

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.