shift/reset の selective CPS 変換
上原 千裕, 浅井 健一
お茶の水女子大学
g1120506@is.ocha.ac.jp, asai@is.ocha.ac.jp
概 要
shift/reset は限定継続を処理するオペレータであり, 非決定性プログラミングなど様々な目的で使われる. しかし, shift/reset を直接サポートしている言語は少ない.
shift/reset をサポートしていない言語で shift/reset を使うには, プログラム全体を CPS変換するという方法があるが, 多くの場合, CPS 変換すると効率は落ちる. そこで, 本稿
では shift/reset を実装するのに必要な部分のみを, システムが自動で特定して CPS 変換
する selective CPS 変換を提案する. Selective に CPS 変換することで, shift/reset に無関係な部分の効率を落とすことなく shift/reset を使うことができるようになる.

1

はじめに

継続とは, 計算中のある時点における残りの計算を表す. 継続の中でも限定継続は, 一定範囲内のみの残りの計算を表す. shift/reset [3] は限定継続を扱うことができるオペレータで, shift はその時
点での継続を切り取ってくる命令, reset は切り取られる継続の範囲を限定する命令である. 限定継続命令を使うと, ユーザがプログラムの実行順序を制御できるため, 例外処理や非決定プログラミン
グなどいろいろな場面で使われる.
これまで, 限定継続命令をサポートするには, システムに手を加えてスタックを操作できるようにすることで直接実装する方法が多くとられてきた. Scheme 上での直接実装 [6], OCaml の Delimcc
ライブラリ [8], Caml Light を拡張した OchaCaml [10] などはこのアプローチをとっている. 一方,
ユーザプログラム全体を CPS 変換して既存の言語の上で shift/reset を使うという選択肢がある. この選択肢は, システムに手を自力で加えることや, shift/reset を使うために新しい言語を手元に用意することなく, shift/reset が使えるという利点がある. しかし, ユーザプログラム上の CPS 変換は,多くの場合効率が落ちる. ここで, shift/reset に関係した部分のみを選んで変換, つまり selective に
CPS 変換 [11] すれば, 効率を落とすことなく限定継続命令をサポートできる可能性がある.
本稿では, 関数型言語を対象にした, selective に CPS 変換するシステムを提案する. このシステム
では, 「式の評価中に shift が行われる可能性があるか」, つまり「CPS 変換を必要とするか」という情報を型システムの制約の形で表現する. 具体的には, 以下の手順で selective に CPS 変換を行う.

1. 型推論を行う. この時, 制約は保存しておく.
2. 制約を解くことにより, 「CPS 変換を必要とするか」という情報を注釈として式に付ける.
3. 解が得られたら CPS 変換が必要な場所が特定されるので, その情報に従って CPS 変換が必要な場所だけ選んで, つまり selective に CPS 変換を行う.
ユーザの視点からこのシステムを見ると, ユーザは注釈なしのプログラムをシステムに入力する. するとシステムが注釈を自動で式に付け, プログラムを selective に CPS 変換する. 得られたプログラムは shift/reset を含まないため, 既存の処理系で実行できる.
ここで, 制約解消は通常「最も良い解」を得られるように行うが, 本研究で扱う制約の解には「最も良い解」が必ずしも存在するとは限らないことを後に示す. その上で本稿では, 過度に型推論と制約解消を複雑にすることなく, ある程度の解を得られる制約解消法について述べる.

1

意味論と解き方と証明

1型, 値, 項α ::= ϵ | iannotationt ::= τ | bool | int | t1 → t2 @cps[t3 , t4 , α]T::= t | ∀τ.T

monomorphic type

polymorphic typev ::= n | x | true | false | λα x.A | fixα f.x.A

value

e ::= v | A1 @α A2 | Sk.A | ⟨A⟩ | if A1 then A2 else A3 | let x = v ϵ in A

A ::= eαexpression

expression with annotation

制約

図 1. 対象言語(ϵ = ϵ)(i = i) shift/reset(ϵ ≤ ϵ) を実装するのに必要な部分を(ϵ ≤ i)(i ≤ i)
なお, Scala では, ユーザの注釈に従って
selective に CPS変換するという方法 [13] がとられている, ユーザが注(t1 ̸= t1 ⇒. ϵ これに対して本研究が提案するシステムは= i)(t1 ̸= t2 ⇒ i = i)
釈をプログラムに付ける必要はなく, システムが自動で注釈を付ける(α1 ̸= α(α1 ̸= α2 ⇒ i = i).
1 ⇒ ϵ = i)
また, SML/NJ [1] のように, 内部表現として CPS を使ったコンパイラであれば, コンパイラに手を加えることで比較的容易に shift/reset をサポートできると思われるが, ここでは OCaml のよう
評価文脈に内部表現として CPS を使っていない言語を対象としている.
本稿は, 第 2 節で本稿の対象言語と注釈を定義する. 定義した型規則に沿って型推論をするが, 注
E α ::= [ ] ϵ | (E α1 @α2 A) α3 | (v ϵ @α2 E α1 ) α3 | (if E α1 then A1 else A2 ) α2 | ⟨E α ⟩ ϵe-context
釈を決定するための制約が発生する. 2 そのため制約解消法を第3 節で定義する. そして注釈が付いた
ϵ
α
α
α
α
ϵ
α
α
α
α
α
1
2
3
1
3
1
2
F ::= [ ] | (F @ A) | (v @ F ) | (if F
then A1 else A2 )pure e-context
プログラムのための selective CPS 変換を第 4 節で定義する. 第 5 節で, 成果として簡単なプログラ
ムで実際に selective CPS 変換を行い, selective に CPS 変換することで効率が向上することをみる.
簡約規則
第 6 節でライブラリ関数を導入する方法を提案する. 第 7 節で関連研究, 第 8 節でまとめを述べる.
((λα1 x.e α2 ) ϵ @α1 v ϵ ) α32

2 ϵ((fixα1 f.x.e) @α1 v ϵ ) α3
注釈, 対象言語, α型規則→ (e α2 [v ϵ /x]) α2→ (e α2 [(fixα2 f.x.e α2 ) ϵ /f ][v ϵ /x]) α2⟨v ϵ ⟩ ϵ → v ϵ
本稿で扱うのは, let 多相の入った λ 計算に整数, 真偽値と if 文, 不動点演算子 fix, そして限定継ϵϵ
α2α2 ϵ ϵ ϵ⟨(F α2 [(Sk.e α1 ) i ]) i ⟩ . その定義を図→ ⟨(let k =1 (λx.⟨F[x ]⟩ ) ,ine α1 ) α1 ⟩, x は変数,
続命令 shift/reset が加わった言語であるに示す. τ は型変数
n は整数(if
trueのϵ kthen
A1 else A. 2 ) α1 → A1
shift を表す
Sk.A
は変数である2.1(if false ϵ then A1 else A2 ) α1

注釈と対象言語→ A2(let x = v ϵ in e α1 ) α1 → (e α1 [v ϵ /x]) α1
α は「式の評価中に shift が行われる可能性があるか」, つまり「CPS 変換が必要かどうか」を示す注釈である. また, A = eα は式 e に注釈 α が付いた式を示す. 注釈 ϵ は CPS 変換が不要であることを示す. CPS 変換が不要な場合, つまり shift によるコントロールエフェクトが起きない場合は,その式は pure である, という表現を使う. 一方, 注釈 i は CPS が必要であることを示す. そのよう1
な式は impure であるという. これはその式の実行中に shift が起こる可能性があることを示している. また, 注釈 i は impure の頭文字からとっている.
多相の let 文は value restriction を仮定して束縛される式は常に v としている. 値でない e における let x = e α in A は, 内部的に (λx. A) @ e α と扱う.
Sk. A は shift 命令である. これで現在の継続を切り取って k に入れた上で A を行うことを示す.
また ⟨A⟩ は reset 命令である. これで, A の中で起こる shift で切り取られる継続を A までに限定する. 以下で例を示すが, 注釈は省略している. これは, 注釈を無視した簡約規則が, 注釈付きの式に対する簡約規則であり, 簡約の本質的な意味に注釈は関係無いからである.

⟨(Sk. k @ 2) − 1⟩
は, (Sk. k @ 2) を実行する時, 計算結果から 1 を引くことが継続である. この式では, λx. ⟨x − 1⟩ をk に入れて,⟨(λx. ⟨x − 1⟩) @ 2⟩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 に変化している. このことを answer type modification という.
関数の型は (t1 → t2 @cps[t3 , t4 , α]) という形になる. これで大雑把には「t1 を受け取ったら t2 を返す関数」を意味するが, この関数を実行すると answer type が t3 から t4 へ変化し, この関数の本
体部分の注釈は α であることを示す. この α が ϵ なら, この関数の本体は pure であり, i なら impureであることを示す.

2.2

型規則

型規則を図 2 に示す. この型規則は, Asai and Kameyama [2] の型規則に注釈と制約を加えたものである. 厳密には, Asai and Kameyama [2] の型規則とは異なる点があるが, それについては第2.3 節で説明する.
型判断は,Γ ⊢ e α : t1 @cps[t2 , t3 , α]の形をしている. これは, 型環境 Γ のもとで式 e α は型 t1 を持ち, answer type を t2 から t3 に変え, 注釈 α を持つことを意味する. 注釈 α は式 e が pure か impure かを示す. 式 e に付く注釈 α は,
@cps[t2 , t3 , α] のように式 e の answer type に付く注釈 α と一致する. 式と answer type の両方に注釈を付けるのは, selecitve CPS 変換は式だけを見て行い, 型推論は型だけを見て行うためである. また, var などの pure な型判断の結論部だけに表れる @cps[t2 , t2 , ϵ] では, answer type が変わらないことを示すだけなので t2 は free である. すると, pure な型判断に付く @cps[t2 , t2 , ϵ] はわざわざ書く
必要がないように思える. しかし pure な型判断に付く @cps[t2 , t2 , ϵ] を消すと, impure な型判断を
pure な型判断にする, 以下の規則が必要になる.
Γ ⊢ e ϵ : t1
Γ ⊢ e ϵ : t1 @cps[t2 , t2 , ϵ]
この型規則は導出する式 e が限定されていないため, 型推論の際に, この型規則を使う場所はすぐには判断できない. 本研究は, 型推論を過度に複雑にしないことを掲げているため, Pure な型判断に @cps[t2 , t2 , ϵ] を付けることで, 全ての型規則が導出する式を１種類にして, 型推論を単純にしている.
他の規則を見る前に制約の説明をする. 制約は以下の３種類からなる.

( = )

( ≤ )

( ̸= ⇒ = i)

これらの制約が満たされる場合を全て書き下すと図 3 になる.
最初の制約は両辺が等しくなければならないことを示す. この制約は図 2 の型規則には出て来な
いが, 後に制約解消を行う際に使われる. 次の制約 (α ≤ α′ ) は, α が i なら α′ も i にならなければな
らず, α′ が ϵ なら α も ϵ にならなければならないことを示す. ϵ と i の大小関係は ϵ < i である.

3

(x ϵ : T ∈ Γ and t1 ⊆ T )varΓ ⊢ x ϵ : t1 @cps[t2 , t2 , ϵ](c ϵ is a constant of basic type t1 )constΓ ⊢ c ϵ : t1 @cps[t2 , t2 , ϵ]

論文用
2 : t @cps[t , t , α ] (α ≤ α ) (tΓ, x : t1 ⊢ e α付き意味論の型規則
2
3 4
2
2
1
3 ̸= t4 ⇒ α2 = i)fun
Γ ⊢ (λα1 x.e α2 ) ϵ : (t1 → t2 @cps[t3 , t4 , α1 ]) @cps[t5 , t5 , ϵ]

α

(

)

上原 千裕

Γ, f ϵ : (t1 → t2 @cps[t3 , t4 , α2 ]), x ϵ : t1 ⊢ e α2 : t2 @cps[t3 , t4 , α2 ] (α2 ≤ α1 ) (t3 ̸= t4 ⇒ α2 = i)fixΓ ⊢ (fixα1 f.x.e α2 ) ϵ : (t1 → t2 @cps[t3 , t4 , α1 ]) @cps[t5 , t5 , ϵ]1(α1 ≤ α) (α2 ≤ α) (α3 ≤ α) (t3 ̸= t6 ⇒ α3 = i) (t5 ̸= t4 ⇒ α1 = i) (t6 ̸= t5 ⇒ α2 = i)Γ ⊢ e1 α1 : (t2 → t1 @cps[t3 , t6 , α3 ]) @cps[t5 , t4 , α1 ]Γ ⊢ e2 α2 : t2 @cps[t6 , t5 , α2 ]appΓ ⊢ (e1 α1 @α3 e2 α2 ) α : t1 @cps[t3 , t4 , α]
意味論と解き方と証明
型, 値, 項Γ ⊢ e α1 : t2 @cps[t2 , t1 , α1 ](t2 ̸= t1 ⇒ α1 = i)
reset
ϵ
α
Γ ⊢ ⟨e 1 ⟩ : t1 @cps[t3 , t3 , ϵ]Γ, k ϵ : ∀τ5 .(t1 → t3 @cps[τ5 , τ5 , ϵ]) ⊢ e α1 : t2 @cps[t2 , t4 , α1 ](t2 ̸= t4 ⇒ α1 = i)α ::= ϵ | i
shift
α
i
1
Γ ⊢ (Sk.e ) : t1 @cps[t3 , t4 , i]t ::= τ | bool | int | t1 → t2ϵ @cps[t3 , t4 , α] α monomorphic typeΓ ⊢ v ϵ : t1 @cps[t5 , t5 , ϵ]Γ, x : Gen(t1 ; Γ) ⊢ e 1 : t2 @cps[t3 , t4 , α1 ](t3 ̸= t4 ⇒ α1 = i)let
T ::= t | ∀τ.T
polymorphic
type
ϵ
α
α
1
1
Γ ⊢ (let x = v in e ) : t2 @cps[t3 , t4 , α1 ]v ::= n | x | true | false | λα x.A | fixα f.x.A
value(α1 ≤ α) (α2 ≤ α) (α3 ≤ α) (t4 ̸= t3 ⇒ α1 = i) (t2 ̸= t4 ⇒ α2 = i) (t2 ̸= t4 ⇒ α3 = i)
| A1@cps[t@α A2 |, tSk.A| ⟨A⟩Γ| ⊢ife Aα12 thenA2 elseA3 | letΓx⊢=ev αϵ 3in: tA@cps[texpression
α1 : vbool2Γ e⊢ e::=: t1 @cps[t1
4 3 , α1 ]22 , t4 , α 2 ]3
1
2 , t4 , α 3 ]
if
α
α
α
α
α
1
2
3
A ::= eexpression
annotationΓ ⊢ (if ewiththene2 else e3 ) : t1 @cps[t2 , t3 , α]1制約

図 2. 型規則(ϵ = ϵ)(i = i)(ϵ ≤ ϵ)(t1 ̸= t1 ⇒ ϵ = i)(ϵ ≤ i)(i ≤ i)(t1 ̸= t2 ⇒ i = i)(α1 ̸= α1 ⇒ ϵ = i)(α1 ̸= α2 ⇒ i = i)

図 3. 制約

評価文脈

最後の制約は, 図 2 の型規則では, 最初の２つには型が入り

1 then A else A ) α2 | ⟨E α ⟩ ϵE α ::= [ ] ϵ | (E α1 @α2 A) α3 | (v ϵ @α2 E(tα1 )̸=α3t | ⇒(ifαE=αi)e-context
1
2
1
2
ϵ
α
α
α
α
ϵ
α
α
α
α
α
1
2
3
2
1
3
1
2
F ::= [ ] | (F @ A) | (v @ F ) | (if F
then A1 else A2 )pure e-contextという形になる. これで, t1 と t2 が異なる型ならば α は i にならなければならないことを示す. 言

い換えると, α が ϵ にならば, t1 と t2 は同じでなければならない.
簡約規則
図 2 の型規則の前提部に @cps[t1 , t2 , α] が出てくる度に (t1 ̸= t2 ⇒ α = i) という制約が加わっている. これで, answer type が変わるなら α は i になり, α が ϵ なら t1 = t2 となることを示している.
((λα1 x.A) ϵ @α1 v ϵ ) α1 → A[v ϵ /x]
なお, 制約解消の段階では
α1
α1((fixα1 f.x.A) ϵ @α1 v ϵ )(αA[(fixf.x.A) ϵ /f ][v ϵ /x]α2 ⇒α = i)1 ̸=→ϵ⟨v ϵ ⟩ , →vϵという形の制約も使用する. この制約では最初の２つの部分には注釈が入っている.
′ϵϵ
α1 i i(α ≤ α ) の形の制約が図2 の型規則のどこに出てくるかを順に見る⟨(F α2 [(Sk.e) ]) ⟩ → ⟨(let k = (λ α2 x.⟨F α.2 [x ϵ ]⟩ ϵ ) ϵ in e α1 ) α1 ⟩規則 fun と fix では, 関数の本体部分の注釈 α と返される関数の型の注釈 α1 の間に, (α2 ≤ α1 )(if true ϵ then A1 else A2 ) α1 → 2A1という制約が導入されている. これは, 関数本体が impure なら関数の型も impure になることを示
ϵ
(if
false
then A1 else A2 ) α1 → A2
している
. (α
2 = α1 ) ではなく (α2 ≤ α1 ) となっているのは, 関数本体が pure でも, 周りの状況に(let x =v ϵ in e α1 ) α1 → (e α1 [v ϵ /x]) .α1例えば,
よってその関数を impureと扱いたい場合があるためである
λf. if true then f @ (λz. (Sk. k @ (k @ z))) else f @ (λx. x)

2 4

1

という項の λx. x である. 図 2 の型規則に合うように (λz. (Sk. k @ (k @ z))) に型と注釈を付けると,[ ] ⊢ (λi z. (Sk. (k ϵ @ϵ (k ϵ @ϵ z ϵ ) ϵ ) ϵ ) i ) ϵ : (t1 → t1 @cps[t1 , t1 , i]) @cps[t2 , t2 , ϵ]となるため, f の引数の型は (t1 → t1 @cps[t1 , t1 , i]) に固定される. この型を λx. x が持つ必要があるため, この例のプログラム中の λx. x は, 図 2 の型規則に合うように型に注釈を付けるとϵ[ ] ⊢ (λi x. x ϵ ) : (t1 → t1 @cps[t1 , t1 , i]) @cps[t4 , t4 , ϵ]となる. 従ってこの例は, 型規則 fun において α1 = i, α2 = ϵ となる例である.
規則 app は関数呼び出しである. ３つの不等式制約で, 関数部分, 引数部分, 関数本体のどこかがimpure なら, 全体として impure になることを示している. また, すべて pure だったとしても, 全体として impure に扱うことも許している.
規則 reset は, 本体部分では shift が使われるかもしれないが, その効果はこの reset までで外には漏れないので, reset 自身は pure として良いことを示す.
規則 shift は impure であること, ここで捕捉される継続 k は pure であることを示す. ここが唯一,
impure であることを強制する場所である. 導出される式には impure であることを示す @cps[t3 , t4 , i]が付く.
規則 let は vaule restriction がかかっているため, v は pure で全体の注釈は e の注釈と一致す
る. また, FTV(t) が t の自由な型変数の集合を表す時, Gen(t1 ; Γ) = ∀τ1 ...τn .t1 （ただし τ1 ...τn =FTV(t1 )\FTV(Γ)）である.
最後に, 規則 if は条件部分, then 部分, else 部分のいずれかが impure だったら全体も impure となることを示す. その際, 規則 app と同様に, 全て pure だったとしても全体として impure に扱うことも許している.

2.3

Asai and Kameyama の型規則との差異

Asai and Kameyama [2] の型規則は, pure な型判断 Γ ⊢p e : t1 と一般の型判断 Γ ⊢ e : t1 @cps[t2 , t3 ]からなる. 前者は本稿の Γ ⊢ e : t1 @cps[t2 , t2 , ϵ] , 後者は Γ ⊢ e : t1 @cps[t2 , t3 , α]（ただし α = ϵ または α = i）に対応する.
Asai and Kameyama [2] の型規則には exp 規則という以下の規則がある.
Γ ⊢ p e : t1exp
Γ ⊢ e : t1 @cps[t2 , t2 ]この規則は pure な型判断を一般の型判断に変換するため, 一般の型判断の形をとっていても実質的に pure な式があった. 従って answer type が同じだったとき, それは shift が起きるがたまたま
answer type が変わらなかったのか, shift が起きないために answer type が変わらなかったのか判断できない. 例えば,
if true then λx. Sk.k @ (k @ x) else λy. yでは, if 文の then 部分と else 部分で同じ型が付き,

λx. Sk.k @ (k @ x) : (t1 → t1 @cps[t1 , t1 ])であるから,

λy. y : (t1 → t1 @cps[t1 , t1 ])という型が付く. Shift が起きる場所だけを CPS 変換することを考えると, then 部分の関数の本体
は CPS 変換が必要で, else 部分の関数 g の本体は CPS 変換を必要としないものとしたい. しかし,どちらも answer type が t1 から t1 への変換であり, CPS 変換を必要とするのか判断ができない.
一方本稿では, 注釈を付けることで impure な場所を特定する. この注釈によって CPS 変換が必
要かどうかを判断することができる.
本稿で示す型規則は, Asai and Kameyama [2] の型規則から exp 規則を取り除き, それ以外の規則に注釈と制約を加えたものだが, 両者の型付け能力は等価である.

5

定理 2.1 Asai and Kameyama の型規則で型が付くなら, 本稿の型規則でも型が付く. 逆に, 本稿の
型規則で型が付くなら, Asai and Kameyama の型規則でも型が付く.
これを示すには, お互いの型規則を模倣できることを確認すれば良い. 具体的な証明は第一著者の修士論文 [14] で行っているため, ここでは言葉で説明する.
本稿の型規則を Asai and Kameyama [2] の型規則で模倣するには, 基本的には単に注釈を無視して対応する型規則を使えば良い. ただ, Asai and Kameyama [2] の型規則では value が pure な型判断であるが, 本稿の型規則では前提部分に pure な型判断が出てくることはない. そのため, 本稿の型規則で前提部分に value が出て来た場合は, 変換時に前提部分に exp 規則を使うことになる.
一方, Asai and Kameyama [2] の型規則を本稿の型規則で模倣するには, 以下のようにすれば良い.

• Pure な型規則は, 本稿の型規則で注釈を ϵ とすることで模倣する.
• それ以外の型規則は, 本稿の型規則で注釈を i とすることで模倣する.
本稿の型規則が Asai and Kameyama [2] の型規則と異なるところは, 注釈によって pure と判断できる部分を増やしていることである. 上に示した模倣では, pure な型規則以外はすべて注釈を i としたが, 場合によっては ϵ にできる場合もある. それを可能にしているのが本稿の型規則である.

3

制約解消

この第 3 節では, 注釈が i か ϵ かまだ定まっていない注釈変数を α と表す.
入力の式を与えられたら, まず図 2 の型規則に従って型推論を行う. その際, 注釈と制約はそのまま保持しておく. 注釈と制約を除けば図 2 の型規則はこれまでの規則とほぼ同一なので, 普通の let
多相の入った型推論をすれば良い. その結果, 入力の式の各部分式や λ, fix, @ にはユニークな注釈の変数が割り振られ, それに対する制約が生成される.
制約に対する解とは, 全ての注釈の変数に対する注釈の割り当てのうち, 全ての制約を満たしている（図 3 の形になっている）ものである. 生成された制約に対して, 全ての注釈に i を入れると解になっているが, これは次の３点を確認することで理解できる.

• (t1 ̸= t2 ⇒ α = i) の形の制約は α に i を入れれば満たされている.
• Value の各構成子及び reset ⟨ ⟩ に対する型規則では, 結論部に ϵ が現れているが, 全ての規則
において, 前提部の注釈は (α1 ≤ α2 ) の形の制約の左辺にしか出てきていない. 従って, 右辺に i が入れば制約は満たされる.
• Let の型規則の最初の前提部に ϵ が現れているが, value の型規則の結論部は全て ϵ になっている. 従って, ϵ が (α1 ≤ α2 ) の形の制約の右辺に出てくることはない.
従って, 解は必ず１つは存在することが分かる. 本稿の制約解消の目標は, なるべく小さい解, つま
りなるべく ϵ が多い解を見つけることである.
しかし, なるべく小さい解を求めるのは簡単ではない. 一般には「最良の解」は存在しないことが分かっている. 以下では, 型推論と制約解消が過度に複雑にならない範囲で, ある程度の解が得られる制約解消法を示す. その際, 別の方法を取ったらより良い解を見つけられる可能性のある場合は,それを明示する.
制約の解消は, 次の４段階からなる.

1. 制約を注釈に関する制約のみに変換する
2. 自明な制約を解消する
3. 自明でない制約を解消する
4. 以上で確定しなかった注釈は ϵ とする
以下, それぞれについて説明する.

6

3.1

制約を注釈に関する制約のみに変換する

まず, (t1 ̸= t2 ⇒ α = i) という, 型 t1 と t2 に言及する制約を, 型に言及しない制約 (α = i), または (α1 ̸= α2 ⇒ α = i) に変換する. 変換は t1 と t2 の場合分けで行い, その方針は以下の２つである.

• t1 と t2 が異なるなら α = i という制約に変換する• t1 と t2 が同じなら, この制約は自明に満たされているので, この制約を削除する
例えば, (bool ̸= int ⇒ α = i) という制約は, bool ̸= int であるから (α = i) となる. また,(int ̸= int ⇒ α = i) という制約は, 前提が成り立たないため, 既に制約を満たしている. そのため,制約自体を削除する. t1 と t2 が関数型

t1 = (t11 → t12 @cps[t13 , t14 , α1 ])t2 = (t21 → t22 @cps[t23 , t24 , α2 ])だった場合は, 再帰的に両者が同じかどうかを判断する. 対応する型が１つでも異なれば両者は異なる型なので, α = i という制約に変換される. 一方, 注釈も含めて全て同じになったら, 両者は同じ型となり, この制約は削除される.
しかし, この方針だと, 型が全て同じだが注釈のみ異なる場合に困る. 注釈の値はまだ確定していないので, 両者が異なるかどうかをこの段階では判断できない. そこで, この場合は異なる注釈 α1と α2 を使って(α1 ̸= α2 ⇒ α = i)という制約に変換する. これでもとの意味を保ったまま関数型に関する制約を注釈に関する制約に変換することができる. 部分式の中が関数型になっており, その中に異なる注釈がある場合には,(α1 ̸= α2 ⇒ α = i) の形の制約が複数作られることになることに注意する.
以上で, t1 , t2 が型変数以外の場合の変換が終了した. 以上の変換は, 変換前後で解の集合を変化させない. 従って, 変換後の制約に対して制約解消を行えば, もとの制約に対して制約解消を行ったのと同じ解が得られることになる.
一方, t1 , t2 の片方, あるいは両方が型変数の場合は, 両者が同じ型変数である場合を除くと, この変換を行うのは簡単ではない. 例として,

let f = λg. g @ 1 in f @ (λx. x)を考える. λg. g @ 1 に対して型推論を行うと以下のようになる. 式に付く注釈は省略している. また,

Γ′ = g : (int → τ2 @cps[τ3 , τ4 , α4 ])とする. この例の更に詳しい解説は著者の修士論文 [14] で行っている.

var
const
Γ′ ⊢ g : (int → τ2 @cps[τ3 , τ4 , α4 ]) @cps[ , , ϵ]Γ′ ⊢ 1 : int @cps[ , , ϵ]app
Γ′ ⊢ g @ 1 : τ2 @cps[τ3 , τ4 , α3 ]fun[ ] ⊢ λg. g @ 1 : ((int → τ2 @cps[τ3 , τ4 , α4 ]) → τ2 @cps[τ3 , τ4 , α2 ]) @cps[ , , ϵ]f に渡される関数を表す g は (int → τ2 @cps[τ3 , τ4 , α4 ]) という型を持っており, それに伴って(τ3 ̸= τ4 ⇒ α4 = i)という制約が生成されている. ここで τ3 と τ4 が異なるかどうかはすぐには判断できない. 上記のプ
ログラムの場合は, f に渡される関数が λx. x という pure な関数であるから τ3 = τ4 とすれば α4 はϵ にできる.
しかし f が in 以下で f @ (λx. Sk. x) のように impure な関数を渡されたとすると τ3 ̸= τ4 とな
り α4 は i でなくてはならない. つまり, f に渡される関数を pure とできるかどうかは in 以下で fがどのように使われるかに依存する. これは, let 多相の考え方と相反するものである. Let 多相で7

上原 千裕C ∪ {α = i} ⇒ C[i/α]C ∪ {α1 ̸= α2 ⇒ ϵ = i} ⇒ C ∪ {α1 ≤ α2 , α2 ≤ α1 }C ∪ {α = ϵ} ⇒ C[ϵ/α]C ∪ {α1 ̸= α2 ⇒ i = i} ⇒ C
C ∪ {ϵ ̸= ϵ ⇒ α = i} ⇒ C
C ∪ {ϵ ̸= i ⇒ α = i} ⇒ C ∪ {α = i}C ∪ {ϵ ≤ ϵ} ⇒ C

C ∪ {ϵ ̸= α2 ⇒ α = i} ⇒ C ∪ {α2 ̸= ϵ ⇒ α = i}C ∪ {ϵ ≤ i} ⇒ C

C ∪ {i ̸= ϵ ⇒ α = i} ⇒ C ∪ {α = i}C ∪ {ϵ ≤ α2 } ⇒ C

C ∪ {i ≤ ϵ} ⇒ 型エラーなので終了

C ∪ {i ̸= i ⇒ α = i} ⇒ C
C ∪ {i ̸= α2 ⇒ α = i} ⇒ C ∪ {α2 ̸= i ⇒ α = i}C ∪ {i ≤ i} ⇒ C

C ∪ {α1 ̸= ϵ ⇒ α = i} ⇒ 自明でないので制約を残す

C ∪ {i ≤ α2 } ⇒ C ∪ {α2 = i}C ∪ {α1 ̸= i ⇒ α = i} ⇒ 自明でないので制約を残す

C ∪ {α1 ≤ ϵ} ⇒ C ∪ {α1 = ϵ}C ∪ {α1 ≤ i} ⇒ C

C ∪ {α1 ≤ α2 } ⇒ 自明でないので制約を残す

C ∪ {α1 ̸= α2 ⇒ α = i} ⇒ 自明でないので制約を残す

図 4. 制約の解消規則

は, let f = λg. g @ 1 in の部分だけを見て f の引数となる関数の型を含む f そのものの型を定め,
generalize した上で in 以下で f を使う. しかし, 注釈の部分は, in 以下でどのように f が使われているかを見ない限り決められない. 本稿ではこのような場合, 型変数は自分以外の型変数や他の具体的な型とは異なると捉えて, (τ ′ ̸= τ ′′ ⇒ α = i) という制約を (α = i) という制約に変換するという方針をとる. これは, 上の例で言えば f の型を∀ τ2 τ3 τ4 . ((int → τ2 @cps[τ3 , τ4 , i]) → τ2 @cps[τ3 , τ4 , i])とすることを意味している. この選択をすることで, より良い解を捨てている可能性がある. 一方,
この選択で, in 以下での f の使われ方を見てから f に渡される関数が pure かどうかを判断するという, let 多相の考え方と相反する解き方を避けている.
以上が, 制約を注釈に関する制約のみに変換する方法の説明である. これを規則にしたものは著者の修士論文 [14] に載っている.

3.2

自明な制約を解消する

制約が注釈に関する制約のみになったら, 次に自明な制約解消を行う. その規則を図 4 に示す. 最1
初の２つは, 等式制約は代入を実際に行うことで制約解消を行うことを示している. その後の規則
は, ( ≤ ) の形の制約解消である. 注釈の代入を行った結果 (i ≤ ϵ) が出てきてしまったら, 型エラーである. 図 2 の型規則では, ϵ は ( ≤ ) の形の左側にしか出てこない. そのため (i ≤ ϵ) の場合は通常では起こり得ない. しかし後に触れるライブラリ関数等を導入しようとする際には, 型規則の中の関数型に ϵ が入っている場合がある. すると ϵ が ( ≤ ) の形の右側に出て来る場合がある. 最後の (α1 ≤ α2 ) の場合は, 現時点では制約解消できないためそのまま残す.
右の列は ( ̸= ⇒ = i) の形の制約の場合である. 基本的に

• ⇒ の左側が成り立つ制約は ⇒ の右側のみの制約に変換• ⇒ の左側が成り立たない制約は削除• ⇒ の右側が成り立つ制約も削除• ⇒ の右側が成り立たない制約は, 左側が成り立たないという制約に変換

8という操作を行っている. 最初の規則は α1 と α2 が等しいことを ( ≤ ) という形の制約で表現している. 最後の３つは, 現時点では制約解消できないので, そのまま残す.
以上を繰り返し行うと, 最終的に残る制約の形は(α1 ̸= ϵ ⇒ α = i)(α1 ̸= i ⇒ α = i)(α1 ̸= α2 ⇒ α = i)(α1 ≤ α2 )となる. 図 4 で示した変換が解の集合を変化させないことは自明である.

3.3

自明でない制約を解消する

最後に残った４種類の制約のうち, 最初の３つの解消は簡単ではない. 任意の命題 A, B においてA ⇒ B は not A or B と書けるため, 最初の３つの制約は以下のように書き直すことができる.

α1 = ϵ or α = i

α1 = i or α = i

α1 = α2 or α = i

このような制約が存在すると, どちらをとって良いか分からず, 単純に制約解消をすることはできな
い. 全数探索などの方法は考えられるが, そもそも第 3.5 節で紹介するように, 最も良い解は一般には存在しないため, 全数探索してもどれを選べば良いのかは明らかではない. 更に, 最初の制約で,より ϵ の多い解を求めたいために不用意に α1 = ϵ を選択すると, 場合によってはそれが他のところ
で他の制約と衝突することも考えられる. 例えば

α1 = ϵ or α = i

α1 = i or α2 = i

α 2 ≤ α1α1 ≤ α2となっていたとする. 最初の制約で α1 = ϵ を選ぶと, ２つ目の制約で α2 = i となる. すると, ３つ目の制約で α1 = i となり最初の α1 = ϵ と衝突する. しかし, α, α1 , α2 に i を入れればすべての制約を満たすので解は存在する. つまり, 貪欲に α1 = ϵ を選ぶことはできないことになる.
以上の考察を踏まえて, 本稿では安全な方法として最初の３つの制約は全て α = i として解消するという方針を取る. この選択も, より良い解があるのに, それを捨てている可能性がある. 一方で,解を全数探索に行く等のことをすることなく解を求めることができるようになっている.
なお, 実際に, ここで全数探索をしていればより良い解が見つかるような例を作ることができる.
しかし, かなり人為的な例 [14] となり, これまで我々が試した限られた実用的な例の中では, このような例に遭遇していない. 全数探索など, より強力な制約解消が必要かどうかを考察することは今後の課題である.

3.4

以上で確定しなかった注釈は ϵ とする

これまでの制約解消の結果, 残った制約は α1 ≤ α2 の形のものだけである. この形の制約は, この時点で確定していない注釈に全て ϵ を入れて解消する. こうしてなるべく pure な解を求めている.

3.5

最も良い解が存在しない例

最も良い解が存在しない例として, 以下の例がある.

λf. λg. (⟨(f @ 1) + (g @ 2)⟩ = true)
これは, 関数 f @ 1 と g @ 2 の結果を加えたら, それが true になるかどうかを真偽値で返す関数である. 加えた結果が true になっているということは, f あるいは g の少なくともどちらかが answer
type を int から bool に変える関数である必要がある. ここで, f と g の型は以下のようになる.

f : (int → int @cps[τ1 , bool, α1 ])g : (int → int @cps[int, τ1 , α2 ])f は answer type を τ1 から bool に変え, g は int から τ1 に変えるような関数となる. 左から実行するとして, f の中で shift が実行されると継続として λy. ⟨y + g @ 2⟩ が取られるが, この継続は, g の中で shift が実行されると answer type として τ1 を返す. f の中でその τ1 を bool に変える. 全体として, answer type は int から bool になるので, 上の式には型が付く.
9

f と g に対して以下の制約が生成される.
(τ1 ̸= bool ⇒ α1 = i)(int ̸= τ1 ⇒ α2 = i)本稿が示す制約解消では, 型変数 τ と int や bool は常に異なるとするので, 結局, α1 = α2 = i となり, f も g も impure となる. しかし, 実際には両方とも impure である必要はなく, f と g のどちらか片方が impure であれば十分である. この２つの解, つまり f のみが impure な解と g のみが impureな解は, 前者では α1 = i, α2 = ϵ なのに対し, 後者は α1 = ϵ, α2 = i となっており, どちらがより良
いかを比べることのできない解になっている.
なお, f のみが impure な解と g のみが impure な解が, この例における一番 ϵ が多い解であるから, この２つの解が「極大の解」である. この例は, 本稿が複雑な型推論と制約解消法を避けているために「極大の解」が得られない場合があることを意味する.

4

Selective CPS 変換

第 3 節で制約解消が済み, 式の各部に ϵ か i の注釈が付いたら, それに従って i の注釈が付いている箇所のみ CPS 変換するのは比較的簡単である. その定義を図 5 に示す. 基本的には, Danvy andFilinski [4] による administrative redex を変換時に簡約する形の CPS 変換を, selective に拡張したものである. ここで, オーバーラインは CPS 変換時に実行される式, アンダーラインは CPS 変換結果として返される構文である. 変換結果の構文は, 標準的な let 多相の入った λ 計算である. 従って,構文を変換すればそのまま OCaml などの処理系で実行することができる.
図 5 の変換は, 変換される式の一番外側の注釈が i か ϵ かによって２種類に分かれている. 基本的に, impure の場合は通常の CPS 変換を行い, pure の場合は直接形式のまま返す. Impure な式の中から pure な式を呼び出す場合は, その時点での継続 k に pure な式の変換結果をそのまま渡す格好になる. 逆に pure な式の中から impure な式を呼び出すのは reset の場合しかあり得ず, その際には恒等関数を継続として渡す.
最終的に, pure な式 e ϵ の selective CPS 変換は∥ e ϵ ∥ϵとなり, impure な式 e i の selective CPS 変換は

λk. ∥ e i ∥i @ (λm. k @ m)となる.
本稿では簡約規則を示していないが, 図 2 の型規則は注釈を無視した簡約規則のもとで subject
reduction を満たすことを証明できる. その上で, 図 5 で示す selective CPS 変換は以下の定理を満たす. ただし, E はアンダーラインの付いた式, つまり CPS 変換後の式の任意の評価文脈である.
定理 4.1e ϵ →∗ v ϵ ∧ ⊢ e ϵ : t1 @cps[t2 , t2 , ϵ] ⇒ ∥ e ϵ ∥ϵ →∗ ∥ v ϵ ∥ϵe i →∗ v ϵ ∧ ⊢ e i : t1 @cps[t2 , t2 , i] ⇒ (λk. ∥ e i ∥i @ (λm. k @ m)) @ (λx. E[x]) →∗ E[∥ v ϵ ∥ϵ ]これは, 注釈のついたプログラムの実行結果と selective CPS 変換後のプログラムの実行結果が対応することを示す. この定理は Danvy and Filinski [4] の証明に沿った形で示すことができる [14].
また, 本稿の注釈付きの型と selective CPS 変換後の, 型と環境の変換を以下に定義する.
定義 4.2 型と環境の変換 ⋆bool ⋆ = boolint ⋆ = int(t1 → t2 @cps[t3 , t3 , ϵ]) ⋆ = (t1 ⋆ → t2 ⋆ )[ ]⋆ = [ ]τ⋆ =τ(∀τ. T ) ⋆ = ∀τ ⋆ . T ⋆(t1 → t2 @cps[t3 , t4 , i]) ⋆ = (t1 ⋆ → ((t2 ⋆ → t3 ⋆ ) → t4 ⋆ ) )(Γ, x ϵ : t) ⋆ = Γ⋆ , x : t⋆10

ministrative redex をなくす方)∥ e i ∥i : Transformation of e i to continuation passing style∥ (v1 ϵ @i e2 i ) i ∥i = λk. ∥ e2 i ∥i @ (λv2 . (∥ v1 ϵ ∥ϵ @ v2 ) @ (λv. k @ v))∥ (e1 ϵ @i e2 i ) i ∥i = λk. (λv1 . ∥ e2 i ∥i @ (λv2 . (v1 @ v2 ) @ (λv. k @ v))) @ ∥ e1 ϵ ∥ϵ(e1 is NOT value)∥ (e1 i @i e2 ϵ ) i ∥i = λk. ∥ e1 i ∥i @ (λv1 .(v1 @ ∥ e2 ϵ ∥ϵ ) @ (λv. k @ v))∥ (e1 ϵ @i e2 ϵ ) i ∥i = λk. (∥ e1 ϵ ∥ϵ @ ∥ e2 ϵ ∥ϵ ) @ (λv. k @ v)

∥ (e1 i @i e2 i ) i ∥i = λk. ∥ e1 i ∥i @ (λv1 . ∥ e2 i ∥i @ (λv2 . (v1 @ v2 ) @ (λv. k @ v)))∥ (v1 ϵ @ϵ e2 i ) i ∥i = λk. ∥ e2 i ∥i @ (λv2 . k @ (∥ v1 ϵ ∥ϵ @ v2 ))∥ (e1 ϵ @ϵ e2 i ) i ∥i = λk. (λv1 . ∥ e2 i ∥i @ (λv2 . k @ (v1 @ v2 ))) @ ∥ e1 ϵ ∥ϵ
i

ϵ

ϵ i

i

(e1 is NOT value)ϵ∥ (e1 @ e2 ) ∥i = λk. ∥ e1 ∥i @ (λv1 . k @ (v1 @ ∥ e2 ∥ϵ ))∥ (e1 i @ϵ e2 i ) i ∥i = λk. ∥ e1 i ∥i @ (λv1 . ∥ e2 i ∥i @ (λv2 . k @ (v1 @ v2 )))∥ (e1 ϵ @ϵ e2 ϵ ) i ∥i = λk. k @ (∥ e1 ϵ ∥ϵ @ ∥ e2 ϵ ∥ϵ )∥ (Sx.e i ) i ∥i = λk. let x= λa. (k @ a) in (∥ e i ∥i @ (λy.y))∥ (Sx.e ϵ ) i ∥i = λk. let x= λa. (k @ a) in ∥ e ϵ ∥ϵ∥ (let x = v ϵ in e i ) i ∥i = λk. let x = ∥ v ϵ ∥ϵ in (∥ e i ∥i @ k)

∥ (if e1 i then e2 i else e3 i ) i ∥i = λk. ∥ e1 i ∥i @ (λv1 . if v1 then ∥ e2 i ∥i @ k else ∥ e3 i ∥i @ k)

∥ (if e1 ϵ then e2 i else e3 i ) i ∥i = λk. if ∥ e1 ϵ ∥ϵ then ∥ e2 i ∥i @ k else ∥ e3 i ∥i @ k∥ (if e1 i then e2 ϵ else e3 i ) i ∥i = λk. ∥ e1 i ∥i @ (λv1 . if v1 then k @ ∥ e2 ϵ ∥ϵ else ∥ e3 i ∥i @ k)
∥ (if e1 i then e2 i else e3 ϵ ) i ∥i = λk. ∥ e1 i ∥i @ (λv1 . if v1 then ∥ e2 i ∥i @ k else k @ ∥ e3 ϵ ∥ϵ )∥ (if e1 ϵ then e2 ϵ else e3 i ) i ∥i = λk. if ∥ e1 ϵ ∥ϵ then k @ ∥ e2 ϵ ∥ϵ else ∥ e3 i ∥i @ k∥ (if e1 ϵ then e2 i else e3 ϵ ) i ∥i = λk. if ∥ e1 ϵ ∥ϵ then ∥ e2 i ∥i @ k else k @ ∥ e3 ϵ ∥ϵ∥ (if e1 i then e2 ϵ else e3 ϵ ) i ∥i = λk. ∥ e1 i ∥i @ (λv1 .k @ (if v1 then ∥ e2 ϵ ∥ϵ else ∥ e3 ϵ ∥ϵ ))∥ (if e1 ϵ then e2 ϵ else e3 ϵ ) i ∥i = λk. k @ (if ∥ e1 ϵ ∥ϵ then ∥ e2 ϵ ∥ϵ else ∥ e3 ϵ ∥ϵ )∥ e ϵ ∥ϵ : Transformation of e ϵ to direct style∥ x ϵ ∥ϵ = x∥ (fixi f.x.e i ) ϵ ∥ϵ = fix f.x.(λk ′ . ∥ e i ∥i @ (λv. k ′ @ v))∥ n ϵ ∥ϵ = n∥ (fixi f.x.e ϵ ) ϵ ∥ϵ = λx. λk ′ . k ′ @ (∥ (fixϵ f.x.e ϵ ) ϵ ∥ϵ @ x)

∥ true ϵ ∥ϵ = true

∥ false ϵ ∥ϵ = false∥ (fixϵ f.x.e ϵ ) ϵ ∥ϵ = fix f.x. ∥ e ϵ ∥ϵϵ

∥ (λi x.e i ) ϵ ∥ϵ = λx. λk ′ . ∥ e i ∥i @ (λv. k ′ @ v)

∥ (λi x.e ϵ ) ϵ ∥ϵ = λx. λk ′ .k ′ @ ∥ e ϵ ∥ϵ

∥ (λϵ x.e ϵ ) ϵ ∥ϵ = λx. ∥ e ϵ ∥ϵ∥ (e1 ϵ @ϵ e2 ϵ ) ϵ ∥ϵ = ∥ e1 ϵ ∥ϵ @ ∥ e2 ϵ ∥ϵ∥ ⟨e i ⟩ ∥ϵ = ∥ e i ∥i @ (λx.x)∥ ⟨e ϵ ⟩ ϵ ∥ϵ = ∥ e ϵ ∥ϵ∥ (let x = v ϵ in e ϵ ) ϵ ∥ϵ = let x = ∥ v ϵ ∥ϵ in ∥ e ϵ ∥ϵ∥ (if e1 ϵ then e2 ϵ else e3 ϵ ) ϵ ∥ϵ = if ∥ e1 ϵ ∥ϵ then ∥ e2 ϵ ∥ϵ else ∥ e3 ϵ ∥ϵ

図 5. Selective CPS 変換

611この時, 以下が式 e の derivation に関する帰納法で証明できる [14].
定理 4.3 Type PreservationΓ ⊢ e ϵ : t @cps[t1 , t1 , ϵ] ⇒ Γ ⋆ ⊢ ∥ e ϵ ∥ϵ : t ⋆Γ ⊢ e i : t @cps[t1 , t2 , i] ⇒ Γ ⋆ ⊢ λk. ∥ e i ∥i @ (λm. k @ m) : ((t ⋆ → t1 ⋆ ) → t2 ⋆ )5

実行例

本研究で提案するシステム, つまり型推論, 制約解消そして selective CPS 変換を実装した. この実装したシステムは, answer type が変わるようなものも扱えるようになっている.
その上で, 本稿で示した selective CPS 変換の効果を見るため, shift/reset を使って具体的なプログラムを書いた. それを selective CPS 変換した結果と CPS 変換した結果の実行時間を計測した.
具体的なプログラムは, prefix 関数と N-Queen 問題を解く関数の２つである. 以下順に説明する.
なお実行環境は MacOSX 10.9.4, メモリが 4GB, CPU が 1.3GHz の Intel Core i5 である. 変換結果のプログラムを OCaml 4.02.2 を使ってネイティブコードにコンパイルし, user time を計測した.
また, システムに直接手を加えて限定継続命令をサポートしている言語との比較はしない. Scheme
上での直接実装 [6] は動的型付けであるため OCaml と単純な比較はできないこと, OCaml の Delimcc
ライブラリ [8] は直接は answer type modification を扱えないこと, Caml Light を拡張した OchaCaml[10] はネイティブコンパイラがないことが理由である.

5.1

Prefix 関数

Prefix 関数を shift/reset を使って非決定性プログラミングの形で記述した [9]. この関数は, 受け取ったリストのプリフィックスのリストを返す. 例えば prefix [1; 2; 3] は [[1]; [1; 2]; [1;2; 3]] となる. プログラムは以下である.
let rec visit = match lst with[] -> shift k -> []| a :: rest -> a :: (shift k -> (k []) :: <k (visit rest)>) in
let prefix lst = <visit lst>
リストの次に付けるべき要素 a までを shift を使って継続 k として取り出す. k [] で a までが付いたリストを, <k (visit rest)>で a 以降に rest のプリフィックスが付いた複数のリストを返す.

5.1.1

実行時間の比較prefix の selective CPS 変換の結果と CPS 変換の結果にリストを渡して実行時間を計測した. 実
行時間の計測結果を図 6 に示す. 図 6 の「Selective CPS」が, プログラムを selective CPS 変換した
結果にリストを渡して実行した時にかかった時間, 「CPS」がプログラムを全て CPS 変換した結果にリストを渡して実行した時にかかった時間である. 渡すリストは要素の数字が全て 0 で, 長さが750, 1000, 2500, 5000, 7500, 10000 の場合を実行している. 表から分かるように約 11% ほどの実行
時間の改善が見られる.

12

The execution time (ms) of preﬁx lst whose length is 750, 1000, 2500, 5000, 7500, 10000, which is user time
length islength islength islength islength islength isselective CPS

16

24

177

771

1796

3233

CPS

18

37

199

842

2050

3618

selective CPS / CPS

0.89

0.89

0.89

0.92

0.88

0.89

750

1000

2500

5000

7500

10000

図 6. loop n の実行時間の比較

5.1.2

変換後のプログラムの比較

prefix を CPS 変換した結果は以下である.
let rec visit = fun k’ ->match x with [] -> let k = fun a’ -> fun k’’ -> k’’ (k’ a’) in []| a :: rest ->let k = fun a’ -> fun k’’ -> k’’ (k’ (a :: a’)) in(k []) (fun x -> x :: ((visit rest) ((fun x -> (k x) (fun x -> x))))) in
let prefix = fun lst -> fun k -> k ((visit lst) (fun x -> x))
また, selective CPS 変換した結果は以下である.

let rec visit = fun k’ ->match x with [] -> let k = fun a’ -> k’ a’ in []| a :: rest -> let k = fun a’ -> k’ (a :: a’) in(k []) :: ((visit rest) (fun x -> k x)) in
let prefix = fun lst -> (visit lst) (fun x -> x)
２つのプログラムの差異は, shift が切り取る継続 k が引数として継続を取るか否かである. Shift が捕捉した継続は pure であるため, selective な方では k への呼び出しが直接形式で行われる. また, リ
ストと match 文を使っているが, 本稿の枠組にこれらをサポートするのは簡単である.

5.1.3

Queen 関数

本稿で示した selective CPS 変換の効果を見るため, N-Queen 問題を解くプログラムを shift/resetを使って非決定性プログラミングの形で記述し [9], その実行時間を計測した.
最初に, 1 から n までを非決定的に選択する関数 choice を定義する. この関数は, 現在の継続 kを切り取ってきて, k に値 num を渡した後, さらに k に j-1 以下の値について再帰した値を渡すため,実質的に num から 1 までの数を非決定的に返す関数とみなせる [9].

(* 引数として数字 num を受け取り, num ~ 1 を順番に返す関数. *)let rec choice num =if num = 1 then 1 else shift k -> (k num; k (choice (num - 1)))
N-Queen 問題を解くメインルーチンは以下のようになる. ここで print solution は解が見つかった時にそれを表示する関数, また is safe は Queen を他の Queen とぶつかることなく置けるかをチェックする関数で, いずれも別途, 定義する必要がある.

13

The execution time (ms) of queen n which is user timequeen 8queen 9 queen 10 queen 11 queen 12 queen13 queen14 queen15

selective CPS

3

9

34

184

1074

6812

45807

329027

CPS

5

12

48

254

1490

9524

63450

458004selective CPS / CPS

0.6

0.75

0.71

0.72

0.72

0.72

0.72

0.72

図 7. queen n の実行時間の比較(* 引数として数字 n を受け取り, n*n の Queen 問題を解いた答えを出力する関数 *)let queen = fun n ->(* loop 関数は, i 列目以前, Queen を何行目に入れるかを決定 *)(* 引数 solution は, i - 1 列目以降, 各列の何行目に Queen を入れるかのリスト *)let rec loop (i, solution) =if i = 0 then print_solution solution (* 答えを出力 *)else
let j = choice n in
let solution2 = j :: solution in
if is_safe solution2(* i 列目は j 行目が答えになる場合 *)then loop (i - 1, solution2)(* i - 1 列目以前の答えを求める *)else ()(* choice で別の j を選んで続ける *)in<loop (n, [])> in(queen n) (* n は引数となる数字 *)choice 関数がバックトラックを全て引き受けるため, queen 関数は単に, Queen を置く場所を順に選び, 最後まで成功したら結果を表示するという処理を記述すれば良い. プログラム中に出てくる
let 文は定義される式が値ではないため, 多相の let 文ではなく単相の let 文, つまり fun 文と関数呼び出しとして扱われる.
queen 関数が, ２つの引数をペアにして受け取ってくるのは, カリー化して順番に受け取るようにすると, そのたびに CPS 変換されてしまい, 全体を CPS 変換する方法にとって著しく不利になるためである. Selective に CPS 変換していれば, １つ目の引数を渡す部分は pure になるため CPS 変換
されず, 従って非効率にはならない.
5.1.4

実行時間の比較queen のプログラムを, プログラム全体を CPS 変換した場合と, 本稿に示す selective CPS 変換
をした場合の２通りについて実行し, その実行時間を計測した. その結果を図 7 に示す. 図 7 の「Selective CPS」が, プログラムを selective CPS 変換して queen n を実行した時にかかった時間,「CPS」がプログラムを全て CPS 変換して queen n を実行した時にかかった時間である. 表から分かるように約 28% ほどの実行時間の改善が見られる.
5.1.5

変換後のプログラムの比較

choice を CPS 変換した結果は以下のようになる.
let rec choice j = fun k’ ->14

if j = 1 then k’ 1else let k = fun a -> fun k’’ -> k’’ (k’ a) in(k j) (fun x -> (choice (j - 1)) (fun x’ -> (k x’) (fun x’’ -> x; x’’)))
また, selective CPS 変換した結果は以下である.

let rec choice = fun k’ ->if j = 1 then k’ 1else let k = fun a -> k’ a in (k j; (choice (j - 1)) (fun x’ -> k x’)))choice は中で shift を使っているため, selective CPS 変換でも基本的には CPS 変換する必要があ
る. しかし, selective な方では, 捕捉した継続が pure であることを利用して k への呼び出しが直接形式で行われるようになっている.
次に, 関数 queen を比べる. CPS 変換した結果を載せて, selective CPS 変換した結果が違う場合
は, CPS 変換の結果 selective CPS 変換の結果 と書く. CPS 変換の結果が selective CPS 変換の結果に含まれない場合は, selective CPS 変換の結果を書かないで, CPS 変換の結果 だけ書く.

let queen = fun n -> fun kk ->let rec loop (i, solution) =fun k -> if i = 0 then (print solution solution) (fun x -> k x)
k (print solution solution)else (choice n)(fun x ->(* x = choice n *)((fun j ->(* j = x *)fun k’ ->(* k’ = fun x -> k x *)((fun solution2 ->(* solution2 = j :: solution *)fun k’’ ->(* k’’ = fun x -> k’ x *)(is safe solution2) (fun x -> if x
if is safe solution2
then (loop (i - 1, solution2)) (fun x -> k’’ x)else k’’ () ) )(j :: solution)) (fun x -> k’ x))x) (fun x -> k x))in(kk ((loop (n, [])) (fun x -> x)) )変換結果の違いは, 以下の３点である.

• 上記のコードでは省略したが, print solution と is safe は pure な関数であるため selective
CPS 変換では CPS に変換されない.
• 従って queen の中からこれらの関数を呼び出す部分も selective な方では直接形式で呼び出す.
• loop 関数は selective な方でも CPS 変換されているが, queen 関数自体は CPS 変換されていない. これは loop 関数の定義は pure であり, loop 関数の呼び出しも reset の中に入っている
ため pure であることが理由である.
最後に queen 関数の呼び出し部分を比べる. 全てを CPS 変換する方では (queen n) (fun x ->x) となるが, selective な方では queen n となる. これは queen が pure と判定されたためである.

15

6

ライブラリ関数の導入

CPS 変換の結果は shift/reset を含まないプログラムになるため, OCaml など一般の処理系で実行できる. このことから, OCaml に既に存在するライブラリ関数の使用を考えることができる.
ライブラリ関数を使うには２通りの方法が考えられる. １つは, ライブラリ関数は CPS 形式では書
かれていないため, 全て pure とする方法である. 例えば List.map は (t1 → t2 ) → t1 list → t2 listという型を持つが, これに次のような pure な注釈を付ける.
Γ ⊢ map : ((t1 → t2 @cps[t3 , t3 , ϵ]) → (t1 list → t2 list @cps[t4 , t4 , ϵ]) @cps[t5 , t5 , ϵ]) @cps[t6 , t6 , ϵ]
このようにしておくと, List.map は必ず pure となり, 従って OCaml の List.map をそのまま使うことができるようになる. この場合, 制約解消の段階で ( ≤ ) の右側に ϵ が入ることが起こり得る.
もう１つは, List.map を定義し直して, 本稿の型システムで型を付け直す方法である. このようにすると List.map に impure な関数も渡せるようになるが, OCaml に用意されている List.map を使うことはできなくなる.

7

関連研究

Rompf ら [13] は本稿と異なり, selective CPS 変換をするための注釈をユーザが与えるように定義している. そのため, ユーザが適切な注釈を与えた場合, 対象言語の「最善の解」や「極大の解」を得られる. その代わり, 複雑なプログラムであると, ユーザが注釈を自力で付けることが困難な場
合がある. 本稿は, 制約解消法を定義しているため, 「最善の解」や「極大の解」を得られない場合がある代わりに, 注釈を自力で付けるというユーザの負担を軽くしている.
Kim and Yi and Danvy [7] は, 本稿が shift/reset が影響する部分だけを CPS 変換するのに対し,例外が起こる箇所だけを CPS 変換するという selective CPS 変換を定義した. また, Reppy の local
CPS 変換 [12] は, 直接形式であるプログラム中の, 特定の関数呼び出しのみを CPS 変換することにより, ネストしたループ等のコンパイル結果の効率を上げる.
Danvy and Hatcliﬀ [5] は, call by name のプログラムの CPS 変換を定義した. まず, strictness
analysis によって call by name の影響を受ける箇所に注釈を付け, 注釈に沿ってプログラムを遅延評価を含む call by value のプログラムに変換する. そして, 遅延評価を含む call by value のプログ
ラムの CPS 変換をする. これは selective CPS 変換ではないが, 本稿と同じように, 注釈に沿ってプ
ログラムを selective に変換する.

8

まとめ
本稿では shift/reset を含むプログラムの selective CPS 変換を定義した. 具体的には以下を行った.

• プログラムに CPS 変換が必要かどうかの情報を注釈として含む型規則を定義した.
• 型推論で生成された制約に対する, 制約の解消法を定義した. この規則は, 過度に型推論と制約解消を複雑にすることなく, ある程度の解を得られるものである.
• 注釈が付いた項に対する selective CPS 変換を定義した.
ユーザの視点からみると, ユーザは注釈が付いていないプログラムを本研究が提案するシステムに入力すれば, システムが自動で注釈を付ける. そしてプログラムの selective CPS 変換の結果が出力として得られる.
今のところ, 最善の解が得られない例は, 一般的にはあまり使わない. よって現時点では, 制約解消の性能を上げても, 一般的なプログラムの性能はさほど上がらない. ただ, 我々は限られたプログ

16

map

ラムしか考察できていない. そのため, 本稿の制約解消法よりも強力な制約解消法が必要なプログ
ラム, その中でも特に一般的なものを探すことは, 今後の課題である.
また, 制約解消法を考える上で, プログラムの中で CPS 変換をするかしないかで大きく実行時間が変わる箇所, つまり注釈の判断がシビアな箇所を断定することは大切である. 現段階でそのような箇所の断定には至っておらず, 今後の課題である.
なお, selective CPS 変換の前後を比べると, 構文は異なるが同じ意味のプログラムになっており,
実行速度以外にも, 検証を通るかなど変換の前後で違う結果を出すものは色々あり得る. このことから, selecitve CPS 変換の潜在的な応用例を本稿で述べたもの以外で見つけることも今後の課題である.

謝辞
本研究において, 筑波大学の亀山幸義教授に, 熱心なご指導と多くのご助言を頂きました. 深く感謝致します. また, 国立情報学研究所の対馬かなえ助教に, 本研究において非常に重要である, 第 3.5
節の最も良い解が存在しない例を考案して頂きました. 深く感謝致します. そして, 多くの有益なコメントを下さった査読者の皆様に深く感謝致します.

参考文献[1] Appel, A. W.: Compiling with Continuations, Cambridge University Press, 1992
[2] Asai, K. and Kameyama, Y.: Polymorphic Delimited Continuations, 5th Asian Symposium on Programming Languages and Systems (APLAS 2007), pp.239–254, November 2007
[3] Danvy, O. and Filinski, A.: Abstracting control, the 1990 ACM Conference on Lisp and Functional
Programming, pp.151–160, 1990
[4] Danvy, O. and Filinski, A.: Representing Control : a Study of the CPS Transformation, Mathematical
Structures in Computer Science, Volume 2, Issue 4, pp.361–391, December 1992
[5] Danvy, O. and Hatcliﬀ, J.: CPS transformation after strictness analysis, ACM Letters on Programming
Languages and Systems, Volume 1, Issue 3, pp.195–212, September 1992
[6] Gasbichler, M. and Sperber, M.: Final Shift for Call/cc: Direct Implementation of Shift and Reset
Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’02),
pp.271–282, October 2002
[7] Kim, J. and Yi, K. and Danvy, O.: Assessing the Overhead of ML Exceptions by Selective CPS
Transformation, the 1998 ACM SIGPLAN Workshop on ML, pp.103–114, September 1998
[8] Kiselyov, O.: Delimited Control in OCaml, Abstractly and Concretely, System Description Functionaland Logic Programming (LNCS 6009), pp.304–320, April 2010[9] 増子 萌: MinCaml コンパイラにおける shift/reset の実装, 第１１回プログラミングおよびプログラミン
グ言語ワークショップ論文集, pp.163–177, 2009[10] Masuko, M. and Asai, K.: Caml Light + shift/reset = Caml Shift, Theory and Practice of Delimited
Continuations (TPDC 2011), pp.33–46, 2011[11] Nielsen, L. R.: A Selective CPS Transformation, BRICS Research Report RS-01-30, Department ofComputer Science, Aarhus University, 2001[12] Reppy, J.: Local CPS conversion in a direct-style compiler, the Third ACM SIGPLAN Workshop on
Continuations (CW’01), pp.13–22, January 2001[13] Rompf, T. and Maier, I. and Odersky, M.: Implementing First-Class Polymorphic Delimited Continuations by a Type-Directed Selective CPS-Transform, The 2009 ACM SIGPLAN International Conference
On Functional Programming, pp.317–328, 2009[14] 上原 千裕: 限定継続命令 shift/reset の Selective CPS 変換, お茶の水女子大学修士論文 (to appear), 201717