CPS 変換と A 正規形変換

C. Flanagan 等 The Essence of Compiling with Continuations (1993) 遊びを続けます。論文とはちょっと異なる道筋を辿って、CPS 変換と A 正規形変換の意味をおおまかに考えてみることにします。

論文では、事例として次に示す式をコンパイル対象に選んでいます。ここでも、これを使うことにします。

(+ (+ 2 2) (let (x 1) (f x)))

最初に、インタープリタでこの式を評価することにします。引数の評価順を左から右として先行評価をおこなうと、次のように、太字の部分の評価が逐次進んでいきます。

  1. (+ (+ 2 2) (let (x 1) (f x)))
  2. (+ (+ 2 2) (let (x 1) (f x)))
  3. (+ (+ 2 2) (let (x 1) (f x)))
  4. (+ (+ 2 2) (let (x 1) (f x)))
  5. (+ (+ 2 2) (let (x 1) (f x))) ; 変数 x を 1 に束縛
  6. (+ (+ 2 2) (let (x 1) (f x)))
  7. (+ (+ 2 2) (let (x 1) (f x)))
  8. (+ (+ 2 2) (let (x 1) (f x)))
  9. (+ (+ 2 2) (let (x 1) (f x)))

論文図 3 の CPS 変換は、上の評価順で評価をおこなっては結果を続きの評価を担当するλ式へ渡していくように式を変換します。それだけでなく、深さ優先で木をトレースすると、上の評価順と同じ順番で該当する式の部分が出現するように変換がおこなわれます。試しに論文の CPS 変換結果を書き直して、上の評価器の評価箇所に対応する部分を同じように太字にすると、そうなっているのがわかります。

((λ (k2) ((λ (k3) (k3 2))
           (λ (t1) ((λ (k4) (k4 2))
                     (λ (t2) (+' k2 t1 t2))))))
 (λ (t3) ((λ (k5) 
            ((λ (k6) (k6 1))
             (λ (t4) (let (x t4)
                        ((λ (k7) ((λ (k8) (k8 f))
                                   (λ (t5) ((λ (k9) (k9 x))
                                             (λ (t6) (t5 k7 t6))))))
                         k5)))))
           (λ (t7) (+' k t3 t7)))))

さて、論文では続いて CPS 変換された式をβ簡約するのですけど、ここではいきなり図 6 の逆 CPS 変換を施してみます。すると、上の式から継続(k ナントカ)が消えて、一時変数(t ナントカ)だけが残ります。

(let (t1 2)
  (let (t2 2)
    (let (t3 (+ t1 t2))
      (let (t4 1)
        (let (x t4)
          (let (t5 f)
            (let (t6 x)
              (let (t7 (t5 t6))
                (+ t3 t7)))))))))

そうして得られた式は、評価器と同じ順番で式を逐次評価する式になっています。この式からさらに一時変数を削除してやると、スタックマシンである SECD マシン向けの仮想コードになります。わざわざ逆 CPS 変換しなくても、CPS 変換した段階で、式を深さ優先でトレースすれば、同じ仮想コードを得ることが可能なため、論文の図 3 の CPS 変換は SECD マシン向けの仮想コードを得るのに向いている中間コードへのコンパイル処理であると言えるのでしょう。なお、ここでは変数は識別子のままにしてますけど、実用上ではコンパイル環境を作って変数を環境のディスプレイにコンパイルするのが普通です。

((CONST 2) (CONST 2) (ADD) (CONST 1) (SET x) (FETCH f) (FETCH x) (AP 1) (ADD))
; ここで、(AP N) はスタック上の実引数 N 個をクロージャへ摘要するとする。

ところが、CEK マシンはスタックを使わず継続だけで評価を進めていくため、上の中間コードでは冗長すぎます。CEK マシンでは項のリストを一度に評価し終えて関数摘要する方が遷移が楽になります。スタックなしで一度に評価できるのは値(定数、変数、λ式)だけなので、値に限定して一時変数を簡約します。

(let (t3 (+ 2 2))
  (let (x 1)
    (let (t7 (f x))
      (+ t3 t7))))

念のため、最初の評価器の評価手順から対応するステップを書き出してみます。

  1. (+ (+ 2 2) (let (x 1) (f x)))
  2. (+ (+ 2 2) (let (x 1) (f x)))
  3. (+ (+ 2 2) (let (x 1) (f x)))
  4. (+ (+ 2 2) (let (x 1) (f x)))

これはまさに、図7 の A 正規形の評価文脈の定義に沿ったものになっています。

以上、CPS 変換は SECD マシン向けで、CEK マシンには粒度が細かくなりすぎているため、関数摘要の項を CEK マシン向けにまとめたものが A 正規形なのだと、おおまかに捉えてみました。