Unifying Semantic Path Order and Weighted Path Order

Problem
Monotone Semantische Pfadordnungen (MSPOs) und Gewichtete Pfadordnungen (WPOs) sind etablierte, leistungsfähige Reduktionsordnungen, die zur Beweisführung der Terminierung von Term-Transformationssystemen (TRSs) verwendet werden. Obwohl beide effektiv sind, wurden sie historisch als getrennte Ansätze behandelt. Vorangegangene Arbeiten zeigten, dass WPOs Instanzen von MSPOs sind, doch ein vereinheitlichender Rahmen, der MSPOs als Instanzen einer verallgemeinerten WPO behandelt und dabei die wünschenswerten Eigenschaften beider bewahrt, war nicht vollständig ausgearbeitet. Darüber hinaus kämpfen bestehende Konstruktionen damit, gleichzeitig Ground-Totalität (entscheidend für den Theorembeweis) und effiziente Vergleichsmechanismen über verschiedene algebraische und präzedenzbasierte Einstellungen hinweg zu erreichen.

Methodik
Die Autoren schlagen eine Vereinheitlichung dieser Ordnungen durch die Einführung der Verallgemeinerten Gewichteten Pfadordnung (GWPO) und ihrer monotonen Variante, der Monotonen Verallgemeinerten Gewichteten Pfadordnung (MGWPO), vor.

1. Fundamentale Struktur: Der Kern der vereinheitlichten Ordnung basiert auf Reduktionstrippeln $(\geq, \succeq, \succ)$, die ursprünglich für MSPOs eingeführt wurden. Ein Reduktionstrippel besteht aus einer Umformungspräordnung $\geq$, einem stabilen Ordnungs-Paar $(\succeq, \succ)$, wobei $\succ$ wohlgegründet ist, und einer Harmoniebedingung, die die Präordnung mit dem Ordnungs-Paar verknüpft.
2. Definition der GWPO: Die GWPO ($>_G$) wird unter Verwendung zweier Paare von Relationen, $(\succeq_A, \succ_A)$ und $(\succeq_B, \succ_B)$, definiert. Ein Term $s$ ist größer als $t$, wenn:
   • $s \succ_A t$, oder
   • $s \succeq_A t$ und spezifische rekursive Bedingungen, die Subterme und lexikografische Vergleiche betreffen, gelten, wobei potenziell das zweite Paar $(\succeq_B, \succ_B)$ für weitere Vergleiche genutzt wird.
3. Monotonie: Um sicherzustellen, dass die Ordnung unter Kontexten abgeschlossen ist (eine Anforderung für Reduktionsordnungen), wird die MGWPO ($>_{MG}$) als Schnittmenge $\geq_A \cap \geq_B \cap >_G$ definiert.
4. Reduktionspaare: Der Rahmen wird auf Reduktionspaare $(\geq, >)$ erweitert, die partielle Status ($\pi$) integrieren. Dies ermöglicht eine flexiblere Handhabung von Funktionsargumenten und verallgemeinert den Standard-WPO-Ansatz.
5. Vereinheitlichungslogik:
   • WPO als MGWPO: Eine Standard-WPO wird als MGWPO gezeigt, bei der das Trippel $A$ durch eine schwach einfache Algebra induziert wird und das Trippel $B$ durch eine Präzedenz.
   • MSPO als MGWPO: Eine MSPO wird als MGWPO gezeigt, bei der das Trippel $A$ trivial ist und das Trippel $B$ dem Reduktionstrippel der MSPO entspricht. Umgekehrt beweisen die Autoren, dass jede MGWPO als MSPO dargestellt werden kann, indem eine spezifische lexikografische Kombination der zugrundeliegenden Trippel konstruiert wird.

Hauptbeiträge

• Verallgemeinerung: Die Arbeit führt GWPOs und MGWPOs ein und zeigt, dass sowohl MSPOs als auch WPOs spezifische Instanzen dieses verallgemeinerten Rahmens sind.
• Ground-Totalität: Die Autoren identifizieren, dass WPOs Ground-Totalität (den Vergleich beliebiger zweier verschiedener Ground-Terme) natürlich unterstützen, MSPOs dies jedoch nicht tun. Der MGWPO-Rahmen ermöglicht die Konstruktion von ground-totalen Reduktionsordnungen, die Gleichungen orientieren können (z. B. für Kombinatoren S und K), die mit bestehenden Konstruktionen zuvor schwer zu handhaben waren.
• Optimierung: Die vereinheitlichte Ordnung bietet eine Optimierung für den Vergleich. Wird eine strikte Abnahme über die erste Komponente ($\succ_A$) erkannt, endet der Vergleich sofort ohne rekursive Prüfungen. Dies imitiert die Effizienz der Knuth-Bendix-Ordnung (KBO) eher als die der Lexikografischen Pfadordnung (LPO).
• Komplexitätsverbesserung: Durch die Auferlegung der Subterm-Eigenschaft auf die strikte Ordnung $\succ_A$ leiten die Autoren ein Verfahren ab, um MGWPO-Vergleiche in linearer Zeit relativ zur Größe der Terme (gemessen an der Anzahl der Basisrelationen-Vergleiche) zu entscheiden, was die typische quadratische Zeitkomplexität von LPO-ähnlichen Definitionen verbessert.
• Vereinheitlichung der Reduktionspaare: Die Arbeit erweitert diese Ergebnisse auf Reduktionspaare mit partiellen Status und beweist, dass MGPOs und MSPOs auch in diesem Setting vereinheitlicht werden können, sofern bestimmte Einfachheitsbedingungen erfüllt sind.

Ergebnisse
Die Autoren implementierten einen Prototyp-Terminierungstool basierend auf der Dependency-Pair-Methode unter Verwendung der vorgeschlagenen Reduktionspaare. Die Evaluierung wurde an 1.528 endlichen TRSs aus der Termination Problem Database (TPDB) mit einem Zeitlimit von einer Minute durchgeführt.

• Leistung: Die GWPO-Konfiguration bewies die Terminierung für 591 Systeme, und die SPO-Konfiguration (Semantische Pfadordnung) bewies 595 Systeme, im Vergleich zu 486 für die Standard-WPO.
• Vergleich: Die Konfigurationen lösten unterschiedliche Problemsets. Die SPO-Konfiguration konnte Probleme lösen, bei denen die algebraische Komponente bezüglich des partiellen Status nicht „schwach einfach" war, eine Bedingung, die für die GWPO erforderlich ist.
• State-of-the-Art: Die Autoren stellen fest, dass ihre Methoden zwar mehr Terminierungsinstanzen beweisen als die Standard-WPO, jedes von ihrem Tool gelöste Problem jedoch auch von den State-of-the-Art-Beweisern AProVE oder NaTT gelöst wurde. Folglich beanspruchen die Autoren nicht, neue Probleme gelöst zu haben, die zuvor unlösbar waren, sondern vielmehr die theoretische Vereinheitlichung und spezifische Effizienzgewinne ihres Ansatzes demonstriert zu haben.

Bedeutung
Die Arbeit beansprucht Bedeutung primär in der theoretischen Vereinheitlichung zweier großer Klassen von Reduktionsordnungen. Indem gezeigt wird, dass MSPOs Instanzen von GWPOs sind (und umgekehrt), bietet die Arbeit einen einzigen Rahmen, der wünschenswerte Eigenschaften von beiden erbt:

1. Sie ermöglicht die Konstruktion von ground-totalen Ordnungen, ein entscheidendes Merkmal für Theorembeweismethoden wie den Superpositions-Kalkül, das für MSPOs nicht natürlich verfügbar war.
2. Sie bietet einen Mechanismus zur Optimierung des Vergleichs, indem rekursive Prüfungen vermieden werden, wenn eine strikte Abnahme in der primären algebraischen Komponente gefunden wird, was in spezifischen Settings zu einer linearen Zeitkomplexität führen kann.
3. Sie klärt die Beziehung zwischen algebraischen Interpretationen und präzedenzbasierten Ordnungen und führt diese Verbindungen auf frühere Beobachtungen bezüglich der Knuth-Bendix-Ordnung und Semantischer Pfadordnungen zurück.

Die Arbeit dient als fundamentaler Schritt, der in der Dissertation des ersten Autors weiter detailliert wird, um die Lücke zwischen semantischen und gewichteten Pfadordnungen zu schließen und ein flexibleres und potenziell effizienteres Werkzeugset für die Terminierungsanalyse anzubieten.