ラムダ計算と簡約
λ計算 (lambda calculus) は関数の抽象（λx. M）と適用（M N）だけからなる計算モデル。チューリングマシンと等価な計算能力を持ち、関数型プログラミングと型理論の基礎をなす。
変換規則
- β-簡約 (β-reduction): 。適用の評価そのもの。
- η-変換 (eta-conversion): （外延性）。
- ζ-簡約 (zeta-reduction):
let束縛の簡約。 - いずれも変数捕獲を避ける代入 (capture-avoiding substitution) が必要。
束縛変数の表現
- 束縛変数 (bound variable) の名前衝突を避けるため、De Bruijn index がよく使われる。名前の代わりに「何階層外側のλに束縛されるか」を自然数で表す（
λx. x→λ. 0、λz.(λy. y (λx. x)) (λx. z x)→λ (λ 1 (λ 1)) (λ 2 1)）。 - De Bruijn 表現は項がバインダーを越えるたびにインデックスのシフトが要り、e-graph 等での共有を壊す（→ slotted e-graph の動機、equality-saturation）。
再帰・継続・実装
- Y コンビネータなどの不動点コンビネータで無名再帰を実現。tuple を模した不動点で相互再帰も可能。
- 継続 (continuation) は「残りの計算」の明示化。thunk（無引数関数に包んだ遅延値）や限定継続へ繋がる。
- 自由変数を捕捉するクロージャ変換（MinCaml 等のコンパイラ段階）で実装に落ちる。
- 簡約戦略を共有付きで効率化するのがグラフ簡約・最適簡約。
関連
- 型を載せるとtype-theory-lambda-cube。
- 簡約の効率化はlambda-calculus、実装ランタイムはhvm-runtime。
- _moc-lang-compilers
最適簡約と相互作用ネット
最適簡約 (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・equality-saturation。
- 並列関数型言語 Cloe も並列グラフ簡約を志向。
- _moc-lang-compilers