egg

egg (e-graphs good) は Max Willsey らが開発した Rust 製の高性能・拡張可能な等式飽和フレームワーク(論文 “egg: Fast and Extensible Equality Saturation”, POPL 2021)。

特徴

  • rebuilding: 書き換えで壊れた合同関係 (congruence) の回復を遅延・バッチ化することで、従来手法より大幅に高速化。
  • e-class analysis: 各 e-class に join semilattice 上の解析値を付け、make / join / modify のインタフェースで定数畳み込み・コスト推定などを統合できる。
  • dynamic / conditional rewrite: 動的書き換えや条件付き書き換えを表現できる。
  • ワークフロー: 項を add → 規則を search/apply で飽和 → コスト関数で extract

エコシステム・応用

  • Herbie(浮動小数点精度改善)、SPORES(線形代数最適化)、diospyros(DSP ベクトル化)、Szalinski(CAD モデル合成)、TENSAT(テンソルグラフ最適化)。
  • Lean 4 のタクティク lean-egg(Marcus Rossel)で定理証明に統合され、slotted e-graph を生んだ。
  • Julia 移植が Metatheory.jl

関連