💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

Dieses im Entstehen begriffene Paper führt einen automatischen Pattern-Matching-Taktik für Autosubst ein, der dessen aktuelle Einschränkungen bei der Handhabung von Typisierungsregeln, Reduktionsrelationen und nicht-eindeutigen Lösungen adressiert, wie durch Evaluierungen an den POPLMark- und POPLMark Reloaded-Challenges demonstriert wird.

Ursprüngliche Autoren: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

Veröffentlicht 2026-07-15

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, ein riesiges, magisches Puzzle zu lösen, bei dem jedes Teil ein verstecktes Etikett besitzt. In der Welt der Informatik werden diese Etiketten De-Bruijn-Indizes genannt. Sie sind eine clevere Art, Variablen im Code zu verfolgen, aber sie sind berüchtigt schwierig. Man kann sie sich wie ein Spiel mit Stühlen vorstellen, bei dem die Stühle (Variablen) jedes Mal die Namen wechseln, wenn sich jemand darauf setzt. Wenn man versucht, ein Puzzleteil (eine Regel) mit einer Lücke (einem Ziel) in diesem Spiel abzugleichen, sehen die Teile oft unterschiedlich aus, obwohl sie eigentlich dieselben sind, nur tragen sie unterschiedliche Hüte.

Lange Zeit war ein Werkzeug namens Autosubst der Held dieser Geschichte. Es ist wie ein superintelligenter Roboter, der sofort sagen kann, ob zwei Puzzleteile identisch sind, selbst wenn ihre Etiketten durcheinandergewürfelt wurden. Dies geschieht durch den Einsatz eines Satzes magischer Regeln (des $\sigma$ -Kalküls), die die Teile normalisieren, bis sie identisch aussehen. Wenn man lediglich prüfen möchte, ob zwei Dinge gleich sind, ist dieser Roboter perfekt.

Das Problem: Die „Apply“-Falle
Es gibt jedoch einen Haken. Wenn man versucht, diese Puzzleteile zu nutzen, um ein Problem zu lösen, indem man eine Regel anwendet (wie das Drücken eines „Apply“-Buttons in einem Videospiel), bleibt der Roboter stecken. Er ist großartig darin zu sagen: „Ja, diese sind gleich“, aber er ist schrecklich darin zu sagen: „Hier ist die Art und Weise, wie du diese Regel in diese spezifische Lücke einpasst.“

Warum? Weil eine Regel auf verschiedene Arten in eine Lücke passen kann, und der Roboter nicht weiß, welche der „richtigen“ Weg ist, ohne Hilfe. In der Vergangenheit mussten menschliche Programmierer die schwere Arbeit leisten. Sie mussten ihre Regeln auf seltsame, indirekte Weise umschreiben oder die fehlenden Etiketten manuell erraten, nur damit der Roboter funktionierte. Es war, als würde man versuchen, einen quadratischen Klotz in ein rundes Loch zu pressen, indem man den Klotz selbst abschleift, anstatt einfach das richtige Werkzeug zu finden.

Die neue Idee: Eine kluge Ratestrategie
Dieses Paper stellt ein neues Werkzeug namens as_apply vor. Denken Sie an einen neuen, etwas abenteuerlustigeren Roboterarm, der darauf ausgelegt ist, diese Puzzleteile zu greifen und sie in die Löcher zu schieben, selbst wenn die Etiketten auf den ersten Blick nicht perfekt überebereinstimmen.

Anstatt aufzugeben oder den Menschen zu bitten, alles neu zu schreiben, nutzt dieser neue Taktik einen Satz von Heuristiken (das sind im Grunde gebildete Vermutungen basierend auf Mustern, die es zuvor gesehen hat). Er betrachtet die Lücke, betrachtet die Regel und sagt: „Ich wette, wenn ich diese Etiketten nur ein kleines Stück verschiebe, werden sie passen!“

Wie es funktioniert (Der Zaubertrick)
Der Prozess läuft in zwei Schritten ab:

Vorbereitung: Der Roboter bereitet die Puzzleteile zuerst mit den alten, zuverlässigen Autosubst-Regeln auf, um sie so ordentlich wie möglich zu machen.
Das Ratespiel: Er versucht dann, die Teile abzugleichen. Wenn die Teile nicht perfekt übereinstimmen, gerät er nicht in Panik. Stattdessen probiert er einige spezifische Tricks aus:
- Er prüft, ob die Unstimmigkeit nur ein einfacher „Shift“ ist (wie das Verschieben einer Variable um eine Position nach oben).
- Er prüft, ob das fehlende Teil nur eine „Identität“ ist (nichts tun).
- Er sucht nach häufig vorkommenden Mustern, die normalerweise in diesen Puzzles auftreten.

Wenn eine dieser Vermutungen funktioniert, füllt er die fehlenden Etiketten auf und macht weiter. Wenn sie fehlschlägt, geht er zurück (Backtracking) und versucht eine andere Vermutung.

Was das Paper sagt (und was nicht)
Die Autoren sind sehr vorsichtig darauf bedacht, nicht zu viel zu versprechen. Sie geben zu, dass dies kein Zauberstab ist, der jedes mögliche Puzzle löst.

Es ist nicht perfekt: Das Paper stellt explizit fest, dass ein Puzzle manchmal mehrere Lösungen haben kann und dieser Roboter vielleicht die falsche wählt. Es ist möglich, ein kniffliges Beispiel zu konstruieren, bei dem der Roboter falsch rät, selbst wenn eine richtige Antwort existiert.
Es ist ein „Work-in-Progress“: Die Autoren beschreiben dies als eine Methode im Prozess der Weiterentwicklung („work-in-progress“). Sie behaupten nicht, die gesamte Theorie des Abgleichs für immer gelöst zu haben.
Die Ergebnisse: Sie haben diese neue Taktik bei zwei berühmten, schwierigen Herausforderungen namens POPLMark und POPLMark Reloaded getestet. Dies sind quasi die „Olympischen Spiele“ beim Beweisen von Programmiersprachen.
- In der POPLMark-Herausforderung (642 Zeilen Code) haben sie die neue Taktik 15 Mal angewendet.
- In der POPLMark Reloaded-Herausforderung (683 Zeilen Code) haben sie sie 10 Mal angewendet.
- In all diesen Fällen hat die Taktik das Ziel erfolgreich gelöst.

Das Urteil
Das Paper legt nahe, dass diese neue Taktik, obwohl sie theoretische Grenzen hat (sie könnte durch sehr seltsame, adversarielle Puzzles verwirrt werden), in der realen Welt überraschend gut funktioniert. Sie ermöglicht es Programmierern, aufzuhören, ihre Regeln auf seltsame, indirekte Weise umzuschreiben, und sie stattdessen natürlich zu schreiben.

Die Autoren sind hoffnungsvoll, aber vorsichtig. Sie deuten an, dass dieser Ansatz in vielen praktischen Fällen die alte, klobige Art ersetzen könnte, aber sie wissen auch, dass noch Arbeit zu leisten ist, um sicherzustellen, dass der Roboter niemals, jemals die falsche Lösung wählt. Sie arbeiten derzeit daran, genau herauszufinden, welche Arten von Puzzles dieser Roboter mit 100 %iger Sicherheit lösen kann und welche möglicherweise immer noch eine menschliche Überprüfung erfordern.

Kurz gesagt: Es ist ein cleveres, hilfreiches neues Werkzeug, das die unordentliche Aufgabe des Abgleichs von Puzzleteilen viel einfacher macht, auch wenn es noch nicht ganz bereit ist, das einzige Werkzeug im Kasten zu sein.

Technische Zusammenfassung: Eine Taktik für das Pattern Matching in Autosubst

Problemstellung
Das Paper adressiert eine spezifische Einschränkung im Autosubst-Framework, einem Code-Generator für den Rocq-Proof-Assistant (ehemals Coq), der das Schließen über de-Bruijn-Terme und Substitutionen mittels des $\sigma$ -Kalküls automatisiert. Während Autosubst die Gleichheitsprüfung für Annahmefreie Ziele mittels der asimpl-Taktik erfolgreich automatisiert, scheitert es, wenn Benutzer versuchen, Annahmen (z. B. Typisierungsregeln oder Lemmata) auf ein Ziel mittels Standard-Taktiken wie apply oder `eapply anzuwenden.

In diesen Szenarien muss der Benutzer ein Ziel modulo $\sigma$ -Äquivalenz mit einer Annahme vereinheitlichen (unify). Die Automatisierung von Autosubst ist jedoch nicht darauf ausgelegt, gegen Annahmen zu matchen. Infolgedessen sind Benutzer gezwungen, umständliche Workarounds zu verwenden, wie zum Beispiel:

Die Formulierung von Regeln in indirekten Formen (unter Verwendung frischer Meta-Variablen anstelle direkter Substitutions-Terme).
Die Einführung Hilfslemmata, um die Lücke zwischen dem Ziel und der Annahme zu schließen.
Das manuelle Transformieren von Zielen oder das explizite Instanziieren existentieller Variablen während der Beweise.

Die Kernschwierigkeit besteht darin, dass das $\sigma$ -Matching (Matching modulo $\sigma$ -Äquivalenz) nicht eindeutig ist; ein einzelnes Matching-Problem kann mehrere Lösungen zulassen, von denen nicht alle die Prämissen des Kontextes erfüllen. Zudem ist das Second-Order-Matching für den vollständigen $\lambda\sigma$ -Kalkül unentscheidbar, und selbst ohne $\beta$ -Reduktion sind die Lösungen nicht notwendigerweise eindeutig.

Methodik
Die Autoren schlagen eine als „Work-in-Progress“ bezeichnete heuristische Taktik namens as_apply vor, die in der Ltac-Sprache von Rocq implementiert ist, um das Pattern Matching modulo $\sigma$ -Äquivalenz zu automatisieren. Die Taktik operiert in zwei primären Phasen:

Preprocessing (Vorverarbeitung):
- Sowohl das Ziel als auch die Konklusion der Zielannahme werden unter Verwendung der bestehenden asimpl-Taktik im Hinblick auf den $\sigma$ -Kalkül normalisiert.
- Quantifizierte Variablen in der Annahme werden durch existentielle Variablen (evars) ersetzt.
- Die Prämissen der Annahme werden in Subziele umgewandelt, die nach der Matching-Phase gelöst werden sollen.
- Die Taktik handhabt die Konvertierung zwischen expliziten Umbenennungsoperationen (z. B. $s\langle\xi\rangle$ ) und Instanziationsoperationen ( $s[\xi]$ ) mittels substify und renamify.
Matching-Phase:
- Die Taktik konstruiert eine Menge von Matching-Gleichungen $M = \{s_i =_\sigma t_i\}$ zwischen den Ziel-Termen und den instanziierten Annahme-Termen.
- Sie verarbeitet Gleichungen von links nach rechts unter Verwendung eines partiellen Verfahrens, $\sigma_{min}$ , welches versucht, modulo des $\sigma_{min}$ -Fragments (einer Teilmenge der $\sigma$ -Regeln, die Instanziierung und Kompositionalität charakterisiert) zu matchen.
- Heuristiken: Falls $\sigma_{min}$ $σ_{min}$ kein Match findet, wendet die Taktik einen Satz von Heuristiken an, die gängige Muster in formalen Entwicklungen erfassen. Dazu gehören:
  - Die Handhabung von Gleichungen der Form $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ durch Instanziierung der Unbekannten mit einer gehobenen (lifted) Substitution ( $?s \mapsto s[\Uparrow\sigma]$ ).
  - Die Handhabung von Fällen, die Identitäts-Substitutionen oder spezifische Variablenstrukturen beinhalten.
- Nach Anwendung der Substitutionen wird die Annahme erneut normalisiert. Der Erfolg ist gegeben, wenn das Ziel und die Annahme syntaktisch identisch werden.

Die Taktik wurde generalisiert, um die vollständige Eingabesprache des Autosubst-Compilers zu unterstützen, einschließlich multipler mutuell induktiver Sorten, Vektor-Substitutionen und First-Class-Umbenennungen.

Wesentliche Beiträge

Einführung von as_apply: Eine heuristische Taktik, die darauf ausgelegt ist, apply/eapply in Autosubst-basierten Entwicklungen zu ersetzen, indem sie das Matching modulo $\sigma$ -Äquivalenz in Gegenwart von Annahmen ermöglicht.
Generalisierung: Erweiterung der Matching-Logik auf die gesamte von Autosubst unterstützte Syntax, einschließlich komplexer Binder und Umbenennungsoperationen.
Empirische Evaluierung: Anwendung der Taktik auf Standard-Benchmarks, spezifisch die POPLMark und POPLMark Reloaded Challenges.

Ergebnisse
Die Autoren evaluierten as_apply auf den POPLMark (642 Zeilen) und POPLMark Reloaded (683 Zeilen) Challenge-Lösungen.

Häufigkeit der Verwendung: Die Taktik wurde 15 Mal in der POPLMark B Lösung und 10 Mal in der POPLMark Reloaded Lösung verwendet.
Effektivität: In allen getesteten Fällen löste as_apply die intendierten Ziele erfolgreich.
Vereinfachung: Der Einsatz der Taktik eliminierte die Notwendigkeit für indirekte Regelformulierungen, Hilfslemmata und manuelle Zieltransformationen, die die bisherigen Lösungen charakterisierten.
Limitierungen: Die Autoren räumen ein, dass as_apply nicht $\sigma$ -vollständig und kein Entscheider ist. Da $\sigma$ -Matching mehrere Lösungen haben kann, bedeutet der heuristische Charakter der Taktik, dass sie theoretisch eine falsche Lösung wählen könnte, wenn eine korrekte existiert, obwohl keine solchen Fehler in den Fallstudien beobachtet wurden.

Bedeutung und Ansprüche
Das Paper behauptet, dass während das theoretische Problem des $\sigma$ -Matchings inhärent schwierig ist (nicht-eindeutige Lösungen, Unentscheidbarkeit im vollen $\lambda\sigma$ ), ein pragmatischer, heuristischer Ansatz in der Praxis ein hohes Maß an Automatisierung wiederherstellen kann. Die Bedeutung liegt in der Reduzierung der manuellen Last für Benutzer, die mit de-Bruijn-Syntax arbeiten, wodurch sie Typisierungsregeln und Lemmata in ihren direkten, natürlichen Formen angeben können, anstatt in indirekten Formen, die auf die Limitationen der Unifikation-Engine des Proof-Assistants zugeschnitten sind.

Die Autoren bleiben bescheiden hinsichtlich des aktuellen Zustands der Arbeit und bezeichnen sie als „Work-in-Progress“. Sie merken an, dass die aktuelle Taktik aufgrund des Potenzials für unendliche oder multiple Lösungen auf Heuristiken angewiesen ist. Zukünftige Arbeiten zielen darauf ab, das größte Fragment $\sigma'$ , für das ein Eindeutigkeitskriterium gilt, zu identifizieren, was potenziell zu einer Matching-Taktik mit bewiesenen Garantien führen könnte.

Mehr davon