E-Graphs eignen sich hervorragend für Gleichungslogik, arbeiten jedoch traditionell mit Termen erster Ordnung, was bindungsbewusstes Umschreiben umständlich macht. Philip Zuckers Lambda MicroEgg erweitert Max Willseys MicroEgg um native Bindungen, Miller-Muster und capture-avoiding Substitution.
Die zentrale technische Erkenntnis besteht darin, Lifting-Annotationen (Bereichstiefe) in einem einzigen Byte zu speichern, das von der u32-E-Klassen-ID abgezweigt wird. Dadurch können alpha-äquivalente Lambda-Terme zu identischen E-Klassen hash-konsiert werden – (@lam x (@lam y (+ x y))) und (@lam a (@lam b (+ a b))) werden zum selben E-Knoten –, während nicht alpha-äquivalente, aber durch Thinning verwandte Terme tiefere Teilstrukturen teilen.
Miller-Muster {?a x y} beschränken Metavariablen darauf, nur auf verschiedene gebundene Variablen im Geltungsbereich angewendet zu werden, und bieten so ein entscheidbares Fragment des Matching höherer Ordnung. Das System unterstützt außerdem lambda-freie Anwendung höherer Ordnung über die []-Notation, die automatisch zu HOApp(Id,Id) curryt und so die verbose Kodierung (app (app f x) y) vermeidet. Beta-Substitution wird zu einer einfachen Umschreibregel.
Die Leistung liegt bei AC-Sättigungs-Benchmarks im Bereich des 2- bis 3-Fachen der Basis-egg-Bibliothek (262k Unions in ~1,5 s gegenüber ~0,6 s bei egg), wobei das Lifting-Byte bei Nichtverwendung vernachlässigbaren Overhead verursacht.
Ein Byte von den u32-E-Klassen-IDs abzweigen, um Lifting-Annotationen zu speichern, wodurch alpha-äquivalentes Hash-Consing und capture-avoiding Substitution ohne zusätzlichen Speicheroverhead ermöglicht werden
E-Graphs erster Ordnung erfordern verbose De-Bruijn-Kodierungen oder explizite Substitutionsmechanismen für Bindungen
Miller-Muster liefern ein entscheidbares, wohldefiniertes Fragment des Matching höherer Ordnung
Das Abzweigen eines Bytes von vorhandenen IDs vermeidet Allokationsoverhead für Lifting-Annotationen
Alpha-äquivalentes Hash-Consing ergibt sich natürlich aus der Lifting-Repräsentation
Ein einzelnes Byte, das von vorhandenen IDs abgezweigt wird, kann die Scoping-Disziplin kodieren und einen E-Graph erster Ordnung mit minimalem Overhead in einen höherer Ordnung verwandeln.
Die Implementierung ist Open Source unter github.com/philzook58/lambda-microegg mit einer WASM-Demo verfügbar. Der Autor plant, Proof-Logging, ephemere Enodes für weitere Variablen und die Integration mit Buchberger-/Multiset-/String-/Semiring-Completion hinzuzufügen.
DEN BELEGEN FOLGEN
Die Quellen
- Lambda MicroEgg Philip Zucker's Blog · philipzucker.com