メインメニューを開く

CEK機械[1]とは、ラムダ計算に対して値渡し評価戦略操作的意味論を与えるための抽象機械の1つである。CEKとは、機械の状態を構成する3つの要素である “Control string”, “Environment”, “Continuation” に由来する[1]

目次

定義編集

拡張ラムダ計算に対するCEKは次のように定義される[1]

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

(式)
 
      (変数)
    (λ抽象)
    (関数適用)
    (基本定数)
    (プリミティブ操作の適用)

(値)
 

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

(環境)
  (変数から、クロージャへの関数(変数とクロージャのペアの集合))
 

(クロージャ)
  (ただし、 の自由変数は全て の定義域に含まれる)

(値)
  (ただし、 の自由変数は全て の定義域に含まれる)

(継続)
 
      (初期継続)
    (関数適用への継続)
    (実引数評価への継続)
    (プリミティブ操作の実引数の評価および適用への継続)

このとき、CEK機械の状態は組 と表される。

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

 
        (  のとき)

 
       

 
       


 
        ( が変数でない場合)

 
        ( が変数でない場合)

 
        ( が変数でない場合)

 
        (   を適用した結果)

このとき、CEK機械による評価関数 は次のように定義される

     (  のとき)

     (  のとき)

Defunctionalizationとの関係編集

CEK機械は、ラムダ計算の標準的な評価関数に対して、クロージャ変換、値渡し評価戦略のCPS変換defunctionalizationを順に適用することで導出できる[2]。ここで、値渡し評価戦略の代わりに名前渡し評価戦略を使うとKrivineの機械が導出される[2]

拡張編集

CEK機械はCPS変換した評価関数から導出するため、call/ccshift/resetといったCPS変換で実装できる演算子との相性が良い[3]

例えば、次のように拡張することで、call/ccを追加できる。

 

 

 
       

 
       ( が変数でない場合)

     (  のとき)

参考文献編集

  1. ^ a b c Matthias Felleisen and Matthew Flatt. Programming Languages and Lambda Calculi. Unpublished manuscript, 1989-2001
  2. ^ a b Olivier Danvy. On Evaluation Contexts, Continuations, and the Rest of the Computation. In Proceedings of the Fourth ACM SIGPLAN workshop on Continuations, 2004.
  3. ^ Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An Operational Foundation for Delimited Continuations in the CPS hierarchy. BRICS research report RS-05-24, 2005. ISSN 0909-0878