仮想機械導出のためのプログラム変換
木谷有沙

1(指導教官: 浅井健一)

はじめに
継続とは，プログラム実行中のある時点における，残りの計算のことを指す．継続を処理することは，プログラムの制御フローを操作することに等しい．継続処
理オペレータがあれば，例外処理のような挙動をユーザが定義することや，型の考慮された大域ジャンプをすることが可能になる．しかし現在，継続処理を実装しているプログラミング言語は多くない．ユーザが機械語実装するにしても，継続処理にともなうスタックやヒープのコピー操作は自明ではなく，困難である．
そこで本研究では，shift/reset を定義する λ 計算インタプリタから，それと全く同じ挙動を示すことが保3.1

スタック導入定義の通り実装された評価器では，継続の中で使われる計算の中間値は自由変数になる．本研究では変換の結果，継続はコードポインタの受け渡しにしたいので，計算の中間値が継続に含まれていては困るし，Ager らの手法を用いるためには継続から自由変数が取り除かれている必要がある．よってここでは，新しくスタックに相当する引数を評価器に導入し，計算の中間値はスタックに積んで受け渡すよう変換する．スタック導入は我々が提案し，変換前後の評価器の等価性を証明した変換である．

3.2

証されているコンパイラ及び仮想機械を導出する．

環境退避

継続の中で使われる環境（変数値リスト）も，まだそのために，変換前後の評価器が等価なものである自由変数になっている．計算の中間値と同様，これもことが保証されたプログラム変換をインタプリタに継続に含まれるのは避けたい．よって，環境は評価器施していき，低レベルな機械に近づけて行く．これはの引数としてではなく，スタックの先頭に積んで受けDanvy ら [3] の手法と同じ考え方だが，我々は彼ら渡すように変換する．環境退避は我々が提案し，変換よりも実際の機械語実装に近い仮想機械の導出を目指

前後の評価器の等価性を証明した変換である．

し，スタック導入，環境退避，戻り番地退避などの変3.3

換を新しく導入している．そうして得られた評価器を，Ager [1] らの手法に基づいてコンパイラと仮想機械へと分割する．

2

shift / reset

shift/reset とは，限定継続を処理するオペレータであり，CPS インタプリタにおいて，その定義が与えられている [2]．本研究では， shift(...) と書くと括弧内の関数に現在の継続が渡され，reset(...) と書
くと括弧内の shift で取って来られる継続が括弧内の処理のみに限定される．

戻り番地退避継続の中に含まれる継続も自由変数になっている．この継続は低レベルな実装における戻り番地に相当する．
これもスタックに積むように変更すれば，継続から完全に自由変数を取り除くことができる．戻り番地退避は我々が提案した変換であり，変換前後の評価器の等価性は，環境退避と同様の方法ですぐに検証できる．

コンパイラ及び仮想機械の導出

4Ager らの手法に則り，以下の手順で評価器を分割し，コンパイラと仮想機械を得る．
4.1

カリー化

評価器をカリー化し，項だけ受け取れば処理できる

3

プログラム変換
本研究では，call-by-value の形無し λ 計算を以下のように shift/reset で拡張したものを対象とする．

t ::= x | λx. t | t0 t1 | shift(t) | reset(t)変数，関数定義，関数呼び出しの他に shift と reset を記述できる．
値としては，関数定義の際に生成されるクロージャ部分とそれ以降に分割する．前者がコンパイラ，後者が仮想機械の処理に相当する．カリー化前後の評価器の等価性は保証されている．

4.2

関数合成に分解カリー化の結果，評価器の出力は fun 文になっているが，それぞれの fun 文で行う処理に名前を付けて関数（自由変数を含まない関数，コンビネータ）としと，shift オペレータによって取り出される継続の二つて定義し，評価器はこれらの関数を呼び出すことにすがある．

る．前節の変換で評価器から正しく自由変数が取り除

v ::= [λ(v, c).t] | [c]これらを関数型言語 OCaml を用いて実装した評価器に，以下のプログラム変換をかける．

かれていれば，各処理はここで名付けた関数と再帰呼
び出しの合成として書き換えられる．この各関数が仮想機械の命令に相当すると考えると，評価器が仮想機

il ⇒ hil, VEnv([]) :: VK([]) :: []ihIPushEnv :: il0 , VEnv(vs) :: si ⇒ hil0 , VEnv(vs) :: VEnv(vs) :: sihIPopEnv :: il0 , v :: VEnv(vs) :: si ⇒ hil0 , VEnv(vs) :: v :: sihIPushK(il) :: il0 , v :: VEnv(vs) :: si ⇒ hil0 , VEnv(vs) :: VK(il) :: sihIAccess(n) :: , VEnv(vs) :: VK(il0 ) :: si ⇒ hil0 , (List.nth vs n) :: sihIPushCls(il) :: , VEnv(vs) :: VK(il0 ) :: si ⇒ hil0 , VFun(il, vs) :: sihICall :: , VFun(il, vs) :: v :: VK(il0 ) :: si ⇒ hil, VEnv(v :: vs) :: VK(il0 ) :: sihICall :: , VCont(s0 , il00 ) :: v :: VK(il0 ) :: si ⇒ hil, hil00 , v :: s0 @sii
hIShift :: , VFun(il, vs) :: VK(il0 ) :: si ⇒ hil, VEnv(VCont(s, il0 ) :: vs) :: VK(id) :: []ihIShift :: , VCont(s0 , il00 ) :: v :: VK(il0 ) :: si ⇒ hil00 , VCont(s, il0 ) :: s0 ihReset(il) :: , VEnv(vs) :: VK(il0 ) :: si ⇒ hil0 , hil, VEnv(vs) :: VK([]) :: []i@si
h[], v :: i ⇒ hvi

図 1: 仮想機械から導かれる状態遷移規則
械の命令列を出力していると見なせるようになる．関から先に評価を行う．各状態に対して適用される数を展開すれば，もとの評価器と全く同じものになる

状態遷移規則は決定的に定められる．

ことより，この変換前後の評価器の等価性は保証されている．

4.3

この実装自体は 4.3 節で作ったモジュールの非関数化であり，非関数化の正当性より，この変換前後の評

ファンクタとモジュールで実装価器の等価性は保証されているといえる．

項を受け取ったら関数を返す部分をファンクタ，各関導出の結果得られた仮想機械では，継続処理のコー数の処理は別のモジュールとして実装する．モジュー

ドポインタの受け渡し及びスタックコピーとしての実ルを展開すれば前節と全く同じ評価器が得られること装をモデル化できている．また，処理が値まで落ちたより，この変換前後の等価性は保証されている．

ら，スタックに積まれた戻り番地を読み取りジャンプ

4.4

コンパイラと仮想機械

同じファンクタを使って，今度はランタイム処理（スタックを受け取って行う処理）をせずに命令列を出力するという挙動になっている．これは低レベルな機械での call/return の振る舞いを模倣しているといえる．

5

まとめと今後の課題

する，つまりコンパイルだけするモジュールを実装す本研究では，shift/reset を含む λ 計算のインタプリる．そして，そのコンパイル結果を受け取りランタイタに対してスタック導入，環境退避，戻り番地退避といム処理を行う仮想機械をさらに別のモジュールとしてう変換を施し，より低レベルな機械語実装に近く，継実装する．こうして得られたコンパイラ及び仮想機械

続から自由変数が取り除かれた評価器を得た．その評の定義は以下のようになる．

価器に Ager らの手法を用いて，コンパイラと仮想機械• 入力項と仮想機械の命令列
tiil::=::=::=

x | λx. t | t0 t1 | shift(t) | reset(t)IPushEnv | IPopEnv | IPushK(il)| IAccess(n) | IPushCls(il) | ICall| IShift | IReset(il)i :: il[[x, xs]][[λx. t, xs]][[t0 t1 , xs]][[shift(t), xs]][[reset(t), xs]]v
svs::=::=::=

変換のみを用いているため，本研究で得たコンパイラと仮想機械は，もともとのインタプリタと全く同じ挙動をすることが保証されている．かつ，このコンパイ
ラと仮想機械は実際の機械語実装における call/returnに近い振る舞いを模倣できている上，shift/reset の処• コンパイラ• 値を得た．変換前後の評価器の等価性が保証されている

==
=

=
=

[IAccess(get(x, xs))][IPushCls([[t, x :: xs]])]IPushEnv:: IPushK(IPopEnv:: IPushK([ICall]):: [[t0 , xs]]) :: [[t1 , xs]]
IPushK([IShift]) :: [[t, xs]]
[IReset([[t, xs]])][il, vs] | [s, il] | [vs] | [il]v :: sv :: vs• 状態遷移規則
仮想機械の状態遷移規則は図 1 のように定義される．h i の中に h i が含まれる場合は，内側の h i

理をコードポインタの受け渡し及びスタックのコピーとしてモデル化できている．今後はこの仮想機械と実際の機械語の命令セットとの対応をより明らかにし，shift/reset の機械語実装の正当性を保証するものにしたい．

参考文献[1] M. S. Ager, D. Biernacki, O. Danvy, and J. Midtgaard.
From interpreter to compiler and virtual machine: A functional derivation. Technical report, BRICS, RS-03-14,2003.
[2] O. Danvy and A. Fillinski. A functional abstraction oftyped contexts. Technical report, DIKU, 89/12, 1989.
[3] O. Danvy and K. Millikin. A rational deconstruction oflandin’s secd machine with the j operator. Logical Methods
in Computer Science, Vol. 4, 4:12, pp. 1–67, 2008.