最適簡約と相互作用ネット

最適簡約 (optimal reduction / beta-optimal) は、λ計算の評価で同じ計算を二度行わないようλ内部の計算まで共有しながら簡約する理論。Lévy の最適性概念を、Lamping の Abstract Algorithm が実現した。教科書は Asperti & Guerrini “The Optimal Implementation of Functional Programming Languages”。

なぜ難しいか

• 通常の共有（グラフ簡約）は項をグラフ表現し部分項を共有するが、λ抽象の本体（自由変数を持つ計算）は素朴には共有できない。
• Haskell の thunk は共有式への参照をメモするが、λがあると本体の計算を共有しきれない。clone を完全に無くすと実用性を失う。

相互作用ネットによる解法

• Interaction Net はチューリングマシンとλ計算を組み合わせた局所的書き換えグラフモデル。最適簡約を局所規則で実現できる。
• superposition（重ね合わせ {a b}） と incremental な dup（複製） により、外側のλからレイヤーごとに on-demand でコピーし、本体の計算を一度だけ評価して共有する。
• 素朴な実装はポインタ参照が多く遅かったが、SIC ベースのフォーマットで大幅高速化（HVM で実用化）。

関連

• 実用ランタイムはhvm-runtime、土台はlambda-calculus・term-rewriting。
• 並列関数型言語 Cloe も並列グラフ簡約を志向。
• _moc-prog-lang