等式飽和とe-graph

等式飽和 (Equality Saturation) は、項に書き換え規則を非破壊的に適用し続け、到達可能な等価項をすべて保持してから最適なものを抽出する最適化・探索手法。2009年の “Equality saturation: a new approach to optimization” で提案された。古典的なterm-rewriting（破壊的書き換え）が抱えるフェーズ順序問題（どの規則をどの順で適用するか）を、すべての書き換えを同時に保持することで回避する。

e-graph

中核となるデータ構造が e-graph (equivalence graph)。項の集合とその上の合同関係 (congruence) をコンパクトに表す。

• e-class: 等価な項の集合。union-find ($U$) で id を管理。
• e-node: 演算子 $f$ と引数（引数は e-class への参照）。canonicalize(f(a_1,...)) = f(find(a_1),...)。
• 部分木は可能な限り共有され（hash consing 的）、指数的な数の等価項を高い共有で保持できる。DAG に似る。
• e-graph $(U,M,H)$ は3つの合同関係を表す: e-class id の同一性 ${\equiv }_{id}$、e-node の同一性 ${\equiv }_{node}$、項の同一性 ${\equiv }_{term}$。

アルゴリズム: 初期項を挿入 → 規則集合を繰り返しマッチ・追加（マージのみ、消去しない）→ 飽和（新たな等価性が出ない）かタイムアウトまで継続 → コスト関数で最良項を extract する。

主要実装と拡張

• egg: Max Willsey らによる Rust 実装。rebuilding（合同の遅延回復）と e-class analysis（join semilattice 上の解析）で高速・拡張可能。
• Metatheory.jl: Julia 実装。EGraph → saturate! → extract!。
• e-graph intersection: 2つの e-graph の共通部分を飽和に似た手続きで計算（合成・検証に応用）。
• proof-producing congruence closure: 等価性に証明（説明）を付与し、Lean 等の証明項を再構築。

応用

• コンパイラ最適化（浮動小数点精度改善 Herbie、線形代数 SPORES、ベクトル化 diospyros）。
• テンソルグラフのスーパー最適化 (TENSAT、TASO の再実装)。
• CAD モデル合成 (Szalinski)、書き換え規則の自動発見、sketch-guided な大規模式の誘導。
• 定理証明: egg を Lean 4 のタクティクとして統合（Marcus Rossel）。束縛変数を第一級に扱う slotted e-graph (PLDI 2025) を生み、Terence Tao 主導の Equational Theories Project で4694法則・約2200万含意の検証を支えた。

関連

• 基盤はterm-rewriting、束縛変数の扱いはlambda-calculus。
• 抽出はコンパイラ最適化 compiler-optimization と直結。
• _moc-prog-lang