項書換えと抽象書き換え

項書換えシステム (Term Rewriting System, TRS) は、書き換え規則 $\ell ⇝r$ の集合により項を変換していく計算モデル。計算そのものを書き換えとして表し、書き換えは一般に非決定的。抽象書き換え (Abstract Rewriting) はこれを抽象化した分野で、言語クラス・論理学・圏論とも関連する。

正規形と効率

• TRS の応用では正規形 (normal form) の計算が基本手続き。言語の意味論は項の正規形であり、単語問題や方程式論の項の統一にも正規形が使われる。
• 木として素朴に書き換えると非効率なので、DAG 表現で部分項を共有すると効率化できる。非左線形システムでも効率的な戦略が得られる。
• 論理回路合成では AIG (And-Inverter Graph) の DAG-aware rewriting、FHE 回路の乗算深さ最小化では cone rewriting（DVD 問題＝Dag vertex deletion problem としての組合せ最適化）など、ドメイン特化の書き換えがある。

グラフ簡約と発展

• グラフ簡約 (graph reduction): 項を木でなくグラフで表し共有を保ちながら簡約する手法。関数型言語処理系の実行モデルの基礎で、optimal-reductionへ繋がる。
• 破壊的な書き換えは局所解やループに陥るため、非破壊的に等価項を保持するequality-saturation（e-graph）へ発展した。

関連

• 非破壊版はequality-saturation、簡約戦略の最適化はoptimal-reduction。
• λ項の簡約規則はlambda-calculus。
• _moc-prog-lang