ラムダ計算と簡約

λ計算 (lambda calculus) は関数の抽象（λx. M）と適用（M N）だけからなる計算モデル。チューリングマシンと等価な計算能力を持ち、関数型プログラミングと型理論の基礎をなす。

変換規則

• β-簡約 (β-reduction): $(\lambda x.M)N\to M[x:=N]$。適用の評価そのもの。
• η-変換 (eta-conversion): $\lambda x.(fx)\to f$（外延性）。
• ζ-簡約 (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。
• 簡約の効率化はoptimal-reduction、実装ランタイムはhvm-runtime。
• _moc-prog-lang