The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

Technisches Resümee: Die Computability Path Order für die $\beta\eta$-Normal höhere-Ordnung-Umschreibung

Problemstellung
Höhere-Ordnung-Umschreibung umfasst verschiedene Formalismen, insbesondere die „einfache“ höhere-Ordnung-Umschreibung (unter Verwendung von syntaktischem Matching und der Behandlung der $\beta$-Reduktion als Umschreibregel) sowie die „normale“ höhere-Ordnung-Umschreibung (unter Verwendung von Matching modulo $\beta\eta$ und der Betrachtung von Termen in ihren $\beta\eta$-Normalformen). Während für die einfache Umschreibung leistungsfähige Terminierungsmethoden existieren, wie etwa die Computability Path Order (CPO), stellt die Anpassung dieser an die $\beta\eta$-normale höhere-Ordnung-Umschreibung (speziell Höhere-Ordnung-Umschriebsysteme bzw. HRSs nach Nipkow) erhebliche Herausforderungen dar.

Bestehende Methoden für HRSs, wie die Normal Higher-Order Recursive Path Order (NHORPO), stützen sich oft auf eine Transformationstechnik namens „Neutralisierung“, um Systeme zu handhaben, in denen der Kern-Order versagt. Neutralisierung erschwert jedoch die Automatisierung. Zudem haben Standard-Pfadordnungen Schwierigkeiten mit normaler Umschreibung, da wohldefinierte Ordnungen, die kompatibel mit $\beta\eta$ sind, im traditionellen Sinne im Allgemeinen nicht monoton (unter Kontexten abgeschlossen) oder stabil (unter Substitutionen abgeschlossen) sind. Beispielsweise kann eine Ordnung, die kompatibel mit $\beta\eta$ und unter Kontexten abgeschlossen ist, zu Widersprüchen wie $c > c$ führen, was die Wohldefiniertheit verletzt.

Methodik
Die Autoren schlagen vor, die Computability Path Order (CPO), die ursprünglich für die einfache höhere-Ordnung-Umschreibung definiert wurde, auf den Bereich der $\beta\eta$-normalen höheren-Ordnung-Umschreibung anzuheben. Der resultierende Ordnung wird die $\beta\eta$-normale Computability Path Order (NCPO) bezeichnet.

Die Methodik stützt sich auf die folgenden Kernkomponenten:

1. Reduktionsordnung-Paar: In Anlehnung an den Ansatz von Jouannaud und Rubio definieren die Autoren eine Reduktionsordnung als ein Paar $(>, \sqsupset)$, wobei $>$ die primäre Ordnung (NCPO) ist und $\sqsupset$ eine „einfache“ Variante (CPO) darstellt. Das Paar erfüllt die $\beta\eta$-normale Stabilität: Wenn $s > t$, dann gilt $s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$ für alle Substitutionen $\sigma$, wobei $\downarrow$ die $\beta\eta$-Normalisierung bezeichnet. Dies ermöglicht den Nachweis der Terminierung durch die Wohldefiniertheit und Monotonie der einfachen CPO-Komponente.
2. Nicht-vielseitige Terme (Nonversatile Terms): Eine entscheidende technische Innovation ist die Beschränkung der Anwendung der Ordnung auf nicht-vielseitige Terme. Ein Term ist nicht-vielseitig, wenn Substitution und anschließende $\beta\eta$-Normalisierung nur dessen echte Teilterme beeinflussen. Die Autoren liefern eine verbesserte hinreichende Bedingung für Nicht-Versatilität (Lemma 1) im Vergleich zu vorangegangener Arbeit, was für den Nachweis der Stabilität der Ordnung essenziell ist.
3. Erweiterungen von CPO: NCPO beinhaltet zwei wesentliche Erweiterungen der ursprünglichen CPO:
   • Zugängliche Teilterme (Accessible Subterms): Diese ermöglichen es rekursiven Vergleichen, in spezifischen Fällen, die durch Typpositionen bestimmt werden (positive/negative Basistyp-Positionen), strikte Typabnahmen zu umgehen.
   • Kleine Symbole (Small Symbols): Diese Funktion erlaubt es, bestimmte Funktionssymbole als „klein“ zu behandeln, was die Terminierungsnachweise für Systeme ermöglicht, in denen Standard-rekursive Pfadordnungen versagen (z. B. Listenverarbeitungsfunktionen).
4. Regelsatz: Die Ordnung wird induktiv über einen Satz von Regeln (Abbildung 1) definiert, die Funktionssymbole (groß und klein), Applikationen und Abstraktionen behandeln. Bemerkenswert ist, dass die Regeln zur Orientierung von $\beta$- und $\eta$-Reduktionen entfernt wurden, da die Ordnung direkt auf Normalformen operiert. Eine neue Regel, $\langle \lambda\triangleright\eta \rangle$, wird eingeführt, um spezifische Fälle zu handhaben, die $\eta$-Expansion im Kontext zugänglicher Teilterme beinhalten.

Wesentliche Beiträge

• Definition von NCPO: Das Paper definiert formal die NCPO, die erste Computability Path Order, die speziell für die $\beta\eta$-normale höhere-Ordnung-Umschreibung entwickelt wurde und zugängliche Teilterme sowie kleine Symbole integriert.
• Korrektheitsbeweis: Die Autoren beweisen, dass das Paar $(>_\tau, \sqsupset_\tau)$ eine gültige $\beta\eta$-normale höhere-Ordnung-Reduktionsordnung darstellt (Theorem 2), wodurch die Terminierung für jedes mit ihr kompatible HRS garantiert wird.
• Verbesserte Bedingung für Nicht-Versatilität: Das Paper bietet eine verfeinerte hinreichende Bedingung für Nicht-Versatilität, die stärker ist als die in der grundlegenden Arbeit zu NHORPO bereitgestellte.
• Automatisierung via SAT/SMT: Die Autoren argumentieren, dass NCPO besser automatisierbar ist als NHORPO mit Neutralisierung. Während Neutralisierung eine komplexe syntaktische Analyse transformierter Terme erfordert, die von symbolischen Parametern abhängen (was die SMT-Kodierung schwierig macht), können NCPO-Parameter (Präzedenz, Typordnungen, Status) direkter kodiert werden.

Ergebnisse
Die Autoren implementierten einen Prototyp von NCPO in Haskell unter Verwendung des Hasmtlib-Pakets, um Terminierungsprobleme in das SMT-LIB 2-Format zu kodieren und sie mit dem Z3-Solver zu lösen. Die experimentellen Ergebnisse (Tabelle 1) vergleichen NCPO mit NHORPO (mit und ohne Neutralisierung) sowie mit HORPO-Implementierungen in WANDA und CSI$^{ho}$.

• Überlegenheit gegenüber NHORPO: NCPO beweist erfolgreich die Terminierung mehrerer Systeme, bei denen NHORPO (selbst mit Neutralisierung) scheitert. Speziell:
  • Beispiel 8 (Listen-Inkrementierung): NCPO beweist die Terminierung unter Verwendung kleiner Symbole, eine Funktion, die in NHORPO fehlt.
  • Beispiel 7 (Negationsnormalformen): NCPO beweist die Terminierung mittels zugänglicher Teilterme, während NHORPO mit Neutralisierung scheitert, die Regeln zu orientieren, da es nicht in der Lage ist, vielseitige Terme im Vergleich zu handhaben.
• Unvergleichbare Leistungsfähigkeit: Die Studie identifiziert Fälle (z. B. neutr.p), in denen NHORPO mit Neutralisierung erfolgreich ist, aber NCPO versagt, was zeigt, dass die beiden Ansätze eine unvergleichbare Leistungsfähigkeit besitzen.
• Effizienz: Die Suche nach Parametern für NCPO erweist sich als rechnerisch effizient und benötigt oft eine vergleichbare Zeit wie NHORPO-Suchen, während die Suche nach Neutralisierungsparametern in ihrer Komplexität explodieren kann.

Bedeutung und Behauptungen
Das Paper behauptet, dass NCPO eine mächtige und leichtgewichtige Alternative zur Kombination aus NHORPO und Neutralisierung bietet. Die Autoren betonen, dass NCPO eine praktikablere Wahl für die automatische Terminierungsbeweisung in der normalen höheren-Ordnung-Umschreibung ist, da die Komplexität der Automatisierung der Neutralisierungstechnik hoch ist, obwohl NHORPO mit Neutralisierung ein starker Konkurrent bleibt.

Die Autoren merken bescheiden an, dass die Transitivität von NCPO weiterhin eine offene Frage bleibt, da die Einbeziehung der $\beta$-Reduktion in den zugrunde liegenden einfachen Order die Nicht-Transitivität für CPO und NHORPO rechtfertigt, aber die spezifischen Eigenschaften von NCPO weitere Untersuchungen erfordern. Zusätzlich schlagen sie vor, dass die Integration von NCPO in Dependency-Pair-Techniken für die normale höhere-Ordnung-Umschreibung ein logischer nächster Schritt ist. Das Paper schließt mit dem Hinweis auf die Notwendigkeit, höhere-Ordnung-Terminierungsmethoden zu formalisieren, um Fehler in der bisherigen Literatur zu vermeiden, wie etwa falsche Behauptungen bezüglich der Lösbarkeit bestimmter Beispiele durch NHORPO.