Ranked MSO-enumeration over compressed words

Résumé technique : Énumération classée sur les mots compressés par MSO

Énoncé du problème
L'article traite du problème de l'énumération des réponses à une requête de logique du second ordre monadique (MSO) fixée sur une chaîne fournie sous un format compressé. Plus précisément, la chaîne d'entrée $w$ est donnée par un programme à lignes droites (SLP - Straight-Line Program), qui est une grammaire hors contexte générant exactement une chaîne. L'objectif est de calculer tous les tuples $(a_1, \dots, a_k)$ de positions dans $w$ satisfaisant une formule MSO fixée $\Phi(x_1, \dots, x_k)$.

Une contrainte critique de ce travail est l'énumération classée (ranked enumeration). Contrairement aux algorithmes d'énumération standards où l'ordre de sortie est opaque, l'énumération classée exige que les tuples de sortie soient imprimés dans un ordre spécifique, défini par l'utilisateur, lequel est lui-même définissable en MSO (par exemple, l'ordre lexicographique sur les tuples de positions). La métrique d'efficacité pour de tels algorithmes est un temps de prétraitement linéaire (linéaire par rapport à la taille du SLP, $|G|$) suivi d'un délai constant (une borne constante sur le temps entre l'affichage de deux tuples consécutifs).

Avant ce travail, l'énumération classée pour les requêtes MSO était connue pour les chaînes et les arbres non compressés, mais aucun résultat n'existait pour les données compressées. De plus, les résultats d'énumération existants pour les chaînes compressées (par exemple, [29]) n'atteignaient qu'un délai linéaire par rapport à la sortie et ne permettaient pas l'énumération classée.

Méthodologie
La solution combine trois composantes techniques primaires :

1. Arbres de factorisation et SLP de Simon :
   L'outil structurel central est l'arbre de factorisation, un arbre d'analyse syntaxique pour un mot par rapport à un morphisme dans un monoïde fini, où les nœuds ayant $\ge 3$ enfants évaluent le même élément idempotent. Le théorème de Simon garantit que de tels arbres ont une hauteur bornée par une constante dépendant de la taille du monoïde.
   Le papier introduit le concept de SLP de Simon (SSLP) : un SLP qui est structurellement compatible avec un arbre de factorisation du mot généré. Les auteurs prouvent (Théorème 3.1) que tout SLP donné peut être transformé en un SSLP équivalent en temps linéaire. Cette transformation implique la construction d'un transcuteur non déterministe qui génère des arbres de factorisation et ensuite la restructuration de la grammaire pour refléter la hiérarchie de l'arbre, garantissant que la « profondeur contractée par l'idempotent » du SLP est bornée par une constante ($3|M|$).

2. Parcours en temps constant dans les chaînes compressées :
   Pour naviguer efficacement dans la chaîne compressée, le papier utilise et étend les techniques de [26] pour un parcours bidirectionnel en temps constant. Les auteurs définissent des chemins compressés (séquences de triplets représentant des mouvements gauche/droite dans le DAG du SLP) et maintiennent une structure de données dynamique (un arbre binaire $B$) qui stocke un nombre constant de chemins « actifs ».
   De manière cruciale, ils définissent les procédures right et left qui, étant donné un chemin dans la représentation compressée, calculent son successeur ou son prédécesseur lexicographique en temps constant. Cela implique de diviser les arêtes dans l'arbre de parcours et de gérer les sous-chemins « contractés par l'idempotent » au sein de parties spécifiques du SLP (les parties-$e$).

3. Interprétation MSO et calcul du successeur :
   L'algorithme d'énumération est formulé comme le calcul de l'image d'une fonction polyrégulière (ou plus généralement, d'une interprétation de type chaîne-vers-chaîne MSO). L'algorithme calcule de manière itérative le « successeur » d'un tuple de positions actuel selon l'ordre linéaire définissable en MSO.
   La preuve implique de transformer les formules MSO en automates à états finis non déterministes (NFA) et de dériver un monoïde fini $M$. En précalculant les éléments du monoïde pour les nœuds de l'arbre de factorisation (ou l'équivalent SSLP), l'algorithme peut déterminer la position suivante dans la séquence d'énumération en temps constant. Il gère la transition entre les positions en analysant les éléments du monoïde des segments situés entre les positions actuelles et en utilisant la structure de l'arbre de factorisation pour naviguer vers la position valide suivante sans décompresser la chaîne.

Contributions clés et résultats

• Théorème principal (Théorème 5.1) : Pour une formule MSO fixée avec $k$ variables de premier ordre libres et un ordre linéaire sur les $k$-tuples définissable en MSO, l'ensemble des réponses aux requêtes sur une chaîne compressée par SLP peut être énuméré avec un temps de prétraitement linéaire ($O(|G|)$) et un délai constant. C'est le premier résultat de ce type pour l'énumération classée sur des données compressées.
• Corollaire pour les fonctions polyrégulières (Corollaire 5.3) : Le résultat se généralise aux fonctions chaîne-vers-chaîne polyrégulières. Pour une fonction polyrégulière $f$ fixée et un SLP $G$ produisant $w$, les symboles de $f(w)$ peuvent être énumérés de gauche à droite avec un prétraitement linéaire et un délai constant. Cela étend un résultat précédent de Bojanczyk [8] (qui supposait une entrée non compressée) au cadre compressé, bien que les fonctions polyrégulières ne préservent généralement pas la taille de la compression.
• Corollaire pour le Successor-MSO (Corollaire 5.5) : Le résultat s'applique à la classe plus large des interprétations chaîne-vers-chaîne de type successor-MSO, qui sont strictement plus larges que les fonctions polyrégulières.
• Contribution technique (SLP de Simon) : Le papier établit que tout SLP peut être converti en un SLP de Simon en temps linéaire. Cela rend les arbres de factorisation accessibles au cadre des grammaires compressées, une contribution notée comme étant d'intérêt indépendant.

Signification et affirmations
Le papier affirme faire le « premier pas » dans la direction de l'énumération classée sur des données compressées. Il traite un écart spécifique où les algorithmes d'énumération compressée précédents (par exemple, [29]) ne pouvaient pas contrôler l'ordre de sortie, et où les algorithmes d'énumération classée précédents (par exemple, [2, 12, 19]) ne pouvaient pas gérer des entrées compressées.

Les auteurs soulignent que leur approche repose sur la structure spécifique des arbres de factorisation et sur la capacité à effectuer une navigation en temps constant sur les SLP. Ils notent explicitement les limites :

• Les résultats actuels ne s'appliquent qu'aux requêtes avec des variables de premier ordre libres ; la gestion des variables d'ensemble libres (qui nécessiterait un délai linéaire par rapport à la sortie plutôt qu'un délai constant) est un problème ouvert, car l'approche de l'arbre de factorisation ne s'étend pas actuellement aux variables d'ensemble.
• Le travail est actuellement restreint aux chaînes ; l'extension des résultats aux forêts (en utilisant des programmes à lignes droites pour forêts) est identifiée comme un travail futur, en attente de la combinaison des théorèmes de factorisation de forêts avec les techniques de parcours de SLP pour forêts.
• Le classement est restreint aux ordres linéaires définissables en MSO ; la relation entre ce modèle et le classement basé sur le poids (utilisant des transducteurs de coût) reste incertaine.

En résumé, le papier fournit un fondement théorique pour le traitement efficace et ordonné des requêtes sur des données hautement compressées, démontant que le « standard d'excellence » de la prétraitement linéaire et du délai constant est réalisable pour les requêtes MSO sur les SLP, à condition que l'ordre de sortie soit définissable en MSO.