Lambda MicroEgg: e-graph с биндерами и Miller-паттернами

Philip Zucker выпустил Lambda MicroEgg — e-graph на S-выражениях с поддержкой альфа-эквивалентных биндеров, высших Miller-паттернов и capture-avoiding подстановки. Инструмент основан на microegg Max Willsey, но добавляет встроенные биндеры и нотацию для каррирования. В тестах AC-сатурация работает медленнее egg, но без значительных накладных расходов. Демо доступно в WASM.

Я был немного удивлён, что пример слияния map и comp может взорваться. Возможно, e-graph'ы отстой.

Ещё за этот день

2026-09-24