CEK機械

定義

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

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

(環境)
${\displaystyle E::=\left\lbrace \left\langle X,c\right\rangle ,...\right\rbrace }$ (変数から、クロージャへの関数(変数とクロージャのペアの集合))
${\displaystyle 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 }$

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

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

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

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

(関数適用の関数部分の評価の開始)
${\displaystyle \left\langle \left\langle M_{1}\ M_{2},E\right\rangle ,K\right\rangle }$
      ${\displaystyle \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 }$

(プリミティブオペレータ適用の引数の評価の開始)
${\displaystyle \left\langle \left\langle o\ M_{1}\ M_{2}\ ...,E\right\rangle ,K\right\rangle }$
      ${\displaystyle \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 }$

(関数の適用)
${\displaystyle \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 }$
      ${\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle M,E[X\leftarrow \left\langle V,E'\right\rangle ]\right\rangle ,K\right\rangle }$ (${\displaystyle V}$が変数でない場合)

(関数適用の関数部分の評価後、引数部分の評価の開始)
${\displaystyle \left\langle \left\langle V,E'\right\rangle ,\left\langle {\mathsf {arg}},\left\langle M,E\right\rangle ,K\right\rangle \right\rangle }$
      ${\displaystyle \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 }$ (${\displaystyle V}$が変数でない場合)

(プリミティブオペレータ適用の引数1つの評価後、次の引数の評価の開始)
${\displaystyle \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 }$
      ${\displaystyle \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 }$ (${\displaystyle V}$が変数でない場合)

(プリミティブオペレータの適用)
${\displaystyle \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 }$
      ${\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle V,\emptyset \right\rangle ,K\right\rangle }$ (${\displaystyle V}$は${\displaystyle o}$に${\displaystyle b_{1},...,b_{i},b}$を適用した結果)

${\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)=b}$    (${\displaystyle \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 }$ のとき)

${\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)={\mathsf {function}}}$    (${\displaystyle \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との関係

拡張

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

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

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

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

${\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)={\mathsf {function}}}$    (${\displaystyle \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 }$ のとき)

参考文献