Decidability of MSO Reparameterization over Countable Chains

Résumé technique : Décidabilité de la reparamétrisation MSO sur les chaînes dénombrables

Énoncé du problème
L'article aborde le problème de la simplification des interprétations de logique monadique du second ordre (MSO). Dans une interprétation MSO, les éléments d'une structure cible sont encodés sous forme de tuples d'éléments d'une structure hôte. Une question centrale est de savoir si une interprétation donnée peut être « simplifiée » en réduisant la dimension de ces tuples représentatifs. Plus précisément, l'article examine si une formule MSO $\phi(\bar{x})$, qui définit le domaine d'une interprétation, admet une reparamétrisation en une formule $G(\bar{x}, \bar{y})$ comportant moins de variables d'image $\bar{y}$, tout en préservant le domaine et en satisfaisant une condition d'image réciproque bornée. Les auteurs se concentrent sur la décidabilité de ce problème sur la classe des ordres linéaires étiquetés dénombrables (chaînes).

Méthodologie
L'approche repose sur la méthode de composition pour la logique MSO sur les ordres linéaires, en utilisant le concept de $r$-types (classes d'équivalence de structures basées sur des formules de rang quantificateur $r$). L'arsenal technique central comprend :

1. Pompabilité et types idempotents : Les auteurs établissent un lien entre l'existence d'un nombre arbitrairement grand de réalisations d'une formule et les propriétés des types idempotents. Une paire de types $(\tau_b, \tau_e)$ est définie comme pompable s'il existe un type idempotent $\tau$ tel que $\tau_b + \tau = \tau_b$ et $\tau + \tau_e = \tau_e$. Cette propriété permet le « pompage » d'intervalles dans une chaîne pour générer un nombre arbitrairement grand de tuples satisfaisants.
2. Élimination de variables via la non-pompabilité : L'article démontre que si une séquence de types définissant une formule contient une paire adjacente non pompable, la variable correspondante peut être éliminée. Cette réduction aboutit à une reparamétrisation de dimension inférieure.
3. Bornes inférieures via la pompabilité : Inversement, si toutes les paires adjacentes de types dans la décomposition d'une formule sont pompables, l'article démontre que la dimension ne peut pas être réduite. Cela est montré en construisant des chaînes spécifiques où le nombre de tuples satisfaisants croît polynomialement avec la taille de l'entrée, correspondant à la dimension actuelle.
4. Construction algorithmique : En combinant ces observations, les auteurs construisent un algorithme qui calcule une reparamétrisation minimale. L'algorithme décompose efficacement la formule d'entrée en une disjonction de formes normales (basées sur les types), vérifie les paires pompables, et réduit soit la dimension, soit confirme la minimalité.

Contributions et résultats clés

• Théorème principal (Décidabilité) : Le résultat principal est qu'il est décidable si une formule MSO $\phi(\bar{x})$ donnée sur une classe de chaînes étiquetées dénombrables admet une reparamétrisation de dimension $d$. De plus, si une telle reparamétrisation existe, elle peut être construite efficacement. Cela généralise un résultat précédent de Bojańczyk, qui était limité aux mots finis.
• Équivalence aux interprétations ponctuelles : L'article démontre que si la formule de domaine d'une interprétation admet une reparamétrisation de dimension $d$, l'interprétation entière est équivalente à une interprétation ponctuelle de dimension $d$. Cela fournit une méthode formelle pour réduire des interprétations complexes à des interprétations basées sur des points plus simples.
• Caractérisation du taux de croissance : Les auteurs définissent le taux de croissance d'une interprétation MSO comme la taille maximale de l'ensemble de sortie par rapport à la taille de l'entrée. Ils démontrent que pour les interprétations MSO sur les chaînes dénombrables, le taux de croissance est polynomial. Crucialement, le degré de ce polynôme est exactement égal à la dimension minimale de reparamétrisation de la formule définissante.
• Calculabilité de la dimension minimale : La dimension minimale requise pour une reparamétrisation est montrée comme étant un nombre calculable dérivé de la formule et de la classe de structures.

Portée et importance
L'article étend la compréhension théorique des interprétations MSO des structures finies aux chaînes dénombrables arbitraires. Il établit que la complexité de la simplification des interprétations (réduction de dimension) est décidable dans ce cadre plus large. Le travail clarifie la relation structurelle entre la complexité logique d'une formule (mesurée par les séquences de types et la pompabilité) et la complexité géométrique de l'interprétation (dimension et taux de croissance).

Les auteurs notent que, bien que le résultat principal se concentre sur les interprétations ponctuelles, des résultats de décidabilité connexes pour les interprétations d'ensembles finis et d'ensembles sur les chaînes dénombrables ont été explorés dans un travail complémentaire [7]. L'article mentionne également que des résultats analogues valent lorsque les variables sont interprétées comme des coupes (complétions de Dedekind) plutôt que comme des points, soulignant la robustesse des techniques sous-jacentes. Les résultats sont présentés sous forme d'ébauches de preuves en raison des limitations d'espace, mais le cadre logique est entièrement défini.