Some Results on Equational Axiomatization of Kleene Algebras
by
Igor Dolinka
University of Novi Sad
Coauthors: Sinisa Crvenkovic (University of Novi Sad)

SOME RESULTS ON THE EQUATIONAL AXIOMATIZATION OF KLEENE ALGEBRAS

Sinisa Crvenkovi\'c and Igor Dolinka
Institute of Mathematics, University of Novi Sad
Trg Dositeja Obradovi\'ca 4, 21000 Novi Sad, Yugoslavia

We define a Kleene algebra to be a structure (A, +, ·, ^*, 0, 1) satisfying all equations of language structures (P(\Sigma^*), +, ·, ^*, 0, 1) equipped with the operations of set union +, concatenation or complex product ·, Kleene star or submonoid generation ^*, and constants 0 (empty set) and 1 (the set containing the empty word \lambda). We will also consider `multiplicative Kleene algebras' which are the structures (A, ·, ^*, 0, 1) satisfying all equations of Kleene algebras not involving the + operation, and commutative Kleene algebras, i.e. Kleene algebras satisfying the equations that hold in the structures (P(\Sigma^\oplus), +, ·, ^*, 0, 1), where \Sigma^\oplus denotes the free commutative monoid on \Sigma. Clearly, the classes of Kleene algebras, multiplicative Kleene algebras and commutative Kleene algebras, respectively, are varieties.

The close connection of Kleene algebras and automata theory relies upon the fact that the free Kleene algebras coincide with the algebras of regular languages, i.e., languages accepted by finite automata (see [, ]). The other important role of Kleene algebras in theoretical computer science is that they serve as a part of dynamic algebras [], one of the main tools of modeling the work of computers in algebra and logic. In such a setting, the elements of a Kleene algebra denote the software, that is, the computer program modules.

Therefore, the equational theory of Kleene algebras is in an obvious correspondence with pairs of regular expressions (Kleene algebra terms) denoting the same regular language. The structure of this equational theory has been studied since the 1960's. In 1964, Redko [, ] proved that neither the equational theory of Kleene algebras, nor the equational theory of commutative Kleene algebras is finitely based, see also [, ]. He also provided a nontrivial equational basis for commutative Kleene algebras. However, the problem (posed by Conway []) of finding a nontrivial, albeit infinite equational basis has been open for a long time. In 1991, Krob [] confirmed Conway's conjecture by proving that an equational basis for Kleene algebras consists of a finite set of so-called `classical equations' and an equation associated with each finite (simple) group. A related equational axiomatization is given in []. There are varieties (in fact, finite algebras) that do not possess an independent basis for their equations, see []. It is not known whether the variety of Kleene algebras is such.

Our first result gives a refinement of Redko's nonfinite axiomatizability result. We prove that for any finite set E of Kleene algebra equations there exist prime numbers p, q and a finite model A such that all of the equations E hold in A, but the equation

(xp)*(xq)* = (xq)*(xp)*

does not. Thus we obtain that there is no finite set of Kleene algebra equations that proves all equations in one variable which hold in Kleene algebras and do not contain the + operation []. An obvious corollary is that the variety of multiplicative Kleene algebras is not finitely based. The latter assertion settles a problem of D. A. Bredikhin posed in 1993. It is an open problem whether the above results are valid for commutative multiplicative Kleene algebras.

Our second result, stating that an equation holds in commutative Kleene algebras if and only if it holds in the Kleene algebra of (regular) languages over the one-letter alphabet [], might be helpful towards solving the above problem. Hence, the variety of commutative Kleene algebras is generated by the Kleene algebra of one-letter (regular) languages. This result answers the Problem III.5.1 in [], and together with the fact that the class of commutative Kleene algebras has no finite axiomatization, it implies that the Kleene algebra of one-letter regular languages is not finitely based, hence giving an answer to another old problem proposed by A. Salomaa in [] (which has recently been solved by a direct argument in []). The proof of the above result is based on the fact that the Kleene algebra of all (regular) languages over an alphabet can be embedded into a direct power of the Kleene algebra of (regular) languages over the one-letter alphabet.

Besides languages, other models of Kleene algebras include Kleene relation algebras (Rel_A, +, ·, ^*, 0, 1) of binary relations on a set A [, ], where + is modeled by set union, · is the composition of relations, ^* is the formation of the reflexive-transitive closure, and where 0 is the empty relation and 1 the identity relation on A. In fact, it is known that the variety of Kleene algebras is also generated by the Kleene relation algebras, so that an equation holds in all Kleene relation algebras iff it holds in all Kleene algebras. One may attempt to extend the type of Kleene algebras (i.e. to enlarge the set of operations on binary relations under consideration) in order to eventually obtain a class of relation algebras generating a finitely based variety. (Relate results and investigations along this line can be found e.g. in [].) For example, a natural and frequently used operation is the conversion (or reversal). Nevertheless, the described problem is still open, since we have that the variety generated by all Kleene relation algebras with conversion of relations also has no finite axiomatization []. The proof of this theorem heavily employs the main result of [] which gives a finite relative axiomatization of Kleene algebras with conversion over the variety of Kleene algebras. Thus it is necessary to look for more (natural) operations on binary relations (or languages) to be involved.

References

Date received: July 12, 1999