Ce document est le résumé en français de l’article
de
Colcombet, Douéneau-Tabot, and Lopez (2023) présenté à la conférence
LICS 2023, dont le pdf, les slides de présentations, ainsi
que le fichier bibtex associé
sont disponibles sur ma page web.
Résumé
Cet article étudie une classe de fonction particulièrement robuste des mots finis vers les entiers relatifs. Ces fonctions, nommées \(\mathbb{Z}\)-polyregulières, admettent de nombreuses caractérisations équivalentes en termes de logique, d’expressions rationelles, d’automates pondérés, et de transducteurs. Après avoir démontré l’équivalence (effective) de ces définitions, nous nous intéressons à deux problèmes de décision. Dans un premier temps, nous montrons que le degré de croissance d’une fonction \(\mathbb{Z}\)-polyrégulière (c’est-à-dire, le plus petit \(k\) tel que \(f(w) = \mathcal{O}(|w|^k)\)) est calculable et correspond précisément au nombre minimal de variables requises pour exprimer la fonction à l’aide de formules \(\mathsf{MSO}\). Dans un second temps, nous montrons que la définissabilité au premier ordre des fonctions \(\mathbb{Z}\)-polyrégulières est décidable. Ce résultat est obtenu grâce à l’introduction d’une notion nouvelle de transducteur résiduel, ainsi que d’une présentation sémantique de la notion d’apériodicité dans le cas des fonctions.
Contextualisation
Les automates déterministes reconnaissent des langages réguliers. Ces mêmes langages peuvent se caractériser par une présentation syntaxique (les expressions régulières de Kleene et al. 1956), une présentation logique (basée sur \(\mathsf{MSO}\), voir Büchi 1960), ainsi qu’une présentation algébrique (sur la base des monoïdes finis Marcel Paul Schützenberger 1961). Au sein des langages réguliers, une classe particulièrement intéressante possède, elle aussi une présentation multiple : celle des langages sans étoile. Ces langages se décrivent aussi bien en terme d’automates (les automates sans compteurs de McNaughton and Papert 1971), d’expressions régulières (les expressions sans étoile M. P. Schützenberger 1965), de logique (la logique au premier ordre \(\mathsf{FO}\), voir Perrin and Pin 1986), et d’algèbre (les monoïdes finis apériodiques M. P. Schützenberger 1965).
De l’équivalence des présentations des langages sans étoile découle la décidabilité du problème suivant : étant donné un langage régulier \(L\), décider s’il est sans étoile. En effet, décider si un monoïde est apériodique est relativement simple, tout comme décider si un automate est sans compteurs. Cependant, la décision repose aussi sur l’existence d’automates (ou de monoïdes) canoniques associées aux langages (respectivement l’automate minimal et le monoïde syntaxique), sans quoi les algorithmes susmentionnés ne permettent pas de conclure.
Les langages réguliers sont un cas particulier de fonctions des mots vers les entiers (relatifs) où les valeurs de la fonction sont prises dans le sous ensemble \(\mathord{\{ 0,1 \}}\). De nombreux travaux ont entrepris de généraliser la notion de régularité à des fonctions mot-à-mot, c’est-à-dire, à des fonctions \(f \colon \Sigma^* \to \Gamma^*\), en lieu et place des fonctions \(\mathop{\mathbf{1}_{L}} \colon \Sigma^* \to \mathord{\{ 0,1 \}}\). Ces tentatives ont mené à une myriade de classes de fonctions non équivalentes (comme les fonctions séquentielles, rationnelles, régulières, polyrégulières, etc.). Les problèmes de décision associés à ces classes, et en particulier le problème de l’apériodicité, deviennent beaucoup plus difficiles à appréhender dans le cadre fonctionnel (voir Scott 1967). Un obstacle conceptuel majeur provient de l’absence d’objet canonique (similaire à l’automate minimal d’un langage) associé à la fonction dans de nombreux modèles. Ainsi, il n’est pas surprenant que la récente démonstration de la décidabilité de l’apériodicité pour les fonctions rationnelles repose sur la construction d’un tel “objet canonique” sur lequel l’apériodicité est clairement visible (Filiot, Gauwin, and Lhote 2016; Filiot et al. 2018).
Contributions de l’article
Cet article (ré-)introduit une classe de fonctions des mots vers les entiers relatifs qui généralise les langages réguliers tout en conservant leurs propriétés de décidabilité ainsi que les différentes caractérisations de ceux-ci. Dans un premier temps, nous montrons l’équivalence (effective) des différentes présentations en termes de logique, d’expressions, d’automates pondérés, ainsi que de transducteurs.
Par la suite, nous proposons un algorithme de minimisation du nombre de variables nécessaires pour exprimer une fonction \(\mathbb{Z}\)-polyrégulière \(f\). Cela met en évidence l’égalité entre le nombre minimal de variables nécessaires et le degré de croissance de la fonction \(f\) (qui est donc calculable). Ce résultat est très simple à obtenir pour des fonctions à valeur dans \(\mathbb{N}\) (où il était déjà connu), mais plus subtil à obtenir dans le cadre des fonctions à valeur dans \(\mathbb{Z}\), à cause des compensations possibles entre termes négatifs et termes positifs. La décidabilité du degré de croissance permet ensuite l’élaboration d’un objet canonique associé à une fonction \(\mathbb{Z}\)-polyrégulière : le transducteur des résiduels. Sa définition utilise la possibilité de soustraire des fonctions \(\mathbb{Z}\)-polyrégulières, ce qui était jusque-là un handicap dans les preuves. Sa construction est effective grâce à la décidabilité du degré de croissance.
À partir de cet objet canonique, on peut alors décider si une fonction \(\mathbb{Z}\)-polyrégulière \(f\) est définissable au premier ordre (i.e., est sans étoile ou apériodique). Nous montrons que la définissabilité au premier ordre coïncide bien avec la notion d’apériodicité dans le cas des langages, et que les caractérisations alternatives se généralises aux fonctions \(\mathbb{Z}\)-polyrégulières : le transducteur des résiduels est sans compteur, les valeurs propres associées à la présentation algébrique sont \(0\) ou \(1\), la fonction s’écrit avec une expression sans étoile. De plus, nous introduisons une caractérisation sémantique originale qui généralise la notion d’apériodicité dans les monoïdes au cas des fonctions à valeur dans \(\mathbb{Z}\) en termes de polynômes. Les résultats de cette seconde partie de l’article reposent crucialement sur l’étude préalable des fonctions \(\mathbb{Z}\)-polyrégulières faite dans la première partie de l’article.
Conclusion
Cet article décrit une classe extrêmement robuste de fonctions généralisant les langages réguliers, qui admet de multiples caractérisations, et dont les principaux problèmes d’appartenance (degré de croissance, apériodicité) sont décidables et possèdent une procédure effective de conversion. Nous pensons que ces résultats, bien que reposant crucialement sur la possibilité de compenser des erreurs grâce aux sorties négatives (qui peut se concevoir comme une forme limitée de backtracking), peuvent se généraliser (avec des preuves plus combinatoires) au cadre des fonctions à valeur dans \(\mathbb{N}\).
Par ailleurs, la définition de fonctions apériodiques à valeur dans \(\mathbb{Z}\) ne coïncide pas avec les précédentes tentatives de généralisations des langages sans étoile aux séries rationnelles, et semble donner une direction prometteuse pour définir les “séries rationnelles apériodiques”.