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。
関連
- 手法と e-graph の理論はequality-saturation、土台はterm-rewriting。
- 実装言語はrust-lang、応用先はcompiler-optimization。
- _moc-prog-lang