This paper presents a new result in the equational theory of regular languages, which emerged from lively discussions between the authors about Stone and Priestley duality. Let us call
lattice of languages
a class of regular languages closed under finite intersection and finite union. The main results of this paper (Theorems 5.2 and 6.1) can be summarized in a nutshell as follows:
A set of regular languages is a lattice of languages if and only if it can be defined by a set of profinite equations.
The product on profinite words is the dual of the residuation operations on regular languages.
In their more general form, our equations are of the form
are profinite words. The first result not only subsumes Eilenberg-Reiterman’s theory of varieties and their subsequent extensions, but it shows for instance that any class of regular languages defined by a fragment of logic closed under conjunctions and disjunctions (first order, monadic second order, temporal, etc.) admits an equational description. In particular, the celebrated McNaughton-Schützenberger characterisation of first order definable languages by the aperiodicity condition
, far from being an isolated statement, now appears as an elegant instance of a very general result.