🔢 mathematics

Categorical E-Graphs for Lambda Calculi

Dieses Paper erweitert den kategorialen Rahmen von E-Graphen auf kartesische symmetrische monoidale Kategorien, um die Variablenbindung im $\lambda$ -Kalkül nativ zu unterstützen, indem es eine hierarchische Hypergraphen-Repräsentation mit einem Double-Pushout-Umschreibmechanismus einführt, der als äquivalent zum Standard-Termumschreiben bewiesen wird.

Ursprüngliche Autoren: Aleksei Tiurin, Dan R. Ghica, Nick Hu

Veröffentlicht 2026-06-26

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Aleksei Tiurin, Dan R. Ghica, Nick Hu

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 Puzzle zu lösen, aber jedes Mal, wenn Sie ein Teil bewegen, zerstören Sie versehentlich die Teile, die Sie bereits platziert haben. Dies ist das Problem, mit dem Informatiker konfrontiert sind, wenn sie komplexe Computerprogramme optimieren wollen. Sie verwenden ein Werkzeug namens e-Graph (Equality Graph), das wie ein super-effizienter Aktenschrank funktioniert. Anstatt alte Versionen eines Programms wegzuwerfen, wenn sie eine bessere finden, bewahrt der e-Graph alle Versionen im selben Schrank auf und gruppiert dabei die Teile, die dasselbe bedeuten. Dies ermöglicht es dem Computer, Millionen von Möglichkeiten gleichzeitig zu erforschen, ohne den Überblick zu verlieren.

Es gibt jedoch einen Haken: e-Graphen hatten historisch gesehen Schwierigkeiten mit Variablen (wie dem „x“ in mathematischen Gleichungen). In einem Programm ist eine Variable wie ein Namensschild, das man hin und her bewegen kann. Wenn man das Namensschild bewegt, kann sich die Bedeutung des Programms ändern, oder zwei identische Programme könnten unterschiedlich aussehen, nur weil die Namensschilder an unterschiedlichen Stellen platziert sind. Das macht es sehr schwierig für den e-Graph zu erkennen, dass sie tatsächlich dieselben sind.

Die große Idee: Von Text zu Bildern

Die Autoren dieses Papers schlagen einen neuen Weg vor, um mit diesen Variablen-Namensschildern umzugehen. Anstatt Programme als Text zu behandeln (wie einen Satz, den man liest), behandeln sie sie als String-Diagramme (wie eine Karte oder ein Flussdiagramm).

Der alte Weg (Text): Stellen Sie sich vor, Sie schreiben ein Rezept. Wenn Sie in Schritt 1 „Salz hinzufügen“ schreiben und in Schritt 5 ebenfalls „Salz hinzufügen“, sieht der Computer zwei separate Sätze. Selbst wenn sie dasselbe bedeuten, muss der Computer zusätzliche Arbeit leisten, um zu erkennen, dass sie identisch sind.
Der neue Weg (String-Diagramme): Stellen Sie sich das Rezept als ein physisches Flussdiagramm vor, bei dem Drähte Zutaten mit Aktionen verbinden. Wenn Sie zwei „Salz hinzufügen“-Schritte haben, sind dies buchstäblich derselbe physische Draht, der mit zwei verschiedenen Stellen verbunden ist. Sie müssen den Text nicht vergleichen; das Bild zeigt, dass sie dieselben sind.

Die „Magic Box“-Lösung

Um dies für Variablen (die „gebunden“ oder innerhalb eines bestimmten Teils des Programms festgeschrieben sein können, wie eine lokale Variable in einer Funktion) zum Laufen zu bringen, nutzen die Autoren ein Konzept aus der fortgeschrittenen Mathematik namens Kategorientheorie.

Betrachten Sie ein Programm als eine Maschine mit Eingängen und Ausgängen.

Die Box: Sie stellen eine Funktion (wie eine Lambda-Abstraktion, λx) als eine abgerundete Box dar. Die Variable x ist ein Draht, der in die Box führt.
Das Sharing: Sie verwenden gestrichelte Boxen, um Gruppen von Dingen darzustellen, die äquivalent sind. Wenn zwei Teile des Programms mathematisch gleich sind, befinden sie sich innerhalb derselben gestrichelten Box.
Das Ergebnis: Durch die Kombination dieser Boxen erschaffen sie eine Struktur, die ein Closed E-Hypergraph genannt wird. Dies ist ein schicker Name für eine „Puzzle-Karte“, die automatisch weiß, wann zwei Teile identisch sind, selbst wenn sie in unterschiedlichen Boxen eingepackt sind oder unterschiedliche Variablennamen haben.

Wie es funktioniert: Der „Rewiring“-Trick

In traditionellen e-Graphen müssen Sie, um ein Programm zu ändern, ein altes Stück löschen und ein neues einfügen. Das ist riskant und langsam.

Die Änderung eines Programms ist in diesem neuen System wie das Neuverkabeln einer Leiterplatte.

Stellen Sie sich eine „Beta-Reduktion“ (eine grundlegende Regel in der Programmierung, bei der man einen Wert in eine Funktion einsetzt) nicht als das Löschen von Text vor, sondern als das einfache Ausstecken eines Drahtes aus einer Buchse und das Einstecken in eine andere.
Da die Struktur auf diesen Diagrammen basiert, muss sich der Computer keine Sorgen um das Umbenennen von Variablen oder darum machen, ob diese „gekapert“ (von einem falschen Scope übernommen) wurden. Die Drähte fließen ganz natürlich.

Warum das wichtig ist (laut dem Paper)

Die Autoren haben diese Idee unter Verwendung einer spezifischen Art von Programmlogik getestet, dem linearen Substitutionskalkül (eine Methode zum Umgang mit „let“-Anweisungen und Sharing in Code).

Das Problem mit dem alten Weg: Um „let“-Anweisungen (wie let x = 1 in...) zu handhaben, mussten alte e-Graphen spezielle „bürokratische“ Knoten und Regeln hinzufügen, um die Namen zu verwalten. Dies überladene das System und verlangsamte es.
Der neue Weg: In ihrem Diagrammsystem sind „let“-Anweisungen einfach natürliche Verbindungen. Das System versteht automatisch, dass let x = 1 in (x + x) dasselbe ist wie let y = 1 in (y + y), ohne dass zusätzliche Regeln erforderlich sind. Das „Sharing“ ist in der Geometrie des Diagramms eingebaut.

Das Fazit

Das Paper behauptet, ein neues mathematisches Fundament für e-Graphen geschaffen zu haben, das Programme als topologische Karten statt als Text behandelt. Indem sie „Boxen“ verwenden, um Variablen zu verbergen, und „Drähte“, um sie zu verbinden, haben sie ein System geschaffen, in dem:

Äquivalenz automatisch erfolgt: Wenn zwei Diagramme topologisch gleich aussehen, sind sie dasselbe Programm.
Rewriting sicher ist: Sie können Teile des Programms ändern, ohne den Rest zu zerstören.
Variablen natürlich gehandhabt werden: Keine unordentlichen Umbenennungen oder speziellen „bürokratischen“ Knoten mehr.

Die Autoren argumentieren, dass dieser Ansatz besonders leistungsstark für funktionale Programmiersprachen (wie jene, die auf dem Lambda-Kalkül basieren) ist und eine sauberere, effizientere Methode zur Optimierung von Code bietet als bisherige Methoden, die auf „slotted“ e-graphs (die Variablen als explizite Datenslots behandeln) zurückgriffen. Sie liefern den mathematischen Beweis, dass ihr diagrammbasiertes Rewriting genauso korrekt ist wie das traditionelle textbasierte Rewriting, jedoch mit dem Vorteil, die „Form“ des Programms direkt zu handhaben.

Technisches Resümee: Kategorische E-Graphen für Lambda-Kalküle

Problemstellung

Equality Saturation ist eine leistungsstarke Technik zur Programmoptimierung und zum Schließen von Argumentationen, die Äquivalenzklassen von Termen (E-Graphen) nutzt, um einen Raum von Umschreibungsregeln (Rewrite Rules) zerstörungsfrei zu explorieren. Herkömmliche E-Graphen verfügen jedoch über keine native Unterstützung für Variablenbindung, ein fundamentales Merkmal funktionaler Programmiersprachen, die auf dem $\lambda$ -Kalkül basieren.

Bestehende Ansätze zur Integration von Bindung stehen vor erheblichen Herausforderungen:

Textuelle Repräsentationen: In der standardmäßigen textuellen Syntax sind $\alpha$ -äquivalente Terme distinkt und können nicht geteilt werden. Während De-Bruijn-Indizes die $\alpha$ -Äquivalenz syntaktisch identifizieren, hängen die Indizes vom Variablenumfang (Scope) ab, was das Teilen von Termen verhindert, die sich nur in der Zuweisung der Indizes unterscheiden (z. B. $\lambda f. f((\lambda x. fx)2)$ ).
Explizite Substitution: Das Hinzufügen von Knoten für explizite Substitution (z. B. $t[x/u]$ ), um Bindung zu handhaben, führt zu „Bürokratie“. Dies erfordert zusätzliche Knoten und Umschreibungsregeln, um Permutationen nicht-interagierender Substitutionen (graphische Äquivalenz) zu verwalten, was den Zustandsraum mit administrativem Overhead belastet, statt auf domänenspezifisches Rewriting zu fokussieren.
Slotted E-Graphs: Jüngste Arbeiten (Schneider et al.) führen „slotted e-graphs“ ein, bei denen Variablen als First-Class-Daten behandelt werden. Während dieser Ansatz effektiv ist, stützt er sich auf nominale Techniken, die für beliebige Sprachen (wie den $\pi$ -Kalkül) anwendbar sind, aber möglicherweise nicht die spezifischen strukturellen Eigenschaften des $\lambda$ -Kalküls so effizient nutzen können wie ein dediziertes semantisches Modell.

Das Kernproblem ist das Fehlen einer nativen, kategorischen Datenstruktur für E-Graphen, die Variablenbindung unterstützt und somit eine effiziente Equality Saturation in $\lambda$ -Kalküle ermöglicht, ohne den Overhead durch explizite Substitutionsknoten oder komplexe Umbenennungsregeln.

Methodik

Die Autoren schlagen eine Lösung vor, die auf der kategorialen Semantik basiert und die Interpretation von E-Graphen als String-Diagramme erweitert.

1. Kategorischer Rahmen

Die Arbeit baut auf den Arbeiten von Tiurin et al. auf, die E-Graphen (ohne Bindung) als Morphismen in symmetrischen monoidalen semilattice-angereicherten Kategorien (SLat-Kategorien) modellierten.

SLat-Anreicherung: Die Hom-Mengen sind Semilattices, wobei die Join-Operation ( $+$ ) die Äquivalenz von Teiltermen (E-Graph-Klassen) repräsentiert.
Monoidale geschlossene Struktur: Um Variablenbindung zu handhaben, erweitern die Autoren die Kategorie zu einer monoidal geschlossenen Kategorie. Dies führt das interne Hom-Objekt ( $A \multimap B$ ) und die Adjunktion $- \otimes B \dashv B \multimap -$ ein.
String-Diagramme: Terme werden als String-Diagramme dargestellt. Bindung wird mittels „abgerundeter Boxen“ (repräsentativ für $\lambda$ -Abstraktion) modelliert, und Äquivalenzklassen werden mittels „gestrichelter Boxen“ (repräsentativ für den Semilattice-Join) modelliert.

2. Kombinatorische Repräsentation: Geschlossene E-Hypergraphen

Um eine konkrete Datenstruktur bereitzustellen, definieren die Autoren geschlossene E-Hypergraphen. Dies sind hierarchische Hypergraphen, die folgendes kodieren:

Hyperedges: Repräsentieren Operationen (Generatoren).
Hierarchische Edges: Zwei Arten von geschachtelten Strukturen:
- E-Klassen (Gestrichelte Boxen): Repräsentieren Äquivalenzklassen von Teiltermen.
- Abstraktions-Boxen (Abgerundete Boxen): Repräsentieren $\lambda$ -Abstraktionen.
Interfaces: Die Struktur verwendet erweiterte Cospans, um Eingaben und Ausgaben zu verwalten, wobei zwischen externen Interfaces (Top-Level) und strikt internen Interfaces (geschachtelt innerhalb von Boxen) unterschieden wird.

3. Rewriting-System

Die Autoren definieren ein Double-Pushout mit Interfaces (DPOI) Rewriting-System für geschlossene E-Hypergraphen.

Rewrite-Regeln: Definiert als Spans von erweiterten Cospans.
Boundary Complements: Eine spezialisierte Definition des „Lochs“ (Hole), das nach dem Entfernen eines Matches entsteht, wird eingeführt, um die hierarchische Natur der Graphen zu handhaben. Dies stellt sicher, dass, wenn ein Subgraph entfernt wird, die internen Interfaces korrekt angepasst werden (z. B. aktualisiert das Entfernen eines geschachtelten Terms das strikt interne Interface des Elternknotens).
Korrektheit und Vollständigkeit: Die Arbeit etabliert, dass DPO-Rewriting auf diesen geschlossenen E-Hypergraphen korrekt und vollständig in Bezug auf das Rewriting von geschlossenen $\Sigma^+$ -Termen modulo den Gleichungen der symmetrischen monoidalen SLat-Kategorien und dem Distributivgesetz der geschlossenen Struktur ist.

Kernbeiträge

Kategoriale Erweiterung: Die Konstruktion einer Form von E-Graphen zur Unterstützung von Bindung durch Erweiterung des kategorialen Bereichs von freien symmetrischen monoidalen SLat-Kategorien zu freien geschlossenen symmetrischen monoidalen SLat-Kategorien.
Geschlossene E-Hypergraphen: Die Definition einer konkreten kombinatorischen Repräsentation (geschlossene E-Hypergraphen), die die Gleichungen der symmetrischen monoidalen Struktur und der geschlossenen Struktur (Bindung) natürlich absorbiert.
DPOI Rewriting für Bindung: Die Formulierung eines DPOI-Rewriting-Systems für diese Strukturen, wobei die Korrektheit und Vollständigkeit relativ zum Term-Rewriting in der entsprechenden kategorialen Theorie nachgewiesen wird.
Vergleich mit Slotted E-Graphs: Ein theoretischer Vergleich, der zeigt, dass während Slotted E-Graphen generische Bindung via nominaler Techniken bieten, der kategoriale Ansatz die Bindung in die interne Sprache des Modells einbettet, was potenziell Vorteile für $\lambda$ -Kalkül-spezifische Optimierungen bietet.

Ergebnisse

Äquivalenz des Rewritings: Die Arbeit beweist, dass das Term-Rewriting von geschlossenen $\Sigma^+$ -Termen äquivalent zum DPO-Rewriting von geschlossenen E-Hypergraphen ist.
Handhabung graphischer Äquivalenz: Der Ansatz handhabt „graphische Äquivalenz“ (Permutationen nicht-interagierender Substitutionen) natürlich, ohne dass explizite Substitutionsknoten erforderlich sind. Im kategorialen Modell wird explizite Substitution als Komposition modelliert, und die strukturellen Gesetze der Kategorie absorbieren die notwendigen Äquivalenzen.
Fallstudie ( $\lambda_{lsub}$ ): Die Autoren wenden die Theorie auf den linearen Substitutionskalkül ( $\lambda_{lsub}$ ) an. Sie zeigen, dass Terme mit expliziten Substitutionen (z. B. Let-Bindings) direkt als String-Diagramme dargestellt werden können.
- Im Gegensatz zu konventionellen E-Graphen, die explizite Knoten für Substitution und Rewrite-Regeln benötigen, um deren Permutation zu handhaben, behandelt das kategoriale Modell diese als strukturelle Eigenschaften des Diagramms.
- Die Arbeit zeigt, dass semantisch äquivalente Programme (z. B. die Umordnung von Let-Bindings) auf dasselbe String-Diagramm abbilden, wodurch die Equality Saturation auf einer normalisierten Repräsentation operieren kann.

Bedeutung und Ansprüche

Die Arbeit beansprucht, eine fundamentale kategoriale Semantik für E-Graphen mit Bindung zu liefern, ein Bereich, der zuvor unterentwickelt war.

Theoretische Rechtfertigung: Sie bietet eine rigorose Rechtfertung für die aufrechterhaltenen Kongruenzen von E-Graphen mit Bindung, indem sie diese in den Eigenschaften von geschlossenen symmetrischen monoidalen SLat-Kategorien begründet.
Effizienzpotenzial: Durch die Absorption struktureller Gleichungen (wie Assoziativität, Kommutativität und Substitutions-Permutationen) in die grafische Syntax und die zugrunde liegende Kategorie zielt der Ansatz darauf ab, die „Bürokratie“ im Equality-Saturation-Zustandsraum zu reduzieren. Dies steht im Gegensatz zu Ansätzen, die diese als explizite Rewrite-Regeln behandeln.
Geltungsbereich: Die Autoren geben explizit an, dass ihr Ansatz für den $\lambda$ -Kalkül und Variationen davon spezialisiert ist, indem er die metatheoretische interne Sprache des kategorialen Modells nutzt. Sie räumen ein, dass Slotted E-Graphen flexibler für beliebige Sprachen mit Bindern (wie den $\pi$ -Kalkül) sein mögen, argumentieren jedoch, dass ihre Methode für $\lambda$ -Kalkül-spezifische Optimierungen überlegen ist.

Die Arbeit präsentiert keine vollständige Softwareimplementierung oder empirische Benchmarks, sondern positioniert die geschlossene E-Hypergraph-Repräsentation als eine lebensfähige Grundlage für den Aufbau von „E-Graphen für String-Diagramm-Rewriting“ in zukünftiger Arbeit.