Edit Distance of Finite-Valued Transducers

Technische Zusammenfassung: Edit-Distanz endlich-wertiger Transduktoren

Problemstellung
Der Artikel behandelt die Berechenbarkeit der Edit-Distanz zwischen zwei endlichen Transduktoren. Während die Edit-Distanz zwischen funktionalen Transduktoren (bei denen jedes Eingabewort höchstens ein Ausgabewort erzeugt) als berechenbar bekannt ist, ist das Problem für beliebige Transduktoren im Allgemeinen unentscheidbar. Die Autoren untersuchen, ob sich diese Berechenbarkeit auf die Klasse der endlich-wertigen Transduktoren erstreckt, bei denen jedes Eingabewort höchstens $k$ Ausgabewörter für eine feste Konstante $k$ erzeugt. Diese Klasse ist strikt ausdrucksstärker als funktionale Transduktoren, behält jedoch die Entscheidbarkeit für viele fundamentale Probleme (z. B. Inklusion und Äquivalenz) bei, die im allgemeinen Fall unentscheidbar sind.

Methodik
Der vorgeschlagene Lösungsansatz folgt einer Reduktionsstrategie, die das Problem der Berechnung der Distanz zwischen endlich-wertigen Transduktoren in eine Reihe berechenbarer Teilprobleme transformiert, die sequentielle Transduktoren und ein neu eingeführtes metrisches Konzept betreffen.

1. Reduktion auf multi-sequentielle Transduktoren:
   Die Autoren nutzen das bekannte Ergebnis, dass jeder endlich-wertige Transduktor effektiv in eine endliche Vereinigung unambiguer (und somit funktionaler) Transduktoren zerlegt werden kann. Sie konstruieren einen Produktautomaten, der die Läufte aller Komponententransduktoren zweier gegebener endlich-wertiger Transduktoren $T$ und $S$ synchronisiert. Diese Konstruktion liefert zwei multi-sequentielle Transduktoren $T'$ und $S'$ (endliche Vereinigungen sequentieller/deterministischer Transduktoren), sodass die Edit-Distanz $d(T, S)$ erhalten bleibt und gleich $d(T', S')$ ist.

2. Einführung der relativen Distanz:
   Um die Distanz zwischen multi-sequentiellen Relationen (die Vereinigungen sequentieller Funktionen sind) zu berechnen, führen die Autoren das Konzept der relativen Distanz ein. Die relative Distanz von einer Funktion $f$ zu einer Relation $R$, bezeichnet als $\vec{d}(f, R)$, ist definiert als das Supremum über alle Eingaben $u$ der minimalen Edit-Distanz zwischen $f(u)$ und einem beliebigen $v \in R(u)$.
   Die Distanz zwischen zwei multi-sequentiellen Relationen $R = \bigcup f_i$ und $S = \bigcup g_j$ wird als Maximum der relativen Distanzen zwischen jeder Komponentenfunktion und der gegenüberliegenden Relation gezeigt:
   $$d(R, S) = \max \left( \max_i \vec{d}(f_i, S), \max_j \vec{d}(g_j, R) \right)$$

3. Entscheidbarkeit der relativen Distanz:
   Die Berechenbarkeit der relativen Distanz $\vec{d}(f, R)$ wird durch ihre Reduktion auf zwei Beschränktheitsprobleme etabliert:

   • Endlichkeit: Entscheidung, ob $\vec{d}(f, R) < \infty$.

   • $k$-Endlichkeit: Entscheidung, ob $\vec{d}(f, R) \leq k$ für eine gegebene ganze Zahl $k$.

   • Endlichkeitsprüfung: Die Autoren konstruieren einen Produkttransduktor $T$, der die synchronen Läufte von $f$ und den Komponenten von $R$ darstellt. Sie partitionieren den Definitionsbereich von $f$ basierend darauf, welche Komponenten von $R$ die Eingabe akzeptieren. Für jede Partition analysieren sie die stark zusammenhängenden Komponenten (SCCs) des Produkttransduktors. Unter Verwendung von Eigenschaften der Wortkonjugiertheit (speziell, dass eine unendliche beschränkte Edit-Distanz die Konjugiertheit der Schleifenausgaben impliziert), beweisen sie, dass die relative Distanz genau dann endlich ist, wenn für jeden Pfad von SCCs im Produkt mindestens eine Komponentenrelation existiert, deren Ausgabeschleife zur Ausgabeschleife der Funktion konjugiert ist. Dies reduziert das Problem auf die Prüfung der Endlichkeit der Distanz zwischen sequentiellen Transduktoren, was entscheidbar ist.

   • $k$-Endlichkeitsprüfung: Um zu entscheiden, ob die Distanz durch $k$ beschränkt ist, konstruieren die Autoren einen nichtdeterministischen endlichen Automaten (NFA) $A_{C,k}$, der das Edit-Budget und die „übrig gebliebenen" ungematchten Suffixe zwischen dem Ausgabe der Funktion und den Ausgaben der Relation verfolgt. Die relative Distanz ist genau dann $\leq k$, wenn die von $A_{C,k}$ akzeptierte Sprache identisch mit dem Definitionsbereich des Produkttransduktors ist.

Hauptbeiträge und Ergebnisse

• Hauptsatz: Die Edit-Distanz zwischen zwei endlich-wertigen rationalen Relationen ist für Metriken der Levenshtein-Familie (Levenshtein, längste gemeinsame Teilsequenz und Damerau-Levenshtein) berechenbar.
• Algorithmischer Rahmen: Der Artikel liefert ein konstruktives Verfahren zur Berechnung dieser Distanz durch Reduktion des endlich-wertigen Falls auf den multi-sequentiellen Fall und anschließend auf die relative Distanz zwischen einer sequentiellen Funktion und einer multi-sequentiellen Relation.
• Komplexitätsanalyse: Die Autoren stellen fest, dass ihr Verfahren eine obere Schranke von 3-EXPSPACE ergibt. Dies ergibt sich aus dem exponentiellen Speicherbedarf zur Umwandlung endlich-wertiger Transduktoren in multi-sequentielle, gefolgt von exponentiellem und doppelt exponentiellem Speicherbedarf für die nachfolgenden Berechnungen der relativen Distanz. Die untere Schranke liegt mindestens bei PSPACE-schwer, da sie das Äquivalenzproblem für nichtdeterministische Automaten umfasst.

Bedeutung und Behauptungen
Der Artikel behauptet, die bekannte Entscheidbarkeit der Edit-Distanz über funktionale Transduktoren hinaus auf die breitere Klasse der endlich-wertigen Transduktoren zu erweitern. Dies ist bedeutend, da endlich-wertige Transduktoren eine Balance zwischen Ausdruckskraft und algorithmischer Handhabbarkeit schlagen und viele praktische Szenarien erfassen, in denen eine einzelne Eingabe eine kleine, beschränkte Menge gültiger Ausgaben erzeugen kann (z. B. in der natürlichen Sprachverarbeitung oder bei der Programmsynthese).

Die Autoren betonen, dass ihre Arbeit eine Grundlage für approximatives Schließen in reaktiven Systemen liefert. In der klassischen Verifikation wird ein System auf exakte Konformität mit einer Spezifikation geprüft. Das Konzept der relativen Distanz ermöglicht das Schließen über Systeme, die einer Spezifikation „nahekommen", und berücksichtigt geringe Abweichungen. Der Artikel behauptet nicht, den Algorithmus hinsichtlich der Effizienz zu optimieren, und räumt die hohe Komplexität ein, behauptet jedoch, dass das Ergebnis die theoretische Möglichkeit der Berechnung dieser Distanzen in einer praktisch motivierten, ausdrucksstarken Klasse von Transduktoren feststellt. Die Techniken werden zudem als mit geringfügigen Modifikationen auf andere Edit-Metriken, wie die Hamming-Distanz, anpassbar beschrieben.