Edit Distance of Finite-Valued Transducers

Résumé technique : Distance d'édition des transducteurs à valeurs finies

Énoncé du problème
L'article aborde la décidabilité de la distance d'édition entre deux transducteurs à états finis. Alors que la distance d'édition entre des transducteurs fonctionnels (où chaque entrée correspond à au plus une sortie) est connue pour être calculable, le problème est généralement indécidable pour des transducteurs arbitraires. Les auteurs examinent si cette calculabilité s'étend à la classe des transducteurs à valeurs finies, où chaque mot d'entrée correspond à au plus $k$ mots de sortie pour une constante fixe $k$. Cette classe est strictement plus expressive que les transducteurs fonctionnels, mais conserve la décidabilité pour de nombreux problèmes fondamentaux (par exemple, l'inclusion et l'équivalence) qui sont indécidables dans le cas général.

Méthodologie
La solution proposée procède par une stratégie de réduction qui transforme le problème du calcul de la distance entre des transducteurs à valeurs finies en une série de sous-problèmes calculables impliquant des transducteurs séquentiels et un concept métrique nouvellement introduit.

1. Réduction aux transducteurs multi-séquentiels :
   Les auteurs exploitent le résultat connu selon lequel tout transducteur à valeurs finies peut être décomposé efficacement en une union finie de transducteurs non ambigus (et donc fonctionnels). Ils construisent un automate produit qui synchronise les exécutions de tous les transducteurs composants de deux transducteurs à valeurs finies donnés, $T$ et $S$. Cette construction donne deux transducteurs multi-séquentiels, $T'$ et $S'$ (unions finies de transducteurs séquentiels/déterministes), tels que la distance d'édition $d(T, S)$ est préservée et égale à $d(T', S')$.

2. Introduction de la distance relative :
   Pour calculer la distance entre des relations multi-séquentielles (qui sont des unions de fonctions séquentielles), les auteurs introduisent le concept de distance relative. La distance relative d'une fonction $f$ vers une relation $R$, notée $\vec{d}(f, R)$, est définie comme le supremum sur toutes les entrées $u$ de la distance d'édition minimale entre $f(u)$ et un certain $v \in R(u)$.
   La distance entre deux relations multi-séquentielles $R = \bigcup f_i$ et $S = \bigcup g_j$ est montrée comme étant le maximum des distances relatives entre chaque fonction composante et la relation opposée :
   $$d(R, S) = \max \left( \max_i \vec{d}(f_i, S), \max_j \vec{d}(g_j, R) \right)$$

3. Décidabilité de la distance relative :
   La calculabilité de la distance relative $\vec{d}(f, R)$ est établie en la réduisant à deux problèmes de bornitude :

   • Finitude : Décider si $\vec{d}(f, R) < \infty$.

   • $k$-Finitude : Décider si $\vec{d}(f, R) \leq k$ pour un entier donné $k$.

   • Vérification de finitude : Les auteurs construisent un transducteur produit $T$ représentant les exécutions synchrones de $f$ et des composants de $R$. Ils partitionnent le domaine de $f$ en fonction des composants de $R$ qui acceptent l'entrée. Pour chaque partition, ils analysent les composantes fortement connexes (CFC) du transducteur produit. En utilisant les propriétés de la conjugaison des mots (spécifiquement, qu'une distance d'édition bornée infinie implique la conjugaison des sorties de boucle), ils prouvent que la distance relative est finie si et seulement si, pour chaque chemin de CFC dans le produit, il existe au moins une relation composante dont la sortie de boucle est conjuguée à la sortie de boucle de la fonction. Cela réduit le problème à la vérification de la finitude de la distance entre transducteurs séquentiels, ce qui est décidable.

   • Vérification de $k$-finitude : Pour décider si la distance est bornée par $k$, les auteurs construisent un automate fini non déterministe (AFN), $A_{C,k}$, qui suit le budget d'édition et les suffixes non appariés « résiduels » entre la sortie de la fonction et les sorties de la relation. La distance relative est $\leq k$ si et seulement si le langage accepté par $A_{C,k}$ est identique au domaine du transducteur produit.

Contributions et résultats clés

• Théorème principal : La distance d'édition entre deux relations rationnelles à valeurs finies est calculable pour les métriques de la famille de Levenshtein (Levenshtein, plus longue sous-séquence commune et Damerau-Levenshtein).
• Cadre algorithmique : L'article fournit une procédure constructive pour calculer cette distance en réduisant le cas à valeurs finies au cas multi-séquentiel, puis à la distance relative entre une fonction séquentielle et une relation multi-séquentielle.
• Analyse de complexité : Les auteurs notent que leur procédure aboutit à une borne supérieure de 3-EXPSPACE. Cela découle de l'espace exponentiel requis pour convertir les transducteurs à valeurs finies en transducteurs multi-séquentiels, suivi des exigences d'espace exponentiel et doublement exponentiel pour les calculs subséquents de distance relative. La borne inférieure est d'au moins PSPACE-dur, car elle englobe le problème d'équivalence pour les automates non déterministes.

Portée et affirmations
L'article affirme étendre la décidabilité connue de la distance d'édition au-delà des transducteurs fonctionnels vers la classe plus large des transducteurs à valeurs finies. Cela est significatif car les transducteurs à valeurs finies établissent un équilibre entre puissance expressive et faisabilité algorithmique, capturant de nombreux scénarios pratiques où une seule entrée peut produire un petit ensemble borné de sorties valides (par exemple, en traitement du langage naturel ou en synthèse de programmes).

Les auteurs soulignent que leur travail fournit une fondation pour le raisonnement approximatif dans les systèmes réactifs. Dans la vérification classique, un système est vérifié pour une conformité exacte à une spécification. Le concept de distance relative permet de raisonner sur des systèmes qui sont « proches » d'une spécification, accommodant de légères déviations. L'article ne prétend pas optimiser l'algorithme pour l'efficacité, reconnaissant la complexité élevée, mais affirme que le résultat établit la possibilité théorique de calculer ces distances dans une classe de transducteurs expressive et motivée par la pratique. Les techniques sont également notées comme adaptables à d'autres métriques d'édition, telles que la distance de Hamming, avec des modifications mineures.