Towards an HRS Category in TermCOMP

Technische Zusammenfassung: Auf ein HRS-Kategorie in TermCOMP zugehen

Problemstellung
Die jährliche Termination Competition (TermCOMP) umfasst eine Kategorie für höherwertiges Umschreiben (higher-order rewriting). Historisch gesehen hat diese Kategorie die Semantik von Algebraischen Funktionellen Systemen (AFSs) genutzt, die auf einfachem Matching und expliziten $\beta$-Reduktionsregeln basieren. Während Nipkows Higher-Order Rewrite Systems (HRSs), die modulo $\beta\eta$ umschreiben und typischerweise Millers Muster (PRSs) oder die neueren Deterministischen Higher-Order Pattern Rewrite Systeme (DPRSs) verwenden, etablierte Formalismen sind, wurden sie bisher nicht vollständig in das Wettbewerbsframework von TermCOMP integriert. Die Herausforderung liegt darin, die Semantik von HRSs (Umschreiben modulo $\beta\eta$) mit dem bestehenden TermCOMP-Framework (basierend auf AFSs und Meta-Substitutionen) in Einklang zu bringen, um Werkzeuge, die auf HRSs abzielen, direkt gegen solche zu lassen, die auf AFSs abzielen.

Methodik
Die Autoren schlagen eine formale Brücke zwischen HRSs und der aktuellen TermCOMP-Semantik für höherwertiges Umschreiben, definiert als Simply-Typed Meta-Substitution Rewrite Systems (STMRSs). Die Methodik umfasst drei Hauptschritte:

1. Generalisierung von Mustern: Die Autoren führen Extended Pattern Rewrite Systems (EPRSs) ein, eine Unterklasse von HRSs, die sowohl PRSs als auch DPRSs generalisiert. EPRSs verwenden „Extended Patterns“ (EPATs), welche die deterministischen Matching-Beschränkungen von DPRSs lockern, aber eine Struktur beibehalten, bei der freie Variablen auf Nicht-Abstraktions-Argumente angewendet werden. Diese Klasse wird primär definiert, um die theoretische Beweisführung zu erleichschen, und nicht als eigenständiges praktisches Werkzeug.
2. Erweiterung der STMRS-Semantik: Die Autoren erweitieren die Definition von STMRS-Regeln (der aktuellen TermCOMP-Standard), um zu erlauben, dass linke Seiten EPATs anstelle von Standardmustern sind. Sie führen das Konzept von „well-behaved“ (gutartig) und „quasi-well-behaved“ (quasi-gutartig) Termen ein. Diese syntaktischen Beschränkungen stellen sicher, dass die resultierenden Terme, wenn Meta-Substitutionen angewendet werden, in $\beta$-Normalform bleiben (speziell in $\beta\eta$-langer Normalform), ohne neue $\beta$-Redexe zu erzeugen, die zusätzliche Reduktionsschritte erfordern würden.
3. Implementierung via normalisierter Reduktion: Der zentrale technische Beitrag besteht darin, festzustellen, dass das Umschreiben in einem well-behaved STMRS, gefolgt von $\beta$-Normalisierung, das Umschreiben in dem entsprechenden EPRS simuliert. Die Autoren definieren eine Translation zwischen gewöhnlichen Substitutionen (verwendet in EPRSs) und Meta-Substitutionen (verwendet in STMRSs), um zu beweisen, dass die beiden Systeme hinsichtlich der Terminierung äquivalent sind.

Wesentliche Beiträge

• Definition von EPRSs: Eine neue syntaktische Unterklasse von HRSs, die DPRSs generalisiert und so eine breitere Palette von Benchmarks ermöglicht, während handhabbare Matching-Eigenschaften erhalten bleiben.
• Syntaktische Beschränkungen für Äquivalenz: Die Einführung von „well-behaved“ STMRS-Regeln. Diese beschränken linke Seiten auf „well-behaved“ und rechte Seiten auf „quasi-well-behaved“. Dies stellt sicher, dass die Anwendung von Meta-Substitutionen keine $\beta$-Redexe erzeugt und somit die $\beta$-Normalform der Terme bewahrt.
• Formaler Äquivalenzbeweis: Das Papier beweist, dass für ein well-behaved STMRS $R$ und einen Term $s$ in $\beta\eta$-langer Normalform ein Rewrite-Schritt in der EPRS-Semantik ($s \to_R t$) genau dann stattfindt, wenn ein Rewrite-Schritt in der STMRS-Semantik gefolgt von $\beta$-Normalisierung erfolgt ($s \Rightarrow_R \cdot \Rightarrow!_\beta t$).

Ergebnisse
Das primäre Ergebnis ist Theorem 15, welches die Korrespondenz zwischen den Rewrite-Relationen von well-behaved STMRSs und ihren entsprechenden EPRSs etabliert. Speziell gilt:

• $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ genau dann, wenn $s \to_R t$ (wobei $R$ als EPRS betrachtet wird).
• Dies führt zu Korollar 20, welches besagt, dass die Terminierung der Strategie „umschreiben und dann $\beta$-normalisieren“ in einem well-behaved STMRS mit der universellen Terminierung des entsprechenden EPRS übereinstimmt.

Die Autoren zeigen, dass diese Äquivalenz für Terme in $\beta\eta$-langer Normalform gilt. Sie merken an, dass für zweiter Ordnung liegende STMRSs die Korrespondenz noch stärker ist, da Meta-Substitutionen in diesem spezifischen Kontext keine $\beta$-Redexe erzeugen können.

Bedeutung
Das Papier beansprucht, das formale Fundament für eine HRS-(Unter-)Kategorie in TermCOMP zu legen. Durch die Definition einer syntaktisch prüfbaren Teilmenge von Benchmarks (well-behaved STMRSs) innerhalb des bestehenden TPDB-Formats ermöglichen die Autoren:

1. Direkten Wettbewerb: Werkzeuge, die für HRSs entwickelt wurden (unter Verwendung von $\beta\eta$-Rewriting), können nun direkt gegen Werkzeuge antreten, die für AFSs entwickelt wurden, da ihre Terminierungseigenschaften unter den vorgeschlagenen Semantiken als identisch bewiesen sind.
2. Breitere Werkzeugunterstützung: Das Implementierungsergebnis ermöglicht den Vergleich von Eigenschaften über die bloße Terminierung hinaus, da die Simulation auf einer schrittweisen Korrespondenz und nicht nur auf einer globalen Terminierungseigenschaft basiert.
3. Verfeinerung bestehender Arbeit: Das Ergebnis stärkt frühere Implementierungen von PRSs in AFSMs (Kop) und kombinatorischen Systemen (van Oostrom und van Raamsdonk), indem es diese auf eine allgemeinere Klasse von HRSs (EPRSs) erweitert und einen rigorosen Beweis für die Äquivalenz von normalisiertem Umschreiben und höherwertigem Umschreiben liefert.

Die Autoren bleiben hinsichtlich des Umfangs bescheiden und räumen ein, dass das Ergebnis nicht alle HRSs abdeckt, da Meta-Substitution streng weniger mächtig ist als die volle höherwertige Substitution. Sie argumentieren jedoch, dass die definierte Unterklasse ausreicht, um einen signifikanten Teil der existierenden Benchmarks sowie die spezifischen DPRSs aus ihrer vorangegangenen Arbeit aufzunehmen.