抽象機械

λ計算などの高レベル計算モデルを、状態遷移で機械的に実行するための仮想機械。評価戦略（CBV/CBN/遅延）を明示の状態に落とし込み、インタプリタ・コンパイラ・継続の扱いの土台になる。

代表的な機械

CEK 機械の状態遷移（具体）

CEK の状態は3つ組 ⟨ C, E, K ⟩:

• C (Control) — 今評価している式
• E (Environment) — 変数 → 値（クロージャ）の束縛
• K (Kontinuation) — 「この値が出たら次に何をするか」を表すスタック

値はクロージャ ⟨λx.body, E⟩（λ本体＋捕捉した環境）。継続フレームは2種類だけ:

K ::= Done                       -- 最終。値が出たら停止
    | Arg(e, E') · K             -- 「関数を評価中、出たら引数 e を E' で評価せよ」
    | Fun(⟨λx.body, E'⟩) · K     -- 「引数を評価中、出たらこのクロージャを適用せよ」

遷移規則（CBV・左から評価）:

⟨ x,       E, K ⟩  ↦  ⟨ v,    E'', K ⟩          where E(x) = v=⟨_,E''⟩   -- 変数参照
⟨ (e1 e2), E, K ⟩  ↦  ⟨ e1,   E,   Arg(e2,E)·K ⟩                         -- 適用: 先に関数部
⟨ λx.b,    E, Arg(e2,E')·K ⟩ ↦ ⟨ e2, E', Fun(⟨λx.b,E⟩)·K ⟩              -- 関数値が出た → 引数へ
⟨ v,       _, Fun(⟨λx.b,E'⟩)·K ⟩ ↦ ⟨ b, E'[x↦v], K ⟩                    -- 引数値が出た → β適用

例: (λx.x) y を E = {y ↦ v} の下で評価する全ステップ。

⟨ (λx.x) y,  E, Done ⟩
↦ ⟨ λx.x,     E, Arg(y,E)·Done ⟩            -- (適用) 関数部 λx.x へ
↦ ⟨ y,        E, Fun(⟨λx.x,E⟩)·Done ⟩       -- 関数値 → 引数 y を評価
↦ ⟨ v,        E, Fun(⟨λx.x,E⟩)·Done ⟩       -- (変数) y を v に解決
↦ ⟨ x,        {x↦v}, Done ⟩                 -- (β) クロージャ適用、本体 x を新環境で
↦ ⟨ v,        E, Done ⟩                     -- (変数) x を v に解決 → Done で停止

ポイントは K が明示のスタックなので、再帰呼び出しを使わず純粋な while ループで評価器が書けること。継続を第一級データにすれば call/cc・例外・末尾呼び出し（K を伸ばさず付け替える）が同じ枠組みで自然に表現できる。

なぜ使うか

• 評価戦略を状態遷移として形式化でき、正しさ証明・停止性議論がしやすい
• 高レベルな簡約（β簡約）を、環境・スタック・継続という実装可能な部品に分解する
• CEK の K ＝ 継続であり、コールスタックを第一級のデータとして扱える → 限定継続や例外の実装が明快に

実用言語の処理系は事実上いずれかの抽象機械をコアに持つ（GHC=STG、OCaml=ZAM、Prolog=WAM）。

押さえどころ（カード化候補）

• 抽象機械とは → λ計算等の高レベル計算モデルを、状態遷移で機械的に実行する仮想機械。評価戦略（CBV/CBN/遅延）を明示の状態に落とし込み、インタプリタ/コンパイラ/継続の土台になる
• SECD → Landin 1964、λ計算を実行する最初の抽象機械。Stack/Environment/Control/Dump の4レジスタ
• CEK → Control/Environment/Kontinuation の3つ組。継続 K を明示スタックとして持つので評価器が再帰なしの while ループで書け、call/cc・例外・末尾呼び出しが自然に表現できる（CBV）
• 継続＝スタック → CEK の K は「値が出たら次に何をするか」のフレーム列。これを第一級データにすると限定継続・例外が実装できる。末尾呼び出しは K を伸ばさず付け替えるだけ
• 実用処理系のコア → GHC=STG（遅延）、OCaml=ZAM、Prolog=WAM、Caml の語源=CAM。実用言語処理系は事実上いずれかの抽象機械をコアに持つ

関連

• λ計算 — 抽象機械が実行する対象の計算モデル
• 継続 / 限定継続 — CEK 等が継続を状態として明示化
• 簡約 — 抽象機械は簡約戦略を機械化したもの
• スタック指向 — SECD/ZAM はスタックマシン
• 末尾呼び出し最適化 — 継続/スタックの再利用と表裏
• OCaml — バイトコードを ZAM で実行