限定継続を含む仮想機械導出のためのプログラム変換
木谷有沙
お茶の水女子大学
arisa@pllab.is.ocha.ac.jp

浅井健一
お茶の水女子大学
asai@is.ocha.ac.jp

概 要
本研究では、限定継続処理のオペレータ shift / reset に関して、正当性の保証された処理系を与えることを目的としている。その手法として、CPS のインタプリタに定義に基づいて shift / reset を追加した評価器に対し、変換前後の等価性が保証される変換のみを用いて仮想機械を導出、遷移規則を得る。その際、CPS 変換、
非関数化、カリー化等の先行研究において妥当性が保証されている変換に加え、より仮想機械の動作に近づけるために、検証が不十分と思われる変換も用いたため、その変換前後の等価性の証明もあわせて行う。現段階では、
インタプリタにスタックを導入する変換、環境をスタックに退避する変換についての検証が済んでおり、CPS の
インタープリタに妥当なプログラム変換を施すことにより、スタックへの環境退避を行うインタプリタを取得できることが分かっている。

1

はじめに
継続とは、プログラム実行中のある時点における、残りの計算のことである。継続を取り出したりコピーしたりすることは、プログラムの制御フローを編集することに相当し、強力な大域ジャンプのようなものとも考えられる。しかし、この操作は継続を取り出した部分にのみしかジャンプを許しておらず、また型システム [3, 5] も存在しており、無条件 goto 文よりも安全であるといえる。この継続処理を使って実装が容易になる例として、例
外処理がよく挙げられる。一般的なプログラミング言語においては、try/catch や raise 等の例外処理専用の機能が特別に用意され、ユーザはこれを利用するようになっている。しかし継続処理ができるプログラミング言語においては、前述のような例外処理用の機能が用意されていなくても、「現在の継続を捨てる」と書けば例外処理に相当する動作を実現できる。
このような継続処理を可能にするために、call/cc [17] や control/prompt [8], shift/reset [5] などの継続処理オ
ペレータが存在する。このうち control/prompt, shift/reset は限定継続であり、call/cc では継続の取り出される範囲が現在以降の全てであるのに対し、限定継続では取り出される継続の範囲をユーザが指定できる。
しかし現在、限定継続処理をユーザが明示的に扱えるプログラミング言語は多くない。継続渡し形式 (continuation-

passing style : CPS) のインタプリタを書くか、call/cc ライブラリを利用すれば間接実装は可能 [9] であるが、限定継続処理そのものの性能を評価したい場合等は、ユーザが機械語で限定継続処理を実装せねばならない。
そこで本研究では、機械語での限定継続処理実装のための、正当性の保証のあるモデルを提示し、限定継続を利用したプログラミングの推奨への第一歩としたい。
その手法として、CPS のインタプリタに定義に基づいて shift/reset を追加した評価器に対し、変換前後の評
価器の等価性が保証された変換のみを用いてより低レベルな評価器を導出していく。
現段階では、インタプリタに CPS 変換、非関数化、線形リスト化、スタック導入、環境退避変換を施すことにより、SECD マシン [12] に類似した抽象機械を取得しており、shift/reset によるスタックコピー及びコピー範囲の限定をモデル化できている。
関連研究

Danvy ら [7] は、SECD マシンを高階関数を使うよう書き換え、スタックを除去し、direct style に変換することで、λ計算のインタプリタを得ている。それに伴い、λ計算インタプリタに CPS 変換、非関数化を施したものが SECD マシンと bisimulation 等価であると述べられている。Ager ら [2] もλ計算インタプリタに対し CPS
変換、非関数化を施すことにより CEK マシンを得ている。この手法での shift/reset を含む抽象機械の導出そのものは Danvy ら自身によるものが既に存在する [4] が、Danvy らが SECD マシンや CEK マシン等の既存の抽象機械に近い形式の抽象機械を導出することを目的としたのに対し、本研究では環境をスタックに積むように変形する等、現実の機械により近いものの導出を目的としている。そしてその際、shift/reset の入った体系に対するスタック導入の正当性を厳密に示している。また Ager ら [1] は、抽象機械を分割して仮想機械とコンパイラを得る手法を示した。この手法を応用して、五十嵐ら [10] は backquote と unquote をサポートするマルチステー
ジ言語 λ° に対する仮想機械とコンパイラを導出している。本論文ではコンパイラの導出には触れないが、最終的には Ager らの手法にしたがって shift/reset に対するコンパイラを導出することを目指している。我々の研究グループでは shift/reset をスタックのコピーとして実装するコンパイラの作成を行っており [13]、本研究の成果はそれに対する正当性を与えるものと期待される。

2

shift / reset
shift オペレータは、現在から最新の reset までの継続 k を取り出すものである。継続を取り出すという点においては call/cc と似ているが、取り出される継続の範囲が reset で限定される点と、shift した後に k が呼び出されなければその継続は破棄されるという点において異なっている。本研究では、shift (...) と書けば、継続 kを括弧内の関数に引数として渡すものとする。たとえば 1 + shift(fun k -> 2 * (k 3)) という計算は、「値を受け取ったら１を足す」という継続が k に渡され、2 * (1 + 3) となり、8 が返ってくる。

reset オペレータは、前述の shift オペレータで取り出される継続の範囲を限定するものである。本研究では、
reset (...) と書けば、括弧内の shift オペレータで取り出される継続を括弧内の処理のみに限定するものとする。たとえば 1 + reset(4 + shift(fun k -> 2 * (k 3))) という計算は、「値を受け取ったら 4 を足す」という継続が k に渡され、1 + (2 * (4 + 3)) となり、15 が返ってくる。最初の 1 を足す部分は、reset の括弧内の shift 命令では取って来られない。

3

CPS のλ計算のインタプリタ
以下のような syntax を持つ言語を対象とする。

t ::= x | λx. t | t0 t1 | shift(t) | reset(t)変数、関数定義、関数呼び出しの他に、shift と reset を記述できる。また、値としては関数定義の際に生成されるクロージャ [x, t, e] と、shift 命令の際に取り出される継続 [c] の二つがある。

v ::= [x, t, e] | [c]これらを関数型言語 OCaml を用いて実装していく。まず、項と値の定義は以下のようになる。
1
2
3
4
5
6
7
8
9
10
11
12
13

(* 項 *)
type t = Var of string(*| Fun of string * t(*| App of t * t(*| Shift of t(*
| Reset of t(*(* 値 *)
type v = VFun of string * t * e (*| VCont of c(*(* 環 境 *)and e = ( string * v ) list(* 継 続 *)and c = ( v -> v )変 数 *)
関 数 定 義 *)関 数 呼 び 出 し *)shift *)
reset *)
ク ロ ー ジ ャ *)継 続 *)

環境は 変数名 x と値 v の組のリストとして実装した。関数 get(x, e) によって、環境 e における変数 x の値 vを得られるものとする。shift/reset の意味を与える評価器 eval1 は、以下のように定義される [6]。
12(* id : v -> v *)let id x = x

3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

(* eval : t * e * c -> v *)let rec eval (t , e , c ) = match t with
Var ( x ) -> c ( get (x , e ))| Fun (x , t ) -> c ( VFun (x , t , e ))| App ( t0 , t1 ) -> eval ( t1 , e , ( fun v1-> eval ( t0 , e , ( fun v0-> ( match v0 with( VFun (x ’ , t ’ , e ’)) -> eval (t ’ , (x ’ , v1 ) :: e ’ , c )| ( VCont (c ’)) -> c (c ’ v1 ) )))))| Shift ( t ) -> eval (t , e , ( fun v-> ( match v with( VFun (x ’ , t ’ , e ’)) -> eval (t ’ , (x ’ , VCont ( c )) :: e ’ , id )| ( VCont (c ’)) -> c ’ ( VCont ( c ))) ))| Reset ( t ) -> c ( eval (t , e , id ))

18
19
20

(* eval1 : t -> v *)let eval1 t = eval (t , [] , id )

この評価器は一般的な CPS のλ計算インタプリタに shift/reset を加えただけのものである。13 〜 16 行目がshift、17 行目が reset の処理に相当する。shift の処理では、その時点での継続を値 VCont(c) としてパッケージ
ングしてから Shift 項の引数 t （の実行結果の関数）に渡している。reset の処理では継続を id にリセットしており、これにより shift 命令で取り出される継続が限定される。これが shift/reset の定義に基づく実装である。
以下、この評価器に対して妥当性の保証された変換を施していくことで、shift/reset の低レベルな実装を得る。

4

CPS 変換評価器が全て末尾呼び出しになっていれば、引数を状態と見なすと評価器からそのまま抽象機械及び状態遷移規則が得られるが、eval1 は shift/reset 実装の際、末尾呼び出しでなくなっている箇所（12, 17 行目）がある。
そこで、eval1 に CPS 変換を施して全ての項で末尾呼び出しとし、その結果得られる評価器を eval2 とする。
この変換により、型は以下のように変わる。
12
3
4

type v = (* 前 と 同 じ *)and e = (* 前 と 同 じ *)and c = (( v * d ) -> v )and d = ( v -> v )(* 値 *)(* 環 境 *)(* 継 続 *)評価器 eval2 は以下のようになる。
1234(* cid : v * d -> v *)(* did : v -> v *)let cid (v , d ) = d v
let did x = x

5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

(* eval : t * e * c * d -> v *)let rec eval (t , e , c , d ) = match t with
Var ( x ) -> c ( get (x , e ) , d )| Fun (x , t ) -> c ( VFun (x , t , e ) , d )| App ( t0 , t1 )-> eval ( t1 , e , ( fun ( v1 , d1 )-> eval ( t0 , e , ( fun ( v0 , d0 )-> ( match v0 with( VFun (x ’ , t ’ , e ’)) -> eval (t ’ , (x ’ , v1 ) :: e ’ , c , d0 )| ( VCont (c ’)) -> c ’ ( v1 , ( fun v ’ -> c (v ’ , d0 ))))) , d1 )) , d )| Shift ( t )-> eval (t , e , ( fun (v , d ’)-> ( match v with( VFun (x ’ , t ’ , e ’)) -> eval (t ’ , (x ’ , VCont ( c )) :: e ’ , cid , d ’)| ( VCont (c ’)) -> c ’ ( VCont ( c ) , d ’))) , d )| Reset ( t ) -> eval (t , e , cid , ( fun v -> c (v , d )))

22
23
24

(* eval2 : t -> v *)let eval2 t = eval (t , [] , cid , did )eval1 はもともと CPS のインタプリタで継続 c を持っていたが、さらに CPS 変換が施された結果、継続が cと d の二つに分離されている。
この変換の正当性は、CPS 変換の正当性から直接導かれる。
定理 4.1 (CPS 変換の正当性 [16]).
任意の項 t に対し eval1 と eval2 は、どちらも評価に失敗するか、または構造的に等しい値を返す。（項 t を
eval1 で評価した結果を CPS 変換したものは、項 t を eval2 で評価した結果と等しい。）

5

非関数化
eval2 は二度の CPS 変換の結果、高階関数を多く使うようになっている。しかし、これから得ようとしている低レベルな実装では高階関数のような高級な機能はない。よって、高階関数を使わずに同等の処理を行うプロ
グラムに変換する必要がある。そのため、eval2 に対し非関数化 [16] という処理を施し、評価器 eval3 とする。
非関数化とは、プログラム中に出現する全ての高階関数 (OCaml の fun 文) に対し、その実行に必要なデータを保持できるオブジェクトを定義し、高階関数を生成する代わりにそのオブジェクトを生成するよう変更することである。さらに各オブジェクトに対し、その処理系 (apply 関数。本論文では run * という名前を使う。) を用意する。

例えば eval2 では Shift 項が評価器に渡されると OCaml の fun 文を生成する（16〜20 行目）。この fun 文の body において、c は自由変数である。c は後でこの継続を処理する際に必要なデータで、eval2 ではすぐ外のスコープの変数を参照することで実現されているが、非関数化する場合は別の場所でも実行できるようにオブジェクトの生成時にこの c を格納しておく必要がある。よって Shift 項の fun 文に相当するオブジェクトは項

c をその子要素として保持するよう定義する。他の fun 文についても同様に、body で自由変数になっているものはオブジェクトに保持するようにする。よって型の定義は以下のように変更される。
1
2
3
4
5
6
7
8
9

type v = (* 前 と 同 じ *)and e = (* 前 と 同 じ *)(* 継 続 *)and c = CApp1 of t * e * c| CApp0 of v * c| CShift of c
| CReset
and d = DRun of c * d| DReset(* 値 *)(* 環 境 *)
(*
(*
(*
(*
(*
(*

A p p 項 で 生 成 さ れ る 外 側 の fun 文 の か わ り *)A p p 項 で 生 成 さ れ る 内 側 の fun 文 の か わ り *)S h i f t 項 で 生 成 さ れ る fun 文 の か わ り *)c の id *)R e s e t 項 で d と し て 生 成 さ れ る fun の か わ り *)d の id *)続いて、各オブジェクトに対する処理系を用意する。eval2 では fun 文の中で行っていた処理を、この関数で行っている。
1
2
3
4
5
6
7
8
9
10
11
12
13
14

(* run_c : c * v * d -> v *)let rec run_c (c , v , d ) = match c with
CApp1 (t ’ , e ’ , c ’) -> eval (t ’ , e ’ , CApp0 (v , c ’) , d )| CApp0 (v ’ , c ’) -> ( match v with
VFun (x ’ , t ’ , e ’) -> eval (t ’ , (x ’ , v ’) :: e ’ , c ’ , d )| VCont (c ’ ’) -> run_c (c ’ ’ , v ’ , DRun (c ’ , d )))| CShift (c ’) -> ( match v with
VFun (x ’ , t ’ , e ’) -> eval (t ’ , (x ’ , VCont (c ’)) :: e ’ , CReset , d )| VCont (c ’ ’) -> run_c (c ’ ’ , VCont (c ’) , d ))| CReset -> run_d (d , v )(* run_d : d * v -> v *)and run_d (d , v ) = match d with
DRun (c ’ , d ’) -> run_c (c ’ , v , d ’)
| DReset -> v

fun 文の代わりに相当するオブジェクトを返すように書き換えるだけでなく、継続の処理に進む箇所は上で用意した処理系に渡すように変更する。例えば eval2 の 8 行目では Var 項が評価器に渡されると、環境から求められた値を継続 c にそのまま渡している。非関数化すると、引数 c には継続オブジェクトが入っているので、それに相当する処理をするためには上記の処理系を呼び出さなければならない。よって、eval3 では Var 項は run c(c, get(x, e), d) と変換される。他の項や d についても同様に変更し、次のような評価器 eval3 を得る。
1234(* cid : c *)(* did : d *)let cid = CReset
let did = DReset

5
6
7
8
9
10
11
12

(* eval : t * e * c * d -> v *)let rec eval (t , e , c , d ) = match t with
Var ( x ) -> run_c (c , get (x , e ) , d )| Fun (x , t ) -> run_c (c , VFun (x , t , e ) , d )| App ( t0 , t1 ) -> eval ( t1 , e , CApp1 ( t0 , e , c ) , d )| Shift ( t ) -> eval (t , e , CShift ( c ) , d )| Reset ( t ) -> eval (t , e , cid , DRun (c , d ))

13
14
15

(* eval3 : t -> v *)let eval3 t = eval (t , [] , cid , did )この変換により、OCaml の fun 文を使って受け渡されていた継続は、継続の実行に必要なデータを保持したオブジェクトとその処理系に分離された。ここで得られた継続オブジェクトは処理の段階を表すものであり、コード列のようなものと見なせる。
この変換の正当性は、非関数化の正当性から直接導かれる。
定理 5.1 (非関数化 [16] の正当性).

任意の項 t に対し eval2 と eval3 は、どちらも評価に失敗するか、または構造的に等しい値を返す。（項 t を

eval2 で評価した結果を非関数化したものは、項 t を eval3 で評価した結果と等しい。）

6

線形リスト化
前節で、eval3 で受け渡される継続オブジェクトはコード列のようなものと見なせる、と書いたが eval3 の継

続オブジェクトは実際には木構造を成しており、コード『列』であるとは言えない。ただし各継続オブジェクト
は高々一つしか c 型の子要素を持たないため、データ構造としては線形リストと見なすことができ、実装もリストに書き換えることが可能である。よって木構造でなくリストにして受け渡しするように変更し、その評価器を

eval4 とする。この変換の結果、引数 c で受け渡すものがコード列であると言えるようにする。
'
$ '
$
継続を
拡張するには、根に親要素を
¯ 追加。

²

継続を
拡張するには、リストの先頭に¯
要素を追加。

² 根 ¯

²
%
c &
©
±
°
¡©
¡
©
?
² head¯

±
°
子要素
²?
¯

±
°
tail
²?
¯

±

±

c
±

?

&
°
¡©©
¡
©

c
c

° 木構造

..?
'$
.
eval3 の継続
&%

%

c
c

° リスト
?
..
'$
.
eval4 の継続&%

図 1: eval3 と eval4 における継続

eval3 では、c 型の継続オブジェクト のうち CApp1, CApp0, CShift がさらに c 型データを保持しており、これにより継続オブジェクトが木構造を成すようになっていた。よって、これらが c 型のデータを持たないように変更する。その代わりに評価器は c 型一つではなくリストを受け渡すようにし、それまでオブジェクト中に c 型
データを保持していた箇所ではリストの先頭に新しい継続オブジェクトを付け加えることにする。すると、保持すべき c 型データをリストの tail として受け渡せる。c 型のデータを持たない CReset では、空リストを渡すよ
うに変える。d についても同様の変換を施す。この結果、c と d に関する型の定義は以下のように変わる。
1
2
3
4
5
6
7
8
9

(* 値 *)
type v = VFun of string * t * e| VCont of c list(* c が c list に *)and e = (* 前 と 同 じ *)(* 環 境 *)(* 継 続 *)and c = CApp1 of t * e(* c 型 の も の は c 型 の 要 素 を 取 ら な い よ う 変 更 *)| CApp0 of v(* も と も と c 型 の デ ー タ を 持 た な い CReset は *)| CShift(* 空 リ ス ト を 渡 す よ う 変 わ る *)and d = DRun of c list(* d 型 の も の は d 型 の 要 素 を 取 ら な い よ う 変 更 *)評価器 eval4 は以下のようになる。
1
2
3
4
5

(* identity function *)(* cid : c list *)(* did : d list *)let cid = []let did = []

6
7
8
9
10
11
12
13

(* eval : t * e * c list * d list -> v *)let rec eval (t , e , c , d ) = match t with
Var ( x ) -> run_c (c , get (x , e ) , d )| Fun (x , t ) -> run_c (c , VFun (x , t , e ) , d )| App ( t0 , t1 ) -> eval ( t1 , e , CApp1 ( t0 , e ) :: c , d )| Shift ( t ) -> eval (t , e , CShift :: c , d )| Reset ( t ) -> eval (t , e , cid , DRun ( c ) :: d )1415(* run_c : c list * v * d list -> v *)

16
17
18
19
20
21
22
23
24

and run_c (c , v , d ) = match c with
CApp1 (t ’ , e ’) :: c ’ -> eval (t ’ , e ’ , CApp0 ( v ) :: c ’ , d )| CApp0 (v ’) :: c ’ -> ( match v with
VFun (x ’ , t ’ , e ’) -> eval (t ’ , (x ’ , v ’) :: e ’ , c ’ , d )| VCont (c ’ ’) -> run_c (c ’ ’ , v ’ , DRun (c ’) :: d ))| CShift :: c ’ -> ( match v with
VFun (x ’ , t ’ , e ’) -> eval (t ’ , (x ’ , VCont (c ’)) :: e ’ , cid , d )| VCont (c ’ ’) -> run_c (c ’ ’ , VCont (c ’) , d ))| [] -> run_d (d , v )

25
26
27
28
29

(* run_d : d list * v -> v *)and run_d (d , v ) = match d with
DRun (c ’) :: d ’ -> run_c (c ’ , v , d ’)| [] -> v

30
31
32

(* eval4 : t -> v *)let eval4 t = eval (t , [] , cid , did )前述の通り、評価器の引数が c から c list、d から d list になっている。また、11, 12, 17 行目は eval3 では継続データをオブジェクト内に格納していた箇所だが、eval4 ではリストの先頭に新しい継続オブジェクトを付け加えたものを受け渡している。13 行目では CReset の代わりに空リスト (cid) を受け渡している。またこの行では、Reset 項が評価器に渡されると現在の継続のパッケージ化したものである DRun(c) が d list の先頭に積まれている。つまり reset 命令で継続が c から切り取られ d へ移されること、d はコード列のリストになることが確認できる。通常、shift/reset 処理は「reset 命令で継続に印を付け、shift 命令でその印までの継続を取り出す」という形で実装されるのに対し、ここでの実装は、「reset 命令で継続を退避させ、shift 命令では退避していない
継続を全て取り出す」という形になっている。後で触れるように、両者は相互に変換可能である。

eval3 と eval4 の違いは継続オブジェクトとその拡張時の処理だけである。 eval3 における継続オブジェクト
は木構造になっているが、どの継続オブジェクトも子要素として持てる継続オブジェクトは最大一つであるため、どれだけ木が大きくなっても eval4 の継続オブジェクトのリストと一対一の対応をとることができる。eval3 で継続オブジェクトを生成する際の拡張処理も、eval4 でリストの先頭に継続オブジェクトを付け加える処理に対応し、拡張によって継続木と継続リストの間の対応関係が崩れることはない。よって、この変換の正当性が導かれる。
定理 6.1 (線形リスト化の正当性).
任意の項 t に対し eval3 と eval4 は、どちらも評価に失敗するか、または構造的に等しい値を返す。（項 t を

eval3 で評価した結果を線形リスト化したものは、項 t を eval4 で評価した結果と等しくなる。）

7

スタック導入7.1

値をスタックに積むよう変換

これまで値は継続オブジェクト内に保持されていた。例えば、 eval4 の CApp0 は引数として v を取っている。
しかし、一般的な機械語ではスタックに中間結果を保存する。より機械語の挙動に近づけるために新たに評価器に引数としてスタックを持たせ、値をスタックに積んで受け渡すように変更し、その評価器を eval5 とする。ここで、スタックは値のリストとして実装する。また、継続オブジェクトの中に保存していた値がスタックに格納されるように変わるため、これまで継続として取り出していたものが継続オブジェクトとスタックに分離することとなる。よって、継続を取り出す際は c list だけでなくスタックも取り出さなければならない。そのため、以下のように型の定義を変更する。
1
2
3
4
5
6
7
8
9
10
11

(* 値 *)
type v = VFun of string * t * e| VCont of ( c list ) * s(* ス タ ッ ク *)and s = v listand e = (* 前 と 同 じ *)(* 継 続 *)and c = CApp1 of t * e| CApp0| CShiftand d = DRun of ( c list ) * s(* c list と ス タ ッ ク を 格 納 *)(* ス タ ッ ク は 値 の リ ス ト *)(* 環 境 *)(* 値 を 保 持 し な く な っ た *)(* c list と ス タ ッ ク と 格 納 *)

ここまでは CApp0(v) として v を受け取っていたが、この v は継続オブジェクトで保存するのではなくスタッ
クに積まれるように変わったので、以降は引数のない CApp0 になっている。また、継続の表現が c list から (clist) * s となっており、VCont や DRun の引数が変わっている。
評価器は、新しくスタック s を引数として受け渡すように変更する。それに伴い、これまで値を受け渡していた run c 関数、run d 関数でもスタックに格納されたデータを保持するために、値一つでなくスタックを受け渡すように引数を変更する。 run c 関数、run d 関数を呼び出す部分では、これまで渡していた値をスタックの先頭に積んで渡す。これらの変更により、評価器 eval5 は以下のようになる。
1234(* cid : c list *)(* did : d list *)let cid = []let did = []

5
6
7
8
9
10
11
12

(* eval : t * s * e * c * d -> v *)let rec eval (t , s , e , c , d ) = match t with
Var ( x ) -> run_c (c , get (x , e ) :: s , d )| Fun (x , t ) -> run_c (c , VFun (x , t , e ) :: s , d )| App ( t0 , t1 ) -> eval ( t1 , s , e , CApp1 ( t0 , e ) :: c , d )| Shift ( t ) -> eval (t , s , e , CShift :: c , d )| Reset ( t ) -> eval (t , [] , e , cid , DRun (c , s ) :: d )

13
14
15
16
17
18
19
20
21
22
23
24
25

(* run_c : c * s * d -> v *)and run_c (c , s , d ) = match c with
CApp1 (t ’ , e ’) :: c ’ -> eval (t ’ , s , e ’ , CApp0 :: c ’ , d )| CApp0 :: c ’ ->( match s with
VFun (x ’ , t ’ , e ’) :: v ’ :: s ’ -> eval (t ’ , s ’ , (x ’ , v ’)
| VCont (c ’ ’ , s ’ ’) :: v ’ :: s ’ -> run_c (c ’ ’ , v ’ :: s ’ ’ ,| CShift :: c ’ ->( match s with
VFun (x ’ , t ’ , e ’) :: s ’ -> eval (t ’ , [] , (x ’ , VCont (c ’ ,| VCont (c ’ ’ , s ’ ’) :: s ’ -> run_c (c ’ ’ , VCont (c ’ , s ’) ::| [] -> run_d (d , s ):: e ’ , c ’ , d )DRun (c ’ , s ’) :: d ))s ’)) :: e ’ , cid , d )s ’ ’ , d ))

26
27
28
29
30

(* run_d : d * s -> v *)and run_d (d , s ) = match (d , s ) with
( DRun (c ’ , s ’) :: d ’ , v :: s ’ ’) -> run_c (c ’ , v :: s ’ , d ’)| ([] , v :: s ’ ’) -> v

31
32
33

(* eval5 : t -> v *)let eval5 t = eval (t , [] , [] , cid , did )前述の通り、評価器及び処理系が引数としてスタック s を受け渡すようになる。8, 9 行目は eval4 では値一つを渡していた箇所だが、値をスタックに積んで渡すように変わっている。また、20, 24, 29 行目は継続を取り出して実行する箇所だが、VCont や DRun からコード列だけでなくその実行に必要なスタックも復元している。
また 29, 30 行目の、引数として受け取ったスタックの先頭を除いたもの (s’’) は、評価器が正しく作られていれば空になる。

7.2

スタック導入前後の等価性

前節ではスタック導入の直観的な説明と、スタック導入した評価器の定義を与えた。しかし、このスタック導入が妥当な変換であるかどうかは明らかではない。実際、eval4 と eval5 は値や継続の型の定義が異なっており、両者の間の単純な等価関係は構築できそうにない。そのため、本節で評価器 eval4 と eval5 が等価である
ことを bisimulation の証明によって行う。
まずは bisimulation の概念を導入する。
定義 7.1 (bisimulation [14]).

P ∼ Q となる P, Q について次の二条件が成立するとき、 ∼ は bisimulation である。
α

α0

α0

α

• P −→ P 0 となる P 0 が存在すれば、Q −→ Q0 かつ P 0 ∼ Q0 となる Q0 が存在する。
• Q −→ Q0 となる Q0 が存在すれば、P −→ P 0 かつ P 0 ∼ Q0 となる P 0 が存在する。

bisimulation は、状態遷移系の同値関係である。
eval4 と eval5 は全て末尾呼び出しになっており、引数を状態と考えることができる。例えば eval4 の 9 行目では、eval 関数に Var(x) が渡されると run c (c, get(x, e), d) が返ってくるが、これは状態 hVar(x), e4 , c4 , d4 i
が状態 hc4 , get(x, e4 ), d4 i に遷移していると見なせる。
このように eval, run c, run d の引数、そして run d の返す最終結果をそれぞれ ht, e, c, di, hc, v, di, hd, vi, hviと表記することにすると、eval4 は図 2 のような遷移規則を持つ状態遷移機械と見なすことができる。

t⇒ht, [], [], []ihVar(x), e, c, dihFun(x, t), e, c, di⇒⇒

hc, get(x, e), dihc, VFun(x, t, e), dihApp(t0, t1), e, c, dihShift(t), e, c, dihReset(t), e, c, di⇒⇒⇒ht1, e, CApp1(t0, e) :: c, diht, e, CShift :: c, diht, e, [], DRun(c) :: dihCApp1(t, e) :: c, v, dihCApp0(v) :: c, VFun(x, t, e), di⇒⇒ht, e, CApp0(v) :: c, diht, (x, v) :: e, c, dihCApp0(v) :: c, VCont(c0 ), dihCShift :: c, VFun(x, t, e), dihCShift :: c, VCont(c0 ), dih[], v, di

⇒
⇒
⇒
⇒

hc0 , v, DRun(c) :: diht, (x, VCont(c)) :: e, [], di
hc0 , VCont(c), di
hd, vihDRun(c0 ) :: d, vi⇒

hc0 , v, dih[], vi⇒hvi

図 2: eval4 の状態遷移規則

eval5 についても同様に、ht, s, e, c, di, hc, s, di, hd, si, hvi の間の、図 3 のような遷移規則を持つ状態遷移機械とみなすことができる。

t⇒ht, [], [], [], []ihVar(x), s, e, c, di⇒

hc, get(x, e) :: s, dihFun(x, t), s, e, c, dihApp(t0, t1), s, e, c, dihShift(t), s, e, c, dihReset(t), s, e, c, di

⇒
⇒
⇒
⇒

hc, VFun(x, t, e) :: s, diht1, s, e, CApp1(t0, e) :: c, diht, s, e, CShift :: c, diht, [], e, [], DRun(c, s) :: dihCApp1(t, e) :: c, s, di⇒ht, s, e, CApp0 :: c, dihCApp0 :: c, VFun(x, t, e) :: v :: s, dihCApp0 :: c, VCont(c0 , s0 ) :: v :: s, dihCShift :: c, VFun(x, t, e) :: s, dihCShift :: c, VCont(c0 , s0 ) :: s, dih[], s, di

⇒
⇒
⇒
⇒
⇒

ht, s, (x, v) :: e, c, di
hc0 , v :: s0 , DRun(c, s) :: diht, [], (x, VCont(c, s)) :: e, [], di
hc0 , VCont(c, s) :: s0 , dihd, sihDRun(c0 , s0 ) :: d, v :: sih[], v :: si⇒⇒

hc0 , v :: s0 , dihvi

図 3: eval5 の状態遷移規則
このように導き出された eval4 と eval5 の状態遷移系間の関係が bisimulation であることを証明することにより eval4 と eval5 の同値関係を示す。
そのために、eval4 と eval5 の間にどういった関係があるかをまず定義したい。ここで、eval4 での値有り継続オブジェクト c4 は、eval5 ではスタック s と値無し継続オブジェクト c5 に分離されていることに着目する。
次のような三項関係=s ⊗ を定義し、c4 =s s ⊗ c5 と書いて、 c4 はスタック導入により s と c5 に分離されることを表すことにする。記号 =s は eval4 と eval5 での状態の対応関係を意図している。

=s ⊗ ).
eval4 における状態の集合を S4 、eval5 における状態の集合を S5 とし、
ht, e4 , c4 , d4 i ∈ S4 , hc4 , v4 , d4 i ∈ S4 , ht, s, e5 , c5 , d5 i ∈ S5 , hc5 , v5 :: s, d5 i ∈ S5 とする。
定義 7.2 (三項関係このとき、 =s ⊗ を以下のように定義する。

(i) c4 = [], s = [], c5 = [] のとき、 c4 =s s ⊗ c5(ii) c4 =s s ⊗ c5 , e4 =s e5 が成り立ち、c04 = CApp14 (t, e4 ) :: c4 , c05 = CApp15 (t, e5 ) :: c5 であるとき、
c04 =s s ⊗ c05(iii) c4 =s s ⊗c5 , v4 =s v5 が成り立ち、c04 = CApp04 (v4 ) :: c4 , c05 = CApp05 :: c5 であるとき、c04 =s (v5 :: s)⊗c05(iv) c4 =s s ⊗ c5 が成り立ち、c04 = CShift4 :: c4 , c05 = CShift5 :: c5 であるとき、 c04 =s s ⊗ c05
ただし、c4 =s s ⊗ c5 のとき VCont4 (c4 ) =s VCont5 (s, c5 ), DRun4 (c4 ) =s DRun5 (c5 , s) と定義する。他の項についても、その子要素にすべて対応関係が言えれば、関係 =s が成り立つものと定義する。
定義 7.2 の (iii) において、c4 には CApp04 (v4 ) として v4 を付け加えているのに対し、c5 には CApp05 だけを付け加えていることに注意する。そのかわり v5 が s に付け加えられており、これがスタックに値を積む動作を表している。
以下、この三項関係 =s ⊗ を用いて eval4 と eval5 の状態遷移系の間にある関係 ∼s を定義し、これがbisimulation であることを示す。
定理 7.1 (スタック導入前後の bisimulation).

c4 =s s ⊗ c5 , e4 =s e5 , d4 =s d5 , v4 =s v5 を満たすとき ht, e4 , c4 , d4 i ∼s ht, s, e5 , c5 , d5 i
c4 =s s ⊗ c5 , d4 =s d5 , v4 =s v5 を満たすとき hc4 , v4 , d4 i ∼s hc5 , v5 :: s, d5 i
d4 =s d5 , v4 =s v5 を満たすとき hd4 , v4 i ∼s hd5 , v5 :: s0 i
v4 =s v5 を満たすとき hv4 i ∼s hv5 iと書く事にする。
このとき、∼s は bisimulation である。
証明. P ∈ S4 , Q ∈ S5 について、P ∼s Q が成り立つとする。
このとき各状態遷移に対して、P −→ P 0 ならば Q −→ Q0 かつ P 0 ∼s Q0 となる Q が存在することと、
eval4

eval5

Q −→ Q0 ならば P −→ P 0 かつ P 0 ∼s Q0 となる P が存在することとを示す。そのために、各状態について場合分けをし、全ての場合でこれが言えることを確かめていく。
eval5

eval4

各場合の詳細な検証は参考文献 [11] において与えている。

eval4 と eval5 の状態遷移系の間の関係が bisimulation であることが言えたので、スタック導入は妥当な変換である。
定理 7.2 (スタック導入の正当性).
任意の項 t に対し eval4 と eval5 は、どちらも評価に失敗するか、または構造的に等しい値を返す。(項 t を
eval4 で評価した結果を v4 、eval5 で評価した結果を v5 とすると、v4 =s v5 が成り立つ。)
スタック導入の正当性が厳密な形で示されたことは本研究の重要な成果の一つである。Biernacka ら [4] はス
タック導入について詳述していない。Danvy ら [7] はスタック除去前後の評価器が等価であることの直感的な説
明は行っているが、本研究で行ったような厳密な証明は行っていない。λ式のみであればそれだけで正しさを確信できるかもしれないが、shift/reset が入ると、継続の取り出し方など、直感的説明だけでは正当性の確信が難しい部分が出てくる。実際、我々が eval5 を実装する際、証明するまで見つからなかった小さな誤りが発見された。また今後、機械語による実装を視野に入れるようになると、ここで示したような厳密な証明は必須であると考えられる。

8

環境退避変換8.1

環境をスタックに積む

eval5 は関数呼び出しされると継続オブジェクト c にその時点での環境 e を格納している (10 行目) 。この評
価器の c list はコード列に相当するが、実際の機械語においては普通『環境を保存する』『環境を復帰させる』に相当するコードはあっても、コードとして環境そのものを保存することはない。よって、継続オブジェクト内に保持されていた環境もスタックに積んで受け渡すように変更し、その評価器を eval6 とする。
この変換により、これまで環境を保持していた CApp1 は環境を保持しなくなる。その代わり、スタックに環境を積むために、パッケージ化して値として扱えるよう型の定義を以下のように変更する。
1
2
3
4
5
6
7
8
9
10
11

(* 値 *)
type v = VFun of string * t * e| VCont of ( c list ) * s| VEnv of eand s = (* 前 と 同 じ *)and e = (* 前 と 同 じ *)(* 継 続 *)and c = CApp1 of t
| CApp0| CShiftand d = (* 前 と 同 じ *)(* 環 境 を 格 納 す る *)(* ス タ ッ ク *)(* 環 境 *)(* 環 境 を も た な い *)評価器は関数呼び出しの際の処理が変わる。これまでは CApp1 に格納していた環境 e を、VEnv(e) として値にパッケージ化してスタックに積むようにする。この継続は CApp1 の処理時にスタックから復帰される。よって、

eval6 の定義は以下のようになる。
1234(* cid : c list *)(* did : d list *)let cid = []let did = []

5
6
7
8
9
10
11
12

(* eval : t * s * e * c list * d list -> v *)let rec eval (t , s , e , c , d ) = match t with
Var ( x ) -> run_c (c , get (x , e ) :: s , d )| Fun (x , t ) -> run_c (c , VFun (x , t , e ) :: s , d )| App ( t0 , t1 ) -> eval ( t1 , VEnv ( e ) :: s , e , CApp1 ( t0 ) :: c , d )| Shift ( t ) -> eval (t , s , e , CShift :: c , d )| Reset ( t ) -> eval (t , [] , e , CReset :: [] , DRun (c , s ) :: d )

13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

(* run_c : c list * s * d -> v *)and run_c (c , s , d ) = match c with
CApp1 (t ’) :: c ’ ->( match s withv :: VEnv (e ’) :: s -> eval (t ’ , v :: s , e ’ , CApp0 :: c ’ , d ))| CApp0 :: c ’ ->( match s with
VFun (x ’ , t ’ , e ’) :: v ’ :: s ’ -> eval (t ’ , s ’ , (x ’ , v ’) :: e ’ , c ’ , d )| VCont (c ’ ’ , s ’ ’) :: v ’ :: s ’ -> run_c (c ’ ’ , v ’ :: s ’ ’ , DRun (c ’ , s ’) :: d ))| CShift :: c ’ ->( match s with
VFun (x ’ , t ’ , e ’) :: s ’-> eval (t ’ , [] , (x ’ , VCont (c ’ , s ’)) :: e ’ , CReset :: [] , d )| VCont (c ’ ’ , s ’ ’) :: s ’ -> run_c (c ’ ’ , VCont (c ’ , s ’) :: s ’ ’ , d ))| CReset :: _ -> run_d (d , s )

29
30
31
32
33

(* run_d : d list * s -> v *)and run_d (d , s ) = match (d , s ) with
( DRun (c ’ , s ’) :: d ’ , v :: s ’ ’) -> run_c (c ’ , v :: s ’ , d ’)| ( DReset :: _ , v :: s ’ ’) -> v

34
35
36

(* eval6 : t -> v *)let eval6 t = eval (t , [] , [] , cid , did )前述の通り、App 項の処理（10 行目）で環境が VEnv にパッケージ化されスタックに積まれた上で、実行は t1

へ進む。t1 の実行が終了し、CApp1(t0) に結果が渡されると、その時点でのスタックには先頭に t1 の実行結果、
その下に先程保存した環境が積まれている筈である（16〜18 行目）。その後の実行は、保存されていた環境を復活してから行われる。
この変換の結果、継続オブジェクトは項 (t) 以外のデータを持たなくなる。これは、項さえ与えられればコード列を生成できることを意味する。また、これにより後に使う変数の退避・復活をモデル化できていると考えられる。

8.2

環境退避変換前後の等価性

eval5 について、eval, run c, run d の引数及び run d の返す最終結果をそれぞれ ht, s, e, c, di, hc, s, di, hd, si, hviと表現し、eval5 はこの状態の間を遷移する状態遷移機械と見なすことができるということは 7.2 節で述べた。

eval6 も全て末尾呼び出しになっているため、同様に ht, s, e, c, di, hc, s, di, hd, si, hvi の間を遷移する、図 4 のよ
うな遷移規則を持つ状態遷移機械と見なすことができる。
t⇒ht, [], [], [], []ihVar(x), s, e, c, dihFun(x, t), s, e, c, dihApp(t0, t1), s, e, c, dihShift(t), s, e, c, di

⇒
⇒
⇒
⇒

hc, get(x, e) :: s, dihc, VFun(x, t, e) :: s, diht1, VEnv(e) :: s, e, CApp1(t0) :: c, diht, s, e, CShift :: c, dihReset(t), s, e, c, di⇒ht, [], e, [], DRun(c, s) :: dihCApp1(t) :: c, v :: VEnv(e) :: s, dihCApp0 :: c, VFun(x, t, e) :: v :: s, dihCApp0 :: c, VCont(c0 , s0 ) :: v :: s, dihCShift :: c, VFun(x, t, e) :: s, di

⇒
⇒
⇒
⇒

ht, v :: s, e, CApp0 :: c, diht, s, (x, v) :: e, c, di
hc0 , v :: s0 , DRun(c, s) :: diht, [], (x, VCont(c, s)) :: e, [], dihCShift :: c, VCont(c0 , s0 ) :: s, dih[], s, di⇒⇒

hc0 , VCont(c, s) :: s0 , dihd, sihDRun(c0 , s0 ) :: d, v :: si⇒

hc0 , v :: s0 , dih[], v :: si⇒hvi

図 4: eval6 の状態遷移規則
この状態遷移系間の関係が bisimulation であることを証明することにより eval5 と eval6 の間の同値関係を示す。
そのために、環境退避変換によって状態遷移系がどう変わったかを明確に記述する必要がある。ここで、eval5では c に保持されていた環境が eval6 ではスタックに積まれることと、環境保持、復元処理以外は変化がない
ことに着目し、eval5 のスタック s5 , コード列 c5 , eval6 のスタック s6 , コード列 c6 の間の四項関係を定義する。環境退避変換によって c5 に保持されていた環境がスタックに積まれるよう変わり、スタックが s6 , コード列が c6 になることを、 s5 ⊗ c5 =e s6 ¯ c6 と書き表すとする。記号 =e は eval5 と eval6 の間の対応関係を意図している。

⊗ =e ¯ ).
eval5 における状態の集合を S5 、eval6 における状態の集合を S6 とし、
ht, s5 , e5 , c5 , d5 i ∈ S5 , hc5 , v5 :: s5 , d5 i ∈ S5 , ht, s6 , e6 , c6 , d6 i ∈ S6 , hc6 , v6 :: s6 , d6 i ∈ S6 とする。
定義 8.1 (四項関係このとき、 ⊗ =e ¯ を以下のように定義する。

(i) s5 = [], c5 = [], s6 = [], c6 = [] のとき、 s5 ⊗ c5 =e s6 ¯ c6(ii) s5 ⊗ c5 =e s6 ¯ c6 が成り立ち、かつ e5 =e e6 となるとき、c05 = CApp15 (t, e5 ) :: c5 , c06 = CApp16 (t) :: c6であるとき、 s5 ⊗ c05 =e (VEnv(e6 ) :: s6 ) ¯ c06(iii) s5 ⊗ c5 =e s6 ¯ c6 が成り立ち、c05 = CApp05 :: c5 , c06 = CApp06 :: c6 であるとき、 (v5 :: s5 ) ⊗ c05 =e (v6 ::s6 ) ¯ c06

(iv) s5 ⊗ c5 =e s6 ¯ c6 が成り立ち、c05 = CShift5 :: c5 , c06 = CShift6 :: c6 であるとき、 s5 ⊗ c05 =e s6 ¯ c06
さらに、s5 ⊗ c5 =e s6 ¯ c6 のとき VCont5 (c5 , s5 ) =e VCont6 (c6 , s6 ), DRun5 (c5 , s5 ) =e DRun6 (c6 , s6 ) と定義する。他の項についても、その子要素が全て等しければ、関係 =e が成り立つものと定義する。
定義 8.1 の (ii) において、c5 には CApp15 (t, e5 ) を付け加えているのに対し、c6 には CApp16 (t) だけを付け加えていることに注意する。そのかわり VEnv(e6 ) が s6 に付け加えられており、これがスタックに環境を積む動作を表している。

⊗ =e ¯ を用いて eval5 と eval6 の状態遷移系間の関係を定義し、それが bisimulation であることを示す。
四項関係

定理 8.1 (環境退避前後の bisimulation).

s5 ⊗ c5 =e s6 ¯ c6 , e5 =e e6 , d5 =e d6 , v5 =e v6 を満たすとき ht, s5 , e5 , c5 , d5 i ∼e ht, s6 , e6 , c6 , d6 i
s5 ⊗ c5 =e s6 ¯ c6 , d5 =e d6 , v5 =e v6 を満たすとき hc5 , v5 :: s5 , d5 i ∼e hc6 , v6 :: s6 , d6 i
d5 =e d6 , v5 =e v6 を満たすとき hd5 , v5 :: s5 i ∼e hd6 , v6 :: s6 i
v5 =e v6 を満たすとき hv5 i ∼e hv6 iと書く事にする。
このとき、∼e は bisimulation である。
証明. P ∈ S5 , Q ∈ S6 について、P ∼s Q が成り立つとする。
このとき各状態遷移に対して、P −→ P 0 ならば Q −→ Q0 かつ P 0 ∼s Q0 となる Q が存在することと、
eval5

eval6

Q −→ Q0 ならば P −→ P 0 かつ P 0 ∼s Q0 となる P が存在することとを示す。定理 7.1 の証明と同様、各状態について場合分けをし、全ての場合でこれが言えることを確かめていく。
eval6

eval5

各場合の詳細な検証は参考文献 [11] において与えている。

eval5 と eval6 の状態遷移系の間の関係が bisimulation であることが言えたので、環境退避変換は妥当な変換である。
定理 8.2 (環境退避変換の正当性).
任意の項 t に対し eval5 と eval6 は、どちらも評価に失敗するか、または構造的に等しい値を返す。(項 t を

eval5 で評価した結果を v5 、eval6 で評価した結果を v6 とすると、v5 =e v6 が成り立つ。)
環境退避変換の正当性が示されたことにより、機械語の実装に見られる局所変数の退避、復活が、言語の定義を与える CPS インタプリタ（3 節）と等価であることが厳密に示された。従来、Danvy らの系統的な抽象機械
導出法は抽象機械や仮想機械のレベルまでととらえられていたが、ここでの結果は、それが実際の機械語レベルまで拡張可能であることを示している。shift/reset のような複雑な操作が入った体系では、機械語レベルの正当性を示すのが重要であるが、ここでの結果はそれに道を開くものとなっている。

9

抽象機械
評価器 eval6 は全て末尾呼び出しになっており、引数をそのまま状態だと見なすと遷移規則を得られる。よってこれまでの変換の結果、図 4 のような状態遷移規則を持つ抽象機械が得られたことになる。
この抽象機械は項 t, スタック s, 環境 e, 継続（コード列） c, 継続（コード列）リスト d を状態として持ち、Landin の SECD マシン [12] に類似しているが、• 関数呼び出し時に環境をスタックに積む• shift/reset 機能をサポートしているの二点において異なる。
前者は、機械語による関数呼び出しの動作をほぼ模倣できていると考えられる。実際、機械語による関数呼び出しでは、後に使う可能性のあるレジスタの中身をスタックに退避させるが、ここで得られた抽象機械はほぼ同様のことを行っている。具体的には t1 を実行する際、後に t0 を実行するときに必要な値（環境に格納されている値）をスタックに退避させている。通常の関数呼び出しでは、関数呼び出し自体の前後でレジスタの退避復活

を行うが、ここでの結果は、部分式 t1 を実行する際（そしてそのときのみ）に退避復活をすれば良いことを示している。
また、後者についても機械語による shift/reset の実装を模倣できていると考えられる。実際、 s@d ( s と d を

append したもの) が機械語実装でのスタックに相当すると考えれば、@ の位置がリセットの位置になり、 shiftで最も近い reset までの継続を取り出せる。また、CShift の実行（抽象機械の下から四つ目の規則）によって、そのときのスタックとコードを VCont に入れているが、前者はスタックの内容をヒープにコピーすることに相当
し、後者は継続のコードを表す番地を保存することに相当する。これは、ちょうど機械語の実装で継続を表すク
ロージャを生成 [13] することに対応している。よって、shift 命令によってスタックがヒープにコピーされることが抽象機械でモデル化できているといえる。この抽象機械は前述の通り、shift/reset の定義に従った実装から妥当性を検証した変換のみを用いて導出したものであるため、その正当性が保証されている。つまり、shift によるスタックコピーに対して、正当性の保証されたモデルが導かれたといえる。
ただし、現段階ではスタック s は値 v のリストとして実装されており、この v が VCont(c, s) となるかもしれず、自己参照が起こる可能性が排除できない。そのため、実際の機械上での実装において、スタックを元のアドレスと異なる場所に復元する際、自己参照のアドレスを修正しながら複写しなければならなくなり、自明でない操作が要求される。この問題に対しては、VCont におけるスタックへの参照を先頭からの index で行うことにした上でその透明性を証明することで解決できると思われる。

10

まとめと今後の課題

本論文では、shift/reset を定義に基づいて実装したインタプリタに CPS 変換、非関数化、線形化、スタック
導入、環境退避変換を施してスタックに値を退避するインタプリタを得られることを示した。CPS 変換、非関数化は先行研究によって既にその妥当性が検証済みであり、それ以外の変換の妥当性については本論文内で検証を行った。そして、このインタプリタから項 t, スタック s, 環境 e, 継続（コード列） c, 継続（コード列）リスト dを状態として持ち、shift/reset 命令をサポートする抽象機械の状態遷移規則が得られることを示した。
この抽象機械は Landin の SECD マシンに類似しているが、shift/reset が実装されている点と、環境を退避す
る点において異なる。後者は実際の機械語実装を模倣したためである。shift/reset についても shift によるスタッ
クコピーと reset によるコピー範囲の限定がモデル化されたものとなっている。
今後、ここでの結果をもとに、さらに厳密に機械語による shift/reset の実装の正当性を確立していく予定である。現段階で得られている抽象機械は shift/reset の挙動を忠実に表しているが、まだインタプリタ実行の形である。今後、この抽象機械を Ager [1] らの手法に従って分割し、コンパイラと仮想機械の抽出を試みる予定である。
本論文で得られた抽象機械では継続オブジェクトが項以外のデータを保持しないため、項さえ与えられれば継続（コード列）を生成することができるはずである。よって、抽象機械を「項を受け取ってコード列を返す」部分と「コード列、スタック、環境、継続を受け取って値を返す」部分に分割する。後者が前者に依存しないように分割できれば、前者をコンパイラ、後者を仮想機械と見なせる。本研究では、この方向を追求するとともに、分割時
及び分割後に施す変換について、その妥当性の検証を与えながら行う。
具体的に施す変換としては、まずはカリー化が挙げられる。カリー化により、評価器が項を評価する部分とそ
れ以降に分割される。ただしカリー化しただけでは高階関数を生成するようになるため、非関数化を行う。すると命令オブジェクト i の型とその処理系が新たに定義される。この命令オブジェクトが仮想機械の命令列、処理系が仮想機械である。さらに i に対し線形リスト化等の変換を施していき、より低レベルな言語と対応がとりや
すいものにしていく。予備的な考察では、shift/reset が入っても問題なくコンパイラ及び仮想機械が得られる見通しである。
最終的には、アセンブラでの実装と対応がとれる仮想機械を得て、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 RS-03-14, BRICS, Aarhus, Denmark (March 2003).

[2] M. S. Ager, D. Biernacki, O. Danvy, and J. Midtgaard: “A Functional Correspondence between Evaluators
and Abstract Machines,” Technical Report RS-03-13, BRICS, Aarhus, Denmark (March 2003).
[3] K. Asai, and Y. Kameyama: “Polymorphic Delimited Continuations,” Proceedings of the Fifth Asian
Symposium on Programming Languages and Systems (APLAS’07), LNCS 4807, pp. 239–254 (November2007).
[4] M. Biernacka, D. Biernacki, and O. Danvy “An Operational Foundation for Deliminated Continuations in
the CPS Hierarchy,” Logical Methods in Computer Science, Vol. 1 (2:5), pp. 1-39 (November 2005).
[5] O. Danvy, and A. Filinski: “A Functional Abstraction of Typed Contexts,” Technical Report 89/12, DIKU,
University of Copenhagen (July 1989).
[6] O. Danvy, and A. Filinski: “Abstracting Control,” Proceedings of the 1990 ACM Conference on Lisp andFunctional Programming, pp. 151–160 (June 1990).
[7] O. Danvy, and K. Millikin: “A Rational Deconstruction of Landin’s J Operator,” Technical Report RS06-17, BRICS, Aarhus, Denmark (December 2006).
[8] M. Felleisen: “The Theory and Practice of First-Class Prompts,” Conference Record of the 15th Annual
ACM Symposium on Principles of Programming Languages, pp. 180–190 (January 1988).
[9] A. Filinski: “Representing Monads,” Conference Record of the 21st Annual ACM Symposium on Principles
of Programming Languages, pp. 446–457 (January 1994).
[10] A. Igarashi and M. Iwaki: “Deriving Compilers and Virtual Machines for a Multi-Level Languages,”
Proceedings of the Fifth Asian Symposium on Programming Languages and Systems (APLAS’07), LNCS
4807, pp. 206–221 (November 2007).
[11] 木谷有沙、浅井健一「限定継続を含む仮想機械導出のためのプログラム変換」お茶の水女子大学理学部情報科学科テクニカルレポート OCHA-IS 08-3 (February 2009).

[12] P. J. Landin: “The mechanical evaluation of expressions,” The Computer Journal, Vol. 6, No. 4, pp. 308–
320, (1964).
[13] 増子萌、浅井健一「MinCaml コンパイラにおける shift/reset の実装」第 11 回プログラミングおよびプログ
ラミング言語ワークショップ (March 2009).
[14] R. Milner: “Communication and Concurrency” Prentice Hall International Series in Computer Science,(1995).
[15] G. D. Plotkin: “Call-by-name, call-by-value, and the λ-calculus,” Theoretical Computer Science, Vol. 1,
No. 2, pp. 125–159 (December 1975).
[16] J. C. Reynolds: “Deﬁnitional Interpreters for Higher-Order Programming Languages,” Proceedings of the
ACM National Conference, Vol. 2, pp. 717–740, (August 1972), reprinted in Higher-Order and Symbolic
Computation, Vol. 11, No. 4, pp. 363–397, Kluwer Academic Publishers (December 1998).
[17] M. Sperber, R. K. Dybvig, M. Flatt, A. van Straaten: “Revised6 report on the algorithmic language
Scheme”, http://www.r6rs.org/ (2007).