CEK機械のソースを表示

'''CEK機械'''<ref name="cek">[[Matthias Felleisen]] and [[Matthew Flatt]]. [http://www.ccs.neu.edu/home/matthias/3810-w02/mono.ps.gz Programming Languages and Lambda Calculi]. Unpublished manuscript, 1989-2001</ref>とは、[[ラムダ計算]]に対して[[評価戦略#値渡し|値渡し評価戦略]]の[[操作的意味論]]を与えるための[[抽象機械]]の1つである。CEKとは、機械の状態を構成する3つの要素である “Control string”, “Environment”, “Continuation” に由来する<ref name="cek"/>。

== 定義 ==
拡張ラムダ計算に対するCEKは次のように定義される<ref name="cek"/>。

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

<div style="margin: 1em; padding: 1em; border:1px solid #999">
(式)<br />
<!-- mathの中で日本語が使えないので、むりやり整形する。もし日本語が使えるようになったらalign環境で書き直してください。 -->
<math>M ::=</math><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<math>X</math> (変数)<br/>
&nbsp;&nbsp;<math>| \ \lambda X. M</math> (λ抽象)<br/>
&nbsp;&nbsp;<math>| \ M \ M</math> (関数適用)<br/>
&nbsp;&nbsp;<math>| \ b</math> (基本定数)<br/>
&nbsp;&nbsp;<math>| \ o^n \ M \ ... \ M</math> (プリミティブオペレータの適用)

(値)<br/>
<math>V ::= \lambda X. M \ | \ b</math>
</div>

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

<div style="margin: 1em; padding: 1em; border:1px solid #999">
(環境)<br/>
<math>E ::= \left\lbrace\left\langle X, c\right\rangle , ...\right\rbrace</math> (変数から、クロージャへの関数(変数とクロージャのペアの集合))<br/>
<math>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 \ne X\right\rbrace</math>

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

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

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

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

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

<div style="margin: 1em; padding: 1em; border:1px solid #999">
(変数の値の環境からの取得)<br/>
<math>\left\langle \left\langle X, E\right\rangle , K\right\rangle </math><br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<math> \longmapsto_\mathsf{cek} \left\langle c, K\right\rangle</math> (<math>E(X) = c</math> のとき)

(関数適用の関数部分の評価の開始)<br/>
<math>\left\langle \left\langle M_1 \ M_2, E\right\rangle , K\right\rangle </math><br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<math> \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 </math>

(プリミティブオペレータ適用の引数の評価の開始)<br/>
<math>\left\langle \left\langle o \ M_1 \ M_2 \ ..., E\right\rangle , K\right\rangle </math><br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<math> \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 </math>


(関数の適用)<br/>
<math>\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 </math><br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<math> \longmapsto_\mathsf{cek} \left\langle \left\langle M, E[X \leftarrow \left\langle V, E'\right\rangle ]\right\rangle , K\right\rangle</math> (<math>V</math>が変数でない場合)

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

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

(プリミティブオペレータの適用)<br/>
<math>\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 </math><br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<math> \longmapsto_\mathsf{cek} \left\langle \left\langle V, \emptyset \right\rangle, K\right\rangle</math> (<math>V</math>は<math>o</math>に<math>b_1, ..., b_i, b</math>を適用した結果)
</div>

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

<div style="margin: 1em; padding: 1em; border:1px solid #999">
<math>\mathit{eval}_\mathsf{cek}(M) = b</math>&nbsp;&nbsp;&nbsp;&nbsp;(<math>\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</math> のとき)

<math>\mathit{eval}_\mathsf{cek}(M) = \mathsf{function}</math>&nbsp;&nbsp;&nbsp;&nbsp;(<math>\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</math> のとき)
</div>

== Defunctionalizationとの関係 ==

CEK機械は、ラムダ計算の標準的な評価関数に対して、[[クロージャ変換]]、値渡し評価戦略の[[CPS変換]]、[[defunctionalization]]を順に適用することで導出できる<ref name="cek_as_defunc">[[Olivier Danvy]]. [http://www.cs.bham.ac.uk/~hxt/cw04/danvy.pdf On Evaluation Contexts, Continuations, and the Rest of the Computation]. In ''Proceedings of the Fourth ACM SIGPLAN workshop on Continuations'', 2004.</ref>。ここで、値渡し評価戦略の代わりに[[評価戦略#名前呼び|名前渡し評価戦略]]を使うと[[Krivineの機械]]が導出される<ref name="cek_as_defunc"/>。

== 拡張 ==
CEK機械はCPS変換した評価関数から導出するため、[[call/cc]]や[[shift/reset]]といったCPS変換で実装できる演算子との相性が良い<ref name="shift_reset_cek">[[Małgorzata Biernacka]], [[Dariusz Biernacki]], and [[Olivier Danvy]]. [http://www.brics.dk/RS/03/41/ An Operational Foundation for Delimited Continuations in the CPS hierarchy]. BRICS research report RS-05-24, 2005. ISSN 0909-0878</ref>。

例えば、次のように拡張することで、call/ccを追加できる。
<div style="margin: 1em; padding: 1em; border:1px solid #999">
<math>M ::= ... \ | \ \mathrm{call/cc} \ X. M</math>

<math>V ::= ... \ | \ \left\langle \mathsf{esc}, K\right\rangle </math>

<math>\left\langle \left\langle \mathrm{call/cc} \ X. M, E\right\rangle , K\right\rangle </math><br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<math>\longmapsto_\mathsf{cek} \left\langle \left\langle M, E[X \leftarrow \left\langle \mathsf{esc}, K\right\rangle ]\right\rangle , K\right\rangle</math>

<math>\left\langle \left\langle V, E\right\rangle , \left\langle \mathsf{fun}, \left\langle \mathsf{esc}, K'\right\rangle , K\right\rangle \right\rangle</math><br/>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<math>\longmapsto_\mathsf{cek} \left\langle \left\langle V, E\right\rangle , K'\right\rangle</math>(<math>V</math>が変数でない場合)
 
<math>\mathit{eval}_\mathsf{cek}(M) = \mathsf{function}</math>&nbsp;&nbsp;&nbsp;&nbsp;(<math>\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</math> のとき)
</div>
== 参考文献 ==
<references/>

{{DEFAULTSORT: CEKきかい}}

[[Category:関数型プログラミング]]
[[Category:仮想機械]]
[[Category:抽象機械]]