A-normal form 再学習 その1 - Scheme VM を書く

ここに書いてある内容は古いです。A正規形まとめをご参照ください。

自分の実装で normalize のバグを発見したのだが正しいありかたに核心が持てないので論文読みに戻る。
また訳してみるメソッドを使う。

CEK machine

論文「The Essence of Compiling with Continuations」のA正規化の核心は Figure 8 にあると思うのだけど、CEK machine が分からないとだめそう。
Figure 2 前後で初出だから周辺の文章を意訳してみるか。

CEKマシンは、Figure 2 に示される遷移関数に従い状態遷移する。
例えば、ブロック (let (x M1) M2) に対する状態遷移は、current environment E の中で M1 を評価するところからはじまり、次に continuation レジスタに残りの計算である (lt x, M2, E, K) をセットする。

(訳注) Figure 2 の ( (let (x M1) M2), E, K) -> (M1, E, (lt x, M2, E, K) ) がこれに相当すると思われる。
K は continuation
E は environment

新しい continuation の結果である value が receive されたら、それを x の値として environment を拡張し、M2 の evaluation に進む。

(訳注) Figure 2 の ((lt x, M, E, K), V*) -> (M, E[x := V*], K) がこれに相当する。
V* は machine values なのだけど、ここに M1 の evaluation の結果が来るのかな。

残りの節も同様に直感的な説明。
「関連 ->*」は、遷移関数の作用遷移クロージャである。
γ関数は構文的な値と environment から machine values を構築する。
記法 E(x) は environment E のの中で x の値を lookup するためのアルゴリズムを参照します。
E[x1 := V1*, ..., xn := Vn*] は environment E を拡張し、これ以降 xi の lookup で Vi* が返るようになります。

(訳注) 関連 ->* は正直意味が分からない。
γ関数は

γ(c, E) = c
γ(x, E) = E(x)
γ((λ x1 ... xn, M), E) = (cl x1 ... xn, M, E)

のことだろう。定数は定数に、参照x は E(x) で取り出せる。

(cl x1 ... xn, M, E) はクロージャである。クロージャとは (λ x1 ... xn, M) の中のコード M、自由変数、x1 ... xn を保持したレコードである。
partial function である δ はプリミティブ演算を抽象化したものである。

(訳注) The partial function ってどういう意味?

CEK machine は、ダイレクトコンパイラをデザインするモデルを提供する。
CEK machine を元に作られたコンパイラは、environment, displays, continuation, stack を効率的な表現で実装している。
そのようなコンパイラから生成される machine code は、CEK machine がこれらの具体的な environment, continuation の表現を操作することで、抽象的な操作を実現する。

大体分かってきたので Figure 8 に行ってみる？
お。以前より読めるようになった。新たに出現しているのは数字付きの -> と ar 。
ar は page8 の後半に出てくる。訳してみよう。

A-reduction が CPSコンパイラの中間表現を生成できるように、我々は A-normal form の言語のために抽象 machine CaEK machine をデザインした。
そして、この machine が Figure 5 のCPS machine と等しいことを証明した。
CaEK machine は、Figure 6にある A-normal forma の Core Scheme サブセットに特化した CEK machine である。
この machine (Figure 8) は2種類の continuation を持つ。stop と、(ar x, M, E, K)の2つである。
CEK machine とは違い、CaEK machine は末尾文脈でない手続き呼び出しの評価するための continuation のみを作れば良い。
例えば末尾呼び出し (V V1 ... Vn) に対する遷移ルールは V をクロージャ(cl x1 ... xn, M', E') へと評価する。environment E' を値 V1 ... Vn で拡張し、M'の実行を続けるのである。
continuation はレジスタ k に残っている。
それに対して、CEK machine はすべての sub expression V, V1 ... , Vn に対して別々の continuation を作る。

だんだんと理解が怪しくなってきたな。
このあたりは、id:scinfaxiさんが Scheme のネイティブコンパイラを書かれているみたいなので話があいそうだ。＞＜。