ИИтог

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

инструментыРедакция ИИтогHacker News🔥57Рейтинг ИИтог57Влияние60Новизна55Релевантность70Неожиданность38Участники35Достоверность88

Разработчик блога philipzucker.com (на GitHub, philzook58) опубликовал Lambda MicroEgg (lambda-microegg), инструмент для работы с e-графами (e-graph, структура данных для компактного представления множества эквивалентных выражений и их переписывания) с фронтендом на основе s-выражений. Инструмент построен поверх microegg, более раннего проекта Max, к которому автор добавил три вещи: встроенную поддержку корректно-скоуп-ированных, альфа-осознанных биндеров (связывающих конструкций вроде lambda или суммы), паттерны Миллера высшего порядка и захватоустойчивую (capture-avoiding) подстановку в правых частях правил переписывания. Паттерны Миллера, по определению автора, это паттерны высшего порядка, в которых метапеременная должна быть применена к различным связанным переменным, а не к произвольным термам; на практике это позволяет, например, записать бета-редукцию лямбда-терма как одно обычное правило переписывания, и в демонстрации (lam x x) 42 инструмент корректно сводит выражение к 42.

Автор приводит бенчмарк на классической AC-задаче (ассоциативность и коммутативность сложения цепочки из 10 чисел, 100 итераций правил). В варианте с обычной, первопорядковой записью применения функций граф после насыщения вырастает до 1023 классов и 57012 e-узлов, а фаза применения правил (apply) занимает около 1000 мс (999.98 мс); для сравнения автор указывает, что на его машине библиотека egg решает похожую задачу примерно за 0,6 с, то есть Lambda MicroEgg работает медленнее, но не радикально. Если вместо первопорядковой записи использовать нотацию высшего порядка для применения функций (HOApp), тот же тест даёт уже 2046 классов и 58035 e-узлов, а фаза apply занимает 1,29 с, заметный рост стоимости из-за более сложного кодирования аппликации.

Отдельно автор демонстрирует, что альфа-эквивалентные термы (различающиеся только именами связанных переменных) хранятся в памяти как один и тот же объект благодаря хеш-консингу, а также что термы, отличающиеся по числу связанных, но не используемых переменных в контексте, частично делят память, то есть память тратится только на переменные, реально задействованные в терме, а не на все формально находящиеся в области видимости. Среди ограничений автор называет поддержку только «упорядоченных» паттернов Миллера: если нелинейная метапеременная (используемая в паттерне дважды) в разных местах применена к переменным в разном порядке, инструмент выдаёт ошибку и предлагает переставить аргументы уже в правой части правила. Автор также отмечает, что был удивлён, увидев комбинаторный взрыв на примере слияния map и comp (map/comp fusion), и перечисляет планы на будущее: поддержать больше семи переменных без лишних затрат на неиспользуемые (склоняясь к идее «эфемерных e-узлов»), попробовать встроить в систему алгоритмы Бухбергера и завершение по мультимножествам/строкам/полукольцам, а также в следующую очередь заняться выводом доказательств в стиле Lean.

Ключевые факты

  • Lambda MicroEgg расширяет более ранний инструмент microegg (проект Max) встроенными биндерами, паттернами Миллера высшего порядка и захватоустойчивой подстановкой в правилах переписывания
  • На тесте AC-10 (насыщение по ассоциативности-коммутативности, 100 итераций) граф вырос до 1023 классов и 57012 e-узлов, фаза apply заняла ~1000 мс против ~0,6 с у библиотеки egg на похожей задаче
  • Версия с настоящим применением функций высшего порядка (HOApp) на том же тесте даёт 2046 классов, 58035 e-узлов и apply-фазу 1,29 с, заметно дороже из-за более сложного кодирования
  • Инструмент выражает бета-редукцию лямбда-термов одним правилом переписывания и хранит альфа-эквивалентные термы в памяти как единый объект благодаря хеш-консингу
  • Пока поддерживаются только «упорядоченные» паттерны Миллера: при нелинейном использовании метапеременной с переменными не по порядку инструмент выдаёт ошибку и просит переставить аргументы в правой части

Почему это важно

E-графы (e-graph), структура данных, лежащая в основе современных компиляторных оптимизаторов и систем автоматического доказательства (equality saturation), но традиционно они плохо дружат со связывающими конструкциями вроде лямбда-выражений: переменные приходится кодировать вручную, теряя часть эффективности хранения. Lambda MicroEgg встраивает поддержку биндеров и альфа-эквивалентности прямо в ядро e-графа, что упрощает работу с языками и системами типов, где связывание переменных, центральная часть синтаксиса.

Кому это важно

Разработчикам компиляторов и оптимизаторов на основе e-графов (в духе egg, egglog), исследователям в области языков программирования и автоматизированного вывода, а также авторам инструментов для доказательства теорем, которым нужна встроенная поддержка бета-редукции и сопоставления термов с биндерами.

Как это применить

Код Lambda MicroEgg открыт на GitHub (repo lambda-microegg), а на сайте автора выложена WASM-демонстрация, позволяющая попробовать инструмент прямо в браузере. Правила переписывания задаются в виде s-выражений с собственной нотацией для биндеров (@) и паттернов Миллера ({?a x}), что даёт возможность экспериментировать с собственными наборами правил без установки. Стоит учитывать, что инструмент экспериментальный и пока поддерживает только упорядоченные паттерны Миллера.

Можно ли доверять

Это личный технический пост в блоге разработчика (philipzucker.com), а не рецензируемая научная работа: все бенчмарки, самостоятельные замеры автора на собственном оборудовании, без независимой проверки и сравнения на едином стенде с другими библиотеками. Код и демонстрации приведены прямо в тексте и воспроизводимы, но текст источника обрывается на середине фразы перед итоговыми выводами автора, поэтому заключение статьи неизвестно.

Риски и подводные камни

По собственным замерам автора, Lambda MicroEgg пока медленнее библиотеки egg на сопоставимой задаче насыщения (около секунды против ~0,6 с), а переход на кодирование применения функций высшего порядка увеличивает время работы ещё сильнее (1,29 с). Поддержка нелинейных паттернов Миллера ограничена только упорядоченным случаем, а один из тестовых примеров (слияние map и comp) неожиданно для самого автора приводит к комбинаторному взрыву числа узлов графа, то есть готовность инструмента к использованию в реальных, а не демонстрационных задачах пока не подтверждена.

«Паттерны Миллера, это паттерны высшего порядка, в которых метапеременная должна быть применена к различным связанным переменным, а не к произвольным термам.»

— автор Lambda MicroEgg, блог philipzucker.com