CEK機械

ウィキペディア

CEK機械

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/02/27 16:50 UTC 版)

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$ (関数適用への継続)
  $|\ \left\langle {\mathsf {arg}},M,K\right\rangle$ (実引数評価への継続)
  $|\ \left\langle {\mathsf {narg}},\left\langle v,...,v,o\right\rangle ,\left\langle c,...\right\rangle ,K\right\rangle$ (プリミティブ操作の実引数の評価および適用への継続)

このとき、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$が変数でない場合)

$\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$ のとき)