CEK機械

CEK機械とは、ラムダ計算に対して値渡し評価戦略の操作的意味論を与えるための抽象機械の1つである。CEKとは、機械の状態を構成する3つの要素である “Control string”, “Environment”, “Continuation” に由来する。

定義

拡張ラムダ計算に対するCEKは次のように定義される。

まず、拡張ラムダ計算を次のように定義する。

(式)
$M::=$
    $X$ (変数)
  $|\ \lambda X.M$ (λ抽象)
  $|\ M\ M$ (関数適用)
  $|\ b$ (基本定数)
  $|\ o^{n}\ M\ ...\ M$ (プリミティブオペレータの適用)

(値)
$V::=\lambda X.M\ |\ b$

次に、CEK機械の状態を構成する要素を次のように定義する。

(環境)
$E::=\left\lbrace \left\langle X,c\right\rangle ,...\right\rbrace$ (変数から、クロージャへの関数(変数とクロージャのペアの集合))
$E[X\leftarrow c]=\left\lbrace \left\langle X,c\right\rangle \right\rbrace \cup \left\lbrace \left\langle Y,c'\right\rangle |\left\langle Y,c'\right\rangle \in E\land Y\neq X\right\rbrace$

(クロージャ)
$c::=\left\langle M,E\right\rangle$ (ただし、$M$の自由変数は全て$E$の定義域に含まれる)

(値)
$v::=\left\langle V,E\right\rangle$ (ただし、$V$の自由変数は全て$E$の定義域に含まれる)

(継続)
$K::=$
    ${\mathsf {mt}}$ (初期継続)
  $|\ \left\langle {\mathsf {fun}},V,K\right\rangle$ (関数適用への継続。$\lambda x.(V\ x)\ K$に相当する)
  $|\ \left\langle {\mathsf {arg}},M,K\right\rangle$ (実引数評価への継続。$\lambda f.M\ (\lambda x.(f\ x)\ K)$に相当する)
  $|\ \left\langle {\mathsf {narg}},\left\langle v,...,v,o\right\rangle ,\left\langle c,...\right\rangle ,K\right\rangle$ (プリミティブオペレータの実引数の評価およびオペレータの適用への継続。$c,...$を順に評価したあと、$v,...$と共にプリミティブオペレータ$o$を適用する、という継続。$v,...$は評価済みの値で、$c,...$はこれから評価するクロージャ)

このとき、CEK機械の状態は組$\left\langle c,K\right\rangle =\left\langle \left\langle M,E\right\rangle ,K\right\rangle$と表される。

CEK機械の遷移規則は次のように定義される。

(変数の値の環境からの取得)
$\left\langle \left\langle X,E\right\rangle ,K\right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle c,K\right\rangle$ ($E(X)=c$ のとき)

(関数適用の関数部分の評価の開始)
$\left\langle \left\langle M_{1}\ M_{2},E\right\rangle ,K\right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle M_{1},E\right\rangle ,\left\langle {\mathsf {arg}},\left\langle M_{2},E\right\rangle ,K\right\rangle \right\rangle$

(プリミティブオペレータ適用の引数の評価の開始)
$\left\langle \left\langle o\ M_{1}\ M_{2}\ ...,E\right\rangle ,K\right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle M_{1},E\right\rangle ,\left\langle {\mathsf {narg}},\left\langle o\right\rangle ,\left\langle \left\langle M_{2},E\right\rangle ,...\right\rangle ,K\right\rangle \right\rangle$

(関数の適用)
$\left\langle \left\langle V,E'\right\rangle ,\left\langle {\mathsf {fun}},\left\langle \lambda X.M,E\right\rangle ,K\right\rangle \right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle M,E[X\leftarrow \left\langle V,E'\right\rangle ]\right\rangle ,K\right\rangle$ ($V$が変数でない場合)

(関数適用の関数部分の評価後、引数部分の評価の開始)
$\left\langle \left\langle V,E'\right\rangle ,\left\langle {\mathsf {arg}},\left\langle M,E\right\rangle ,K\right\rangle \right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle M,E\right\rangle ,\left\langle {\mathsf {fun}},\left\langle V,E'\right\rangle ,K\right\rangle \right\rangle$ ($V$が変数でない場合)

(プリミティブオペレータ適用の引数1つの評価後、次の引数の評価の開始)
$\left\langle \left\langle V,E\right\rangle ,\left\langle {\mathsf {narg}},\left\langle c',...\right\rangle ,\left\langle \left\langle N,E'\right\rangle ,c,...\right\rangle ,K\right\rangle \right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle N,E'\right\rangle ,\left\langle {\mathsf {narg}},\left\langle \left\langle V,E\right\rangle ,c',...\right\rangle ,\left\langle c,...\right\rangle ,K\right\rangle \right\rangle$ ($V$が変数でない場合)

(プリミティブオペレータの適用)
$\left\langle \left\langle b,E\right\rangle ,\left\langle {\mathsf {narg}},\left\langle \left\langle b_{i},E_{i}\right\rangle ,...,\left\langle b_{1},E'\right\rangle ,o\right\rangle ,\left\langle \right\rangle ,K\right\rangle \right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle V,\emptyset \right\rangle ,K\right\rangle$ ($V$は$o$に$b_{1},...,b_{i},b$を適用した結果)

このとき、CEK機械による評価関数${\mathit {eval}}_{\mathsf {cek}}(M)$は次のように定義される

${\mathit {eval}}_{\mathsf {cek}}(M)=b$    ($\left\langle \left\langle M,\emptyset \right\rangle ,{\mathsf {mt}}\right\rangle \longmapsto _{\mathsf {cek}}^{*}\left\langle \left\langle b,E\right\rangle ,{\mathsf {mt}}\right\rangle$ のとき)

${\mathit {eval}}_{\mathsf {cek}}(M)={\mathsf {function}}$    ($\left\langle \left\langle M,\emptyset \right\rangle ,{\mathsf {mt}}\right\rangle \longmapsto _{\mathsf {cek}}^{*}\left\langle \left\langle \lambda X.M,E\right\rangle ,{\mathsf {mt}}\right\rangle$ のとき)

Defunctionalizationとの関係

CEK機械は、ラムダ計算の標準的な評価関数に対して、クロージャ変換、値渡し評価戦略のCPS変換、defunctionalizationを順に適用することで導出できる。ここで、値渡し評価戦略の代わりに名前渡し評価戦略を使うとKrivineの機械が導出される。

拡張

CEK機械はCPS変換した評価関数から導出するため、call/ccやshift/resetといったCPS変換で実装できる演算子との相性が良い。

例えば、次のように拡張することで、call/ccを追加できる。

$M::=...\ |\ \mathrm {call/cc} \ X.M$

$V::=...\ |\ \left\langle {\mathsf {esc}},K\right\rangle$

$\left\langle \left\langle \mathrm {call/cc} \ X.M,E\right\rangle ,K\right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle M,E[X\leftarrow \left\langle {\mathsf {esc}},K\right\rangle ]\right\rangle ,K\right\rangle$

$\left\langle \left\langle V,E\right\rangle ,\left\langle {\mathsf {fun}},\left\langle {\mathsf {esc}},K'\right\rangle ,K\right\rangle \right\rangle$
      $\longmapsto _{\mathsf {cek}}\left\langle \left\langle V,E\right\rangle ,K'\right\rangle$($V$が変数でない場合)

${\mathit {eval}}_{\mathsf {cek}}(M)={\mathsf {function}}$    ($\left\langle \left\langle M,\emptyset \right\rangle ,{\mathsf {mt}}\right\rangle \longmapsto _{\mathsf {cek}}^{*}\left\langle \left\langle \left\langle {\mathsf {esc}},K\right\rangle ,E\right\rangle ,{\mathsf {mt}}\right\rangle$ のとき)