According to Redko the equational theory of regular languages with operations $+, \cdot, *$ over a single letter has no finite set of axioms.

Why does this imply that it has no finite set of axioms over an arbitrary alphabet?

Suppose I have a finite set of axioms for the equational theory of an alphabet with more than one letter, how would this give a finite set of axioms for the single letter case? I mean in the single letter case we have additional equations which did not hold in the arbitrary case, for examle $AB = BA$ for two languages $A,B$, and therefore which could not be derived from the axioms, hence these axioms do not axiomatize the single letter case.

Some clarification as asked for in the comments: Given a fixed alphabet $\Sigma$ and a set of variables $X = \{A,B,C,\ldots\}$, the terms are inductively defined:

1) Every $a \in \Sigma$ is a term,

2) Every variable $X$ is a term,

3) If $s,t$ are terms, then $s + t, s\cdot t, t^{\ast}$ are terms.

The interpretation of the regular sets $\mathcal{Reg}(\Sigma)\subseteq \mathcal P(\Sigma^{\ast})$ is as usual. As written in the comments, as set of terms $\Gamma$ axiomises $\mathcal{Reg}(\Sigma)$, the regular languages over a given alphabet $\Sigma$, if $$ \Gamma \vdash t_1 = t_2 \mbox{ iff } \mathcal{Reg}(\Sigma) \models t_1 = t_2. $$ Where $t_1, t_2$ are terms with alphabet letters from $\Sigma$, and variables are interpreted as universally quantified. The only rule of interference being substitution, that I mean by equational logic.

  • $\begingroup$ Is there a reference in English? $\endgroup$
    – Leo163
    Commented May 6, 2018 at 11:39
  • 1
    $\begingroup$ I had not read the russian article either, but I know the proofs in the unary alphabet case from A. Ginsburg, Algebraic Theory of Automata and J.H. Conway Regular Algebra and Machines. But they both do not give details for how the result for arbitrary alphabets is implied. $\endgroup$
    – StefanH
    Commented May 6, 2018 at 11:45
  • $\begingroup$ Nice question! Two little facts: (1) $L + \{a\}^* = \{a\}^*$ is equivalent to saying that the language $L$ uses only the single letter $a$; (2) the conjunction $(t_1 = u_1) \land (t_2 = u_2)$ is equivalent to the equality $(a_1 t_1 + a_2 t_2) = (a_1 u_1 + a_2 u_2)$, where we expand the alphabet to add two new letters $a_1,a_2$ that aren't mentioned in $t_1,t_2,u_1,u_2$, so we can express conjunctions of equalities as a single equality (in the case of a multi-letter alphabet). I can't see how to use this to prove a reduction, though. $\endgroup$
    – D.W.
    Commented May 6, 2018 at 20:48
  • $\begingroup$ @D.W. Today I had an idea to prove it, but it is based on the knowledge that we know a complete axiom system for unary languages. See me own answer. $\endgroup$
    – StefanH
    Commented May 7, 2018 at 8:41
  • 1
    $\begingroup$ A related question and another one on other stackexchange sites. $\endgroup$
    – J.-E. Pin
    Commented Apr 29, 2020 at 11:01

2 Answers 2


For each $k > 0$, the equation $$ A^{\ast} = (A^k)^{\ast}(1 + A + A^2 + \ldots + A^{k-1}) $$ holds for regular languages over every alphabet, hence if for some alphabet we have a finite axiomatization, this equation is provable from it. Now as shown in A. Ginsburg, Algebraic Theory of Automata, the following infinite system of axioms is complete for unary regular languages. \begin{align*} A + B & = B + A \\ A + (B + C) & = (A + B) + C \\ A + A & = A \\ A + \emptyset & = A \\ AB &= BA \\ (AB)C & = A(BC) \\ A1 & = A \\ A \emptyset & = \emptyset \\ (A+B)C & = AC + BC \\ 1^{\ast} & = 1, \emptyset^{\ast} = 1 \\ (AB^{\ast})^{\ast} & = 1 + AA^{\ast}B^{\ast} \\ (A + B)^{\ast} & = A^{\ast} B^{\ast} \\ A^{\ast} & = (A^k)^{\ast}(1 + A + A^2 + \ldots + A^{k-1}), \quad k > 0 \end{align*} So we get a finite axiomatisation for unary languages, if we take but the last family of axioms, and all axioms from the finite axiom system for some alphabet that prove $$ A^{\ast} = (A^k)^{\ast}(1 + A + A^2 + \ldots + A^{k-1}) $$ for each $k > 0$. Then all of the above equations are derivable by this finite axiom system, and as the above one is complete, this finite axiom system would be complete, which is not possible. Hence there is no finite system of axioms for any alphabet.


The axioms $$ (a b) c = a (b c),\quad a 1 = a = 1 a,\quad a 0 b = 0,\quad a (b + c) d = a b d + a c d,\\ (a + b) + c = a + (b + c),\quad a + 0 = a = 0 + a,\quad a + b = b + a,\quad a + a = a,\\ a^* ≥ 1 + a a^*,\quad a ≥ b a → a ≥ b^* a,\quad a ≥ a c → a → a c^*, $$ are complete, where the partial ordering relation is the innate one associated with the upper semi-lattice structure formed by $(0,+)$, given by $b ≤ a ⇔ a ≥ b ⇔ a = a + b$. More precisely, the algebra freely generated from a set $X$ is isomorphic to the Kleene algebra of regular expressions over $X$; i.e. the algebra of regular subsets of the free monoids $X^*$. In case that's not clear: this means every equation that holds between regular subsets of $X^*$ can be proven using these axioms. With respect to the ordering relation, $0$ is the minimum element and $+$ is the supremum operator.

This result is well-known and was established in the 1990's by Kozen (The Completeness Theorem). There is another, more direct, proof that involves the Kleene-algebraic analogue of intertwining operators that I may post elsewhere, later, soon. If so, then I'll post a link in a comment. There is an, as-yet undeveloped, representation theory for Kleene algebras and of "idempotent power series" (over arbitrary monoids) that underlies all of this.

The result that is being alluded to is Conway's "no go" theorem for equational axiomatizations (which might be in his 1971 book on "Regular" algebra). Although interesting, it misses a key point that first order axiomatizations can also use Horn clauses and be implicational, not just equational. This confusion set back the field 30 years, in much the same way that Minsky's "no go" result in his Perceptrons book did for the field of neural nets.

When the infinitary axiom (what is now known as the "star-continuity" property) $$a \left(⋁_{n≥0} b^n\right) c = ⋁_{n≥0} \left(a b^n c\right),$$ along with the axiom that the supremum $⋁_{n≥0} a^n$ exist (which is now known as the "star-completeness" property), which then serves as the definition of the operator $a ↦ a^*$, are added this leads to what are called "star-continuous Kleene algebras", or just "R-dioids". The algebraic variety, itself, comprises what is known as an Eilenberg-Moore Category. Similar categories can be defined for types 0 and 2 in the Chomsky Hierarchy, alongside type 3 for "regular" algebras. Type 1 is out of the loop, since its closure under morphisms is type 0, because of erasing morphisms.

The free algebra, with respect to the axioms laid out above, generated by a set $X$ - regardless of its cardinality - has the star-continuity property as an emergent property: it is also the free R-dioid generated by $X$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.