On a question of A. Salomaa: The equational theory of regular expressions over a singleton alphabet is not finitely based

Salomaa (1969, p. 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative answer to this long-standing question. The proof of our main result rests upon a model-theoretic argument. For every finite collection of equations, that are sound in the algebra of regular expressions over a singleton alphabet, we build a model in which some valid regular equation fails. The construction of the model mimics the one used by Conway (1971, p. 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions. Our analysis of the model, however, needs to be more refined than the one provided by Conway (1971).