Lambda MicroEgg: Ein E-Graph, der gebundene Variablen wirklich versteht

Philip Zucker hat mit Lambda MicroEgg einen E-Graph veröffentlicht, der Alpha-Äquivalenz und Capture-vermeidende Substitution direkt unterstützt. Der auf Max Willseys MicroEgg aufbauende Prototyp führt Binder, Miller-Patterns und Higher-Order-Anwendungen in eine s-expression-basierte Oberfläche ein. In einem AC-Sättigungslauf mit 100 Runden verarbeitet er 262.291 Unions und 57.012 E-Knoten in etwa 1,5 Sekunden – etwas langsamer als egg, aber ohne nennenswerten Overhead durch die in einem Byte des u32-Id gespeicherten Liftings.