限定継続命令 shift/reset の Selective CPS 変換
理学専攻 情報科学コース

1

上原 千裕 (指導教員：浅井 健一)

はじめにの実行中に shift が起こる可能性があることを示す.
Sk. A は shift 命令である. これで現在の継続を切り取って k に入れた上で A を行うことを示す. また ⟨A⟩は reset 命令である. これで, A の中で起こる shift で切り取られる継続を A までに限定する. 例えば,継続とは, 計算中のある時点における残りの計算を表す. 継続の中でも限定継続は, 一定範囲内のみの残りの計算を表す. shift/reset [2] は限定継続を扱うことができるオペレータで, shift はその時点での継続を切り取ってくる命令, reset は切り取られる継続の範囲を限定する命令である. 限定継続命令を使うと, ユーザがプログラムの実行順序を制御できるため, 例外処理や非決定プログラミングなど色々な場面で使われる.
これまで, 限定継続命令をサポートするには, システムに手を加えて直接実装する方法が多くとられてきた. 一方プログラム全体を CPS 変換すれば, 限定継続命令を使うことができるようになるが, 多くの場合効率が落ちる. しかし, shift/reset に関係した部分のみを selective に CPS 変換 [4] すれば, 効率を落とすことなく限定継続命令をサポートできる可能性がある.
本研究では, 関数型言語を対象にした, selective にCPS 変換を行うシステムを提案する. 最初に「CPS変換を必要とするか」という情報を型システムの制約の形で表現する. 制約解消は通常「最も良い解」を得られるように行うが, ここで扱う制約の解には「最も良い解」が必ずしも存在するとは限らない. 本研究では, 過度に型推論と制約解消を複雑にすることなく, ある程度の解を得られる制約解消法を提案する. 解が得られたら, CPS 変換が必要な場所が特定されるので,その情報に従って selective に CPS 変換を行う. また
簡単なプログラムで実際に selective CPS 変換を行い,selective に CPS 変換することで効率が向上することを確認した.

2⟨(Sk. k @ 2) − 1⟩
は, Sk. k @ 2 を実行する時, 計算結果から 1 を引くことが継続である. この式では, λx. ⟨x − 1⟩ を k に入れて,⟨(λx. ⟨x − 1⟩) @ 2⟩という式になる. 後は関数適用が実行されて, 1 が返る. また string of int を, int を string に変える関数であるとして,⟨(Sk. string of int (k @ 2)) − 1⟩という式を考える. この式は実行すると⟨string of int ((λx. ⟨x − 1⟩) @ 2)⟩となるため, (λx. ⟨x − 1⟩) @ 2 の結果である int の 1 がstring になって返る. この時, reset の中身が返す型を考える.

(Sk. string of int (k @ 2)) − 1は引き算であるから int を返す予定だったが, 実際はstring を返した. このような, reset の中身が返す型
を answer type と呼ぶ. この例では, shift 命令によりanswer type が int から string に変化した.
関数の型は (t1 → t2 @cps[t3 , t4 , α]) という形になる.
これで大雑把には「t1 を受け取ったら t2 を返す関数」を意味するが, この関数を実行すると answer type がt3 から t4 へ変化し, この関数の本体部分の注釈は α であることを示す. この α が ϵ なら, この関数の本体はpure であり, i なら impure であることを示す.

対象言語, 注釈, 型規則

本稿で扱うのは, let 多相の入った λ 計算に整数, 真偽値と if 文, 不動点演算子 fix, そして限定継続命令shift/reset が加わった言語であり, 定義は以下である.

α::=t ::=ϵ|iannotation

τ | bool | int | t1 → t2 @cps[t3 , t4 , α]2.2monomorphic type

対象言語の型規則を定義した. その一部として型規則 fun は以下である. ただし

T::=t | ∀τ.Tv::=n | x | true | false | λα x.A | fixα f.x.A valuee ::=polymorphic type

2.1

t′ = (t1 → t2 @cps[t3 , t4 , α1 ])v | A1 @α A2 | Sk.A | ⟨A⟩ | let x = v ϵ in A| if A1 then A2 else A3

A ::=型規則eαとする.

expression(α2 ≤ α1 ) (t3 ̸= t4 ⇒ α2 = i)expression with annotation

Γ, x ϵ : t1 ⊢ e α2 : t2 @cps[t3 , t4 , α2 ]fun
Γ ⊢ (λα1 x.e α2 ) ϵ : t′ @cps[t5 , t5 , ϵ]

対象言語と注釈

α は「CPS 変換が必要かどうか」を示す注釈である.
また, A = eα は式 e に注釈 α が付いた式を示す. 注釈
ϵ は CPS 変換が不要であることを示す. CPS 変換が不要な場合, つまり shift によるコントロールエフェクトが起きない場合は, その式は pure である, という表現を使う. 一方, 注釈 i は CPS が必要であることを示す.
そのような式は impure であるという. これはその式

関数の本体部分の注釈 α2 と返される関数の型の注釈
α1 の間に, (α2 ≤ α1 ) という制約がある. これは, 関数本体が impure なら関数の型も impure になることを示している. (α2 = α1 ) ではなく (α2 ≤ α1 ) となっているのは, 関数本体が pure でも, 周りの状況によってその関数を impure と扱いたい場合があるためである.

1

この型規則は, 基本的には Asai and Kameyama [1]の型規則に注釈と制約を加えたものである.
型判断は,変換する selective CPS 変換を定義した. 注釈付きの式の型規則は注釈を無視した簡約規則のもとで subjectreduction を満たすことを示すことができる. Pure な式 e ϵ に対する selective CPS 変換を ∥ e ϵ ∥p , impureな式 e i に対する selective CPS 変換を ∥ e i ∥ とすると, 以下の定理が満たされる. ただし, E は CPS 変換
後の式の任意の評価文脈とする.

Γ ⊢ e α : t1 @cps[t2 , t3 , α]の形をしている. これは, 型環境 Γ のもとで式 e α は型t1 を持ち, answer type を t2 から t3 に変え, 注釈 α を持つことを意味する. 注釈 α は式 e が pure か impureかを示す. 式 e に付く注釈 α は, answer type に付く注
釈 α と一致する.
制約は以下の３種類からなる.

( = )

( ≤ )

定理 4.1⇒∥ e ϵ ∥p →∗ ∥ v ϵ ∥p

これは, 注釈のついたプログラムの実行結果と selectiveCPS 変換後のプログラムの実行結果が対応することを示している. この定理は, Danvy and Filinski [3] の証
明に沿った形で示すことができる.

(i = i)(ϵ ≤ i)(t1 ̸= t1 ⇒ ϵ = i)(i ≤ i)(t1 ̸= t2 ⇒ i = i)5

実行例

N-Queen 問題を解く簡単なプログラムで selective
CPS 変換を行った. このプログラムはバックトラックを shift/reset を使って実装している. Selective に CPS変換することで, プログラム全体を CPS 変換したものに比べて, 約 28% ほどの実行時間の改善が見られた.

制約 (α ≤ α′ ) は, α が i なら α′ も i にならなければならず, α′ が ϵ なら α も ϵ にならなければならないことを示す. ϵ と i の間には, ϵ < i の大小関係がある.
最後の制約は型規則では, 最初の２つには型が入り(t1 ̸= t2 ⇒ α = i)

6まとめ

本稿では shift/reset を含むプログラムの selective
CPS 変換を定義した. 具体的には以下を行った.という形になる. これで, t1 と t2 が異なる型ならば αは i にならなければならないことを示す. 逆に, α が ϵにならば, t1 と t2 は同じであると解釈しても良い.
型規則の前提部に @cps[t1 , t2 , α] が出てくる度に(t1 ̸= t2 ⇒ α = i) という制約が加わっている. これで, answer type が変わるなら α は i になり, α が ϵ なら t1 = t2 となることを示している.

• 型と式に注釈を含む型規則を定義した• 型推論で生成された制約に対する制約の解消法を定義した. これは, 過度に型推論と制約解消を複雑にしないである程度の解を得られるものである• 注釈が付いた項の selective CPS 変換を定義した

制約解消

今のところ, 本稿で定義した制約解消法で, 一般的なプログラムには良い注釈が付いている. しかし, 我々は限られたプログラムしか考察できていない. そのため,現在の制約解消法よりも強力なものが必要なプログラ
ムを探すことは, 今後の課題である.

入力の式を与えられたら, まず型規則に従って型推論を行う. その際, 注釈と制約はそのまま保持する. 注
釈と制約を除けば型規則はこれまでの規則とほぼ同一なので, 普通の let 多相の入った型推論をすれば良い.
その結果, 入力の各式にはユニークな注釈の変数が割り振られ, それに対する制約が生成される.
制約に対する解とは, 全ての注釈の変数に対する注釈の割り当てのうち, 全ての制約を満たしているものである. 生成された制約に対して, 全ての注釈に i を入れると解になっている. これは直感的には, 全ての式を CPS 変換することが, 解の１つであるということを意味する. 従って, 解は必ず１つは存在することが分かる. 本稿の制約解消の目標は, なるべく小さい解,つまりなるべく ϵ が多い解を見つけることである.
しかし, なるべく小さい解を求めるのは簡単ではな
い. 一般には「最良の解」は存在しないことが分かっている. 本研究では, 型推論と制約解消を過度に複雑にすることのない範囲での制約解消を提供する. 制約解消規則は, この修論要旨には載せない.

4⊢ e ϵ : t1 @cps[t2 , t2 , i] ∧ e i →∗ v ϵ( ̸= ⇒ = i)(ϵ = ϵ)3⇒∥ e i ∥ @ (λx. E[x]) →∗ E[∥ v ϵ ∥p ]これらの制約が満たされる場合は以下である.

(ϵ ≤ ϵ)⊢ e ϵ : t1 @cps[t2 , t2 , ϵ] ∧ e ϵ →∗ v ϵ

参考文献[1] Asai, K. and Kameyama, Y.: Polymorphic Delimited Continuations, 5th Asian Symposium on Programming Languages and Systems (APLAS 2007),
pp.239–254, 2007
[2] Danvy, O. and Filinski, A.: Abstracting control,the 1990 ACM Conference on Lisp and Functional
Programming, pp.151–160, 1990
[3] Danvy, O. and Filinski, A.: Representing Control : a Study of the CPS Transformation, Mathematical Structures in Computer Science, Volume2, Issue 4, pp.361–391, 1992
[4] Nielsen, L. R.: A Selective CPS Transformation,
BRICS Research Report RS-01-30, Department ofComputer Science, Aarhus University, 2001

Selective CPS 変換

制約解消が済み, 式の各部に ϵ か i の注釈が付いたら, それに従って i の注釈が付いている箇所のみ CPS

2