CEK機械
定義

拡張ラムダ計算に対する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  のとき)