CEK機械

CEK機械とは、ラムダ計算に対して値渡し評価戦略の操作的意味論を与えるための抽象機械の1つである。CEKとは、機械の状態を構成する3つの要素である “Control string”, “Environment”, “Continuation” に由来する。 拡張ラムダ計算に対するCEKは次のように定義される。 まず、拡張ラムダ計算を次のように定義する。 (式) M ::= {\displaystyle M::=}      X {\displaystyle X} (変数)    |   λ X . M {\displaystyle |\ \lambda X.M} (λ抽象)    |   M   M {\displaystyle |\ M\ M} (関数適用)    |   b {\displaystyle |\ b} (基本定数)    |   o n   M   . . .   M {\displaystyle |\ o^{n}\ M\ ...\ M} (プリミティブ操作の適用) (値) V ::= λ X . M   |   b {\displaystyle V::=\lambda X.M\ |\ b} 次に、CEK機械の状態を構成する要素を次のように定義する。 (環境) E ::= { ⟨ X , c ⟩ , . . . } {\displaystyle E::=\left\lbrace \left\langle X,c\right\rangle ,...\right\rbrace } (変数から、クロージャへの関数(変数とクロージャのペアの集合)) E [ X ← c ] = { ⟨ X , c ⟩ } ∪ { ⟨ Y , c ′ ⟩ | ⟨ Y , c ′ ⟩ ∈ E ∧ Y ≠ X } {\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 } (クロージャ) c ::= ⟨ M , E ⟩ {\displaystyle c::=\left\langle M,E\right\rangle } (ただし、 M {\displaystyle M} の自由変数は全て E {\displaystyle E} の定義域に含まれる) (値) v ::= ⟨ V , E ⟩ {\displaystyle v::=\left\langle V,E\right\rangle } (ただし、 V {\displaystyle V} の自由変数は全て E {\displaystyle E} の定義域に含まれる) (継続) K ::= {\displaystyle K::=}      m t {\displaystyle {\mathsf {mt}}} (初期継続)    |   ⟨ f u n , V , K ⟩ {\displaystyle |\ \left\langle {\mathsf {fun}},V,K\right\rangle } (関数適用への継続)    |   ⟨ a r g , M , K ⟩ {\displaystyle |\ \left\langle {\mathsf {arg}},M,K\right\rangle } (実引数評価への継続)    |   ⟨ n a r g , ⟨ v , . . . , v , o ⟩ , ⟨ c , . . . ⟩ , K ⟩ {\displaystyle |\ \left\langle {\mathsf {narg}},\left\langle v,...,v,o\right\rangle ,\left\langle c,...\right\rangle ,K\right\rangle } (プリミティブ操作の実引数の評価および適用への継続) このとき、CEK機械の状態は組 ⟨ c , K ⟩ = ⟨ ⟨ M , E ⟩ , K ⟩ {\displaystyle \left\langle c,K\right\rangle =\left\langle \left\langle M,E\right\rangle ,K\right\rangle } と表される。 CEK機械の遷移規則は次のように定義される。 ⟨ ⟨ X , E ⟩ , K ⟩ {\displaystyle \left\langle \left\langle X,E\right\rangle ,K\right\rangle }        ⟼ c e k ⟨ c , K ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle c,K\right\rangle } ( E ( X ) = c {\displaystyle E(X)=c} のとき) ⟨ ⟨ M 1   M 2 , E ⟩ , K ⟩ {\displaystyle \left\langle \left\langle M_{1}\ M_{2},E\right\rangle ,K\right\rangle }        ⟼ c e k ⟨ ⟨ M 1 , E ⟩ , ⟨ a r g , ⟨ M 2 , E ⟩ , K ⟩ ⟩ {\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 } ⟨ ⟨ o   M 1   M 2   . . . , E ⟩ , K ⟩ {\displaystyle \left\langle \left\langle o\ M_{1}\ M_{2}\ ...,E\right\rangle ,K\right\rangle }        ⟼ c e k ⟨ ⟨ M 1 , E ⟩ , ⟨ n a r g , ⟨ o ⟩ , ⟨ ⟨ M 2 , E ⟩ , . . . ⟩ , K ⟩ ⟩ {\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 } ⟨ ⟨ V , E ′ ⟩ , ⟨ f u n , ⟨ λ X . M , E ⟩ , K ⟩ ⟩ {\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 }        ⟼ c e k ⟨ ⟨ M , E [ X ← ⟨ V , E ′ ⟩ ] ⟩ , K ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle M,E[X\leftarrow \left\langle V,E'\right\rangle ]\right\rangle ,K\right\rangle } ( V {\displaystyle V} が変数でない場合) ⟨ ⟨ V , E ′ ⟩ , ⟨ a r g , ⟨ M , E ⟩ , K ⟩ ⟩ {\displaystyle \left\langle \left\langle V,E'\right\rangle ,\left\langle {\mathsf {arg}},\left\langle M,E\right\rangle ,K\right\rangle \right\rangle }        ⟼ c e k ⟨ ⟨ M , E ⟩ , ⟨ f u n , ⟨ V , E ′ ⟩ , K ⟩ ⟩ {\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 } ( V {\displaystyle V} が変数でない場合) ⟨ ⟨ V , E ⟩ , ⟨ n a r g , ⟨ c ′ , . . . ⟩ , ⟨ ⟨ N , E ′ ⟩ , c , . . . ⟩ , K ⟩ ⟩ {\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 }        ⟼ c e k ⟨ ⟨ N , E ′ ⟩ , ⟨ n a r g , ⟨ ⟨ V , E ⟩ , c ′ , . . . ⟩ , ⟨ c , . . . ⟩ , K ⟩ ⟩ {\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 } ( V {\displaystyle V} が変数でない場合) ⟨ ⟨ b , E ⟩ , ⟨ n a r g , ⟨ ⟨ b i , E i ⟩ , . . . , ⟨ b 1 , E ′ ⟩ , o ⟩ , ⟨ ⟩ , K ⟩ ⟩ {\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 }        ⟼ c e k ⟨ ⟨ V , ∅ ⟩ , K ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle V,\emptyset \right\rangle ,K\right\rangle } ( V {\displaystyle V} は o {\displaystyle o} に b 1 , . . . , b i , b {\displaystyle b_{1},...,b_{i},b} を適用した結果) このとき、CEK機械による評価関数 e v a l c e k ( M ) {\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)} は次のように定義される e v a l c e k ( M ) = b {\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)=b}     ( ⟨ ⟨ M , ∅ ⟩ , m t ⟩ ⟼ c e k ∗ ⟨ ⟨ b , E ⟩ , m t ⟩ {\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 } のとき) e v a l c e k ( M ) = f u n c t i o n {\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)={\mathsf {function}}}     ( ⟨ ⟨ M , ∅ ⟩ , m t ⟩ ⟼ c e k ∗ ⟨ ⟨ λ X . M , E ⟩ , m t ⟩ {\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 } のとき) CEK機械は、ラムダ計算の標準的な評価関数に対して、クロージャ変換、値渡し評価戦略のCPS変換、defunctionalizationを順に適用することで導出できる。ここで、値渡し評価戦略の代わりに名前渡し評価戦略を使うとKrivineの機械が導出される。 CEK機械はCPS変換した評価関数から導出するため、call/ccやshift/resetといったCPS変換で実装できる演算子との相性が良い。 例えば、次のように拡張することで、call/ccを追加できる。 M ::= . . .   |   c a l l / c c   X . M {\displaystyle M::=...\ |\ \mathrm {call/cc} \ X.M} V ::= . . .   |   ⟨ e s c , K ⟩ {\displaystyle V::=...\ |\ \left\langle {\mathsf {esc}},K\right\rangle } ⟨ ⟨ c a l l / c c   X . M , E ⟩ , K ⟩ {\displaystyle \left\langle \left\langle \mathrm {call/cc} \ X.M,E\right\rangle ,K\right\rangle }        ⟼ c e k ⟨ ⟨ M , E [ X ← ⟨ e s c , K ⟩ ] ⟩ , K ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle M,E[X\leftarrow \left\langle {\mathsf {esc}},K\right\rangle ]\right\rangle ,K\right\rangle } ⟨ ⟨ V , E ⟩ , ⟨ f u n , ⟨ e s c , K ′ ⟩ , K ⟩ ⟩ {\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 }        ⟼ c e k ⟨ ⟨ V , E ⟩ , K ′ ⟩ {\displaystyle \longmapsto _{\mathsf {cek}}\left\langle \left\langle V,E\right\rangle ,K'\right\rangle } ( V {\displaystyle V} が変数でない場合) e v a l c e k ( M ) = f u n c t i o n {\displaystyle {\mathit {eval}}_{\mathsf {cek}}(M)={\mathsf {function}}}     ( ⟨ ⟨ M , ∅ ⟩ , m t ⟩ ⟼ c e k ∗ ⟨ ⟨ ⟨ e s c , K ⟩ , E ⟩ , m t ⟩ {\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 } のとき)