Résumé : Cet article présente un nouveau
résultat sur la théorie équationnelle des langages
rationnels, obtenu à la suite de discussions animées entre
les auteurs sur les dualités de Stone et de Priestley. Appelons
treillis de langages une classe de langages rationnels fermée
par intersection finie et union finie. Les résultats principaux de
cet article peuvent être résumés ainsi:
Un ensemble de langages rationnels est un treillis de langages si et
seulement si il peut être défini par un ensemble
d'équations profinies.
Le produit des mots profinis est le dual de l'opération de
résiduation sur les langages rationnels.
Dans leur forme la plus générale, nos équations sont
de la forme u --> v, où u et v sont des mots profinis. Le premier
résultat généralise la théorie
d'Eilenberg-Reiterman et ses extensions successives à un cadre
beaucoup plus général et montre par exemple qu'une classe de
langages rationnels définie par un fragment de logique (du premier
ordre, du second ordre monadique, temporelle, etc.) fermée par
conjonctions et disjonctions admet une description équationnelle.
Abstract :
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
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 u
--> v, where u and v 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.