The equational theory of regular words (Q1776401)

Regular words, introduced by \textit{B. Courcelle} [``Frontiers of infinite trees'', RAIRO, Inf. Théor. 12, 319--337 (1978; Zbl 0411.68065)], are (finite or infinite) words isomorphic to the frontier of regular binary trees with lexicographic ordering of the leaves. Regular words can be generated [see \textit{S. Heilbrunner}, ``An algorithm for the solution of fixed-point equations for infinite words'', RAIRO, Inf. Théor. 14, 131--141 (1980; Zbl 0433.68062)] from singletons by applying the operations of concatenation, omega power, omega-op power, and shuffles. Following previous work of their own [``Axiomatizing omega and omega-op powers of words'', Theor. Inform. Appl. 38, 3--17 (2004; Zbl 1082.68070)], the authors prove that the algebra of nonempty regular words on an alphabet \(A\), equipped with these operations, is freely generated by \(A\) in a variety which is completely axiomatized by an infinite collection of certain natural equations, and show that the equational theory of that variety is decidable in P-time and is not finitely based, thus solving open problems stated by Courcelle over 20 years ago.