Vol. 48

No. SIG 0(PRO 34)

情報処理学会論文誌：プログラミング

2007

階層化コントロールオペレータに対する型システムの構築
鈴 木 輝 信†亀 山 幸 義†本論文は，関数型プログラム言語におけるコントロールオペレータを対象とし，これに対する型シ
ステムの構築とその性質について述べる．本論文で対象とする shift/reset は，限定継続を操作するコントロールオペレータであり，その意味が CPS 変換に基づいて厳密に定義されているため，形式的に扱いやすいという特徴がある．shift/reset は様々な制御構造を表現できるが，複数の異なる目的
で shift/reset を用いると，それぞれの shift/reset が干渉しあい，プログラマの意図通りにプログラ
ムが実行されない場合がある．そこで，それぞれの shift/reset を区別するため，shift/reset に自然数のレベルを付与して階層化することが提案されている．
階層化 shift/reset に対して，これまで，型システムやその性質について十分には検討されておらず，ML などの型をもつプログラム言語に階層化 shift/reset を直接導入することはできなかった．
我々は，先行研究において，レベル 2 の shift/reset の型システムを構築したが，この方式では，1つの項の型付けにおいて，レベルの指数関数の個数の型を必要とするため，レベル 3 以上の型システ
ムに拡張することは困難であった．
本論文では，任意レベルの階層化 shift/reset に対する型システムを提案し，型システムの健全性などの望ましい性質が成立することを示す．これにより，型があるプログラム言語に階層化 shift/resetを導入できるようになると考えられる．

Construction of a Type System for Layered Control Operators
Terunobu Suzuki† and Yukiyoshi Kameyama†
We construct a type system for control operators in functional programming languages.
Speciﬁcally, we treat the layered version of the control operators shift and reset whose semantics is deﬁned in terms of (iterated) CPS translations. While shift and reset are capableof representing various control structures, we cannot have two or more diﬀerent uses of shift
and reset in a single program since they may interfere with each other. In order to avoid thisinterference, shift and reset should be layered, that is, we should assign to each occurrence ofshift and reset a natural number which designates its level.
Although it is apparent that a sound type system for layered shift and reset is necessary
to introduce them to practical programming languages, no work has ever tried to construct
a suﬃciently expressive type system for them. In this paper we reﬁne our previous work
which solved this problem for the case of level-2, and propose a type system for an arbitrarylevel. We show that desirable properties such as type soundness hold for this type system,
which enables one to introduce the layered shift and reset to statically typed programming
languages.

本研究が対象とする

1. は じ め にshift/reset

は，様々な制御

構造を表現できる コントロールオペレータであり，「継☆

コントロールオペレータは，関数型プログラムの制続」(continuation) すなわち「計算の残り」を表す概念

御を行うための言語プリミティブであり，様々なプロをプログラマが直接操作できるようになる．shift/reset

グラム言語に含まれている．例えば，例外 (Standard

は，CPS 変換に基づいて意味が定義されているため，

ML の exception, Java の try-catch-ﬁnally など)，第形式的に扱いやすく，近年，盛んに研究が行われてい一級継続 (Scheme や Standard ML/NJ の call/cc)

る?),?) ．shift/reset を含む計算体系に対する型システ

が，これに該当する．

ムとしては，Danvy と Filinski?) が提案したものがある．彼らの型システムでは，項の型付けの判断に，項† 筑波大学システム情報工学研究科コンピュータサイエンス専攻
Department of Computer Science, Graduate School of
Systems and Information Engineering, University ofTsukuba☆

1

Filinski?) は，一定の条件のもとで，任意の制御効果 (control
eﬀect) が shift/reset を用いて表現できることを示した．

2

情報処理学会論文誌：プログラミング

2007

そのものの型だけでなくその継続の型を加えている．

Scheme 等のプログラム言語における call/cc がある．

shift/reset を複数の異なる目的で利用した場合にそcall/cc は，継続を変数に束縛するため，継続をプログ

れぞれの shift/reset の計算が干渉しあって，プログラ

ラム中で利用することができる．call/cc と shift/reset

マの意図通りに実行さわれないことがある．これを解の違いは，call/cc が獲得する継続はプログラムが終了決するために階層化 shift/reset ?) が提案された．階層

するまでの計算全てであるが，shift/reset が獲得する

化 shift/reset は，階層化されない shift/reset と同様

継続は，プログラムが終了するまでの計算の一部分にに，その意味が CPS 変換により厳密に与えられていできることである．後者の継続を限定継続 (delimited

るという利点があるが，その複雑さのため，型システ

continuation) と呼び，より精密にプログラムを制御

ムやその性質に関しては十分には検討されてこなかっすることができる．

た．階層化 shift/reset に対する型システムは，型のあshift オペレータは，k を変数，M を式とするとき，る言語への導入のためだけではなく，型によってプロ

Sk.M という形で表現される．この式はその (限定) 継グラムを抽象化することによりプログラムの理解を助

続を k に束縛して，M を計算するという式である．一けるという効果もある．我々は階層化 shift/reset に方，継続を束縛する際にその範囲を限定するのが reset

対する型システムについて研究しており，先行研究であり hM i と表す．shift で継続を捕捉する際には，においてレベル 2 の階層化 shift/reset に対して型シ

reset までの範囲の継続が対象となる．

?)

ステムを提案した．しかし，この型システムでは，1これらの式の意味を以下の例で考える．

h2 + Sk.(3 + 4)i + 1

つの型判断が，レベルの指数関数の個数の型を必要とし，この多数の型を適切に記述する記法がなかったた=(3 + 4) + 1 = 8
h2 + Sk.(3 + (k(k4)))i + 1

め，レベル 3 以上の階層化 shift/reset に対応するのは難しかった．

=(3 + (2 + (2 + 4))) + 1 = 12

本研究では，型スキームと呼ばれる記法を導入する

最初の式は，shift で捕えた継続を利用しない場合であことにより上記の問題点を克服し，任意のレベルのる．Sk.(3+4) を実行する際の残りの計算は，h2+[ ]i+1

shift/reset に対する型システムを提案する．さらに，

であるが，shift が捕える継続は最も近い reset まででこの型システムが型の健全性や CPS 変換による型の保あるため，h2 + [ ]i (2 を加える) という継続 (を関数

存など，型システムとして必要とされる良い性質を満で表現したオブジェクト) が k に束縛される．次に，たすことを証明する．これにより，階層化 shift/reset

shift の内側の計算 (3 + 4) を行い，この部分の計算がを静的な型システムをもつ言語に導入できるようにな終わると reset の継続 ([ ] + 1) に飛ぶ．結果として，2ると考えている．

を加える部分は実行されず，8 という計算結果を得る．

本 論 文 の 構 成 は 以 下 の 通 り で あ る ．??章 で は ，

2 つ目の式は，shift の内側の計算で k を利用した場

shift/reset の概要と階層化について述べる．??章で合である．k には，「2 を加える」という関数が束縛さは，対象とする λ 計算に階層化 shift/reset を追加しれており，この計算を 2 回行った後に 3 を足す．このた言語 λSm と CPS 変換の定義を与えた後，本論文時点で shift の内側の式の計算が終わったので，resetが提案すると型システムの形式的な定義を述べる．??

の外側に飛んで残りの計算を行い，計算結果は 12 に章では，本論文のた型システムが満たす性質を示し，なる．

??章で，まとめと今後の課題を述べる．

2. shift/reset と階層化
この章では，shift/reset の概要，簡単なプログラム
例，階層化の必要性について述べる．

2.2 shift/reset の階層化
階層化 shift/reset は，前節の shift/reset に自然数のレベルを割り当て，使用目的の異なる shift と resetを区別できるようにしたコントロールオペレータである?) ．階層化した shift は Sn k.M , reset は hM in と

2.1 コントロールオペレータ shift/reset

いう形になり，それぞれの n がその shift, reset のレ

前章で，shift/reset は継続を扱うためのコントロー

ベルになる．

ルオペレータであると述べた．継続は，対象となる式

階層化 shift/reset の例を以下に示す．

の計算後からプログラム終了までの計算を表す概念で

1 + h h (S2 k. k(k1)) + 3i1 + 2i2あり，shift/reset はこの継続をプログラムの中から利もし，この式の shift/reset のレベルが無いとする用する機構を与える．

と，k に束縛される継続は 3 を足す部分だけなので，これと同様のコントロールオペレータとして，

1 + (((1 + 3) + 3) + 2) = 10 になるが，この場合，shiftVol. 48

No. SIG 0(PRO 34)

階層化コントロールオペレータに対する型システムの構築

3のレベルが 2 なので，レベルが 1 の reset を無視して，

言語 λSm を形式的に定義し，さらにその CPS 変換

外側のレベルが 2 の reset までの継続を捕えることにと本論文で提案する型システムについて述べる．

なり，計算結果は 1+((1+3+2)+3+2) = 12 になる．

3.1 構文と評価

この例ではレベル 2 までしかないが，一般に n > 0 な

m を正の自然数とする．本論文が対象とする言語

る任意の自然数に対して，レベル n の shift/reset が

λSm は，λ 計算に m 以下のレベルの shift と reset を定義される．

追加した言語である．λSm の項 M と値 V は以下の2.3 階層化 shift/reset の例

ように定義される．

階層化 shift/reset の利用法を説明するため，文献?) の例を取り上げる．まず，非決定的な計算を行うプ

M ::= x(変数)

ログラムを shift/reset で表現したものを以下に示す．

| λx.M(λ-抽象)

ﬁlp(x) = S1 k.(k(true); k(false); fail( ))| M1 M2(適用)

fail(x) = S1 k.“no”| Sn k.M(shift, 1 ≤ n ≤ m)

| hM in(reset, 1 ≤ n ≤ m)choice(n) = if n < 1 then fail( )else if ﬁlp( ) then choice(n − 1)else nここでは任意の値であり，a; b は式 a と式 b を順番に実行して b の値を結果とする式である．

V ::= x| λx.M
Sn k.M はレベル n の shift を用いた項であり，この項の中で，変数 k が束縛される．shift が獲得する継このような関数を定義し，hprint(choice(3))i1 とい続の範囲を限定するのが reset であり，hM in と表現

うプログラムを実行すると，1,2,3 がこの順で印刷さされる．変数は λ あるいは Sn により束縛され，α 同れる．すなわち，関数 ﬂip は非決定的選択を実現する

値性や代入 M {x := M 0 } は，通常のラムダ計算と同関数である．

様に定義する．また，α 同値な項は同一視する．

次に，生成された数を収集するための関数を以下のように定義する．

次に，λSm に対する文脈を 3 種類導入する．

C ::=[ ] | λx.C | M C | CM | hCin | Sn k.Cemit(n) = S1 k.cons(n, k(nil))(文脈)例えば，hemit(1); emit(2); emit(3)i1 という計算を行E ::=[ ] | V E | EM | hEin

うと自然数のリスト [1; 2; 3] を返す．
そこで，hemit(choice(3))i1 とすると，自然数のリ(評価文脈)
E n ::=[ ] | V E n | E n M | hE n ii

(i < n)スト [1; 2; 3] を返すことを期待する．しかし，実際に(レベル n の評価文脈)

計算してみると，[1], [2], [3] という別々のリストは生

C は一般の文脈であり，[ ] は穴 (hole) を表す．E は成されるが，これらが収集されて一つのリストになる

値呼び計算戦略における評価文脈である．ただし，穴ことはない．

を取り囲む reset があってもよいように拡張している．

このように，shift/reset を用いた関数を複数組み合

E n は，穴を囲む reset のレベルを n より小さいレベ

わせることにより，これらが干渉して意図通りにプロルに制限した評価文脈であり，次に述べる shift の評

グラムが動かなくなってしまうことがある．そこで，

価規則において利用する．文脈 C に対し，C[M ] は文

階層化 shift/reset を用いて，emit の定義を以下のよ

脈 C の穴を項 M で埋めた項をあらわす．

うに変更する．

emit(n) = S2 k.cons(n, k(nil))hemit(choice(3))i2 を実行すると，期待通り [1; 2; 3]というリストが返る．

λSm の評価規則を次に示す．ただし，n ≤ j とする．
E[(λx.M )V ] → E[M {x := V }]E[hE n [Sn k.M ]ij ] → E[hM {k := λx.hE n [x]in }ij ]E[hV in ] → E[V ]階層化していない shift/reset を複数用いる場合，最初の規則は，値呼び λ 計算の通常の β 簡約である．

shift/reset 同士の干渉は容易に起きる問題であり，そ2 番目の規則は shift の計算を表すもので，shift かの解決のために階層化することは，現実のプログラミ

ら見て一番内側の reset(ただし，reset のレベルは n 以

ングを行う際には非常に重要であると考える．

上) までの継続 E n を捕捉し，それを関数 λx.hE n [x]in

3. 階層化 shift/reset の形式化と型システム
この章では λ 計算に階層化 shift/reset を追加したに変形して変数 k に束縛する．レベル n の shift が獲得する継続は，レベル n 以上の reset によって限定されるので，n ≤ j という条件がついている．たとえば，

情報処理学会論文誌：プログラミング

4

2007

hE 2 [hE 1 [S2 k.M ]i1 ]i2 という式における S2 が獲得す

去することができ，通常の CPS 変換を 1 回行って得る継続は，外側のレベル 2 の reset までである．

られる項と同じである．shift は 1 個目から n 個目まnk に束縛される関数として λx.hE [x]in のかわりにでの継続をまとめて k に割り当てて，M の 1 個目かλx.E n [x] を採用すると，shift/reset とは意味が異なら n 個目までの継続は初期化される．また，reset でる control/prompt と呼ばれるコントロールオペレー

は 1 個目から n 個目の継続を n + 1 個目の継続にま?)タになる ．control/prompt は，部分継続を表現す

とめる．これにより，レベルが n 以下の shift では継る最初のコントロールオペレータであるが，その意味

続が束縛されない．

論が shift/reset より複雑であったことを一因として，
今日では shift/reset が主に使われている．
評価規則の最後のものは，reset の内側の項が値になった場合に，その reset を除去する規則である．

3.3 先行研究の型システム
本研究の型システムについて述べる前に，先行研究の shift/reset に対する型システムについて述べる．

Danvy と Filinski は文献?) において，階層化して3.2 CPS 変換

いない shift/reset に対する型システムを与えた．彼

CPS 変 換 は ，プ ロ グ ラ ム を CPS(Continuation

らの型システムでは，項の型を考える際に継続の型を

Passing Style) とよばれる特別な形式に変換するプ

考慮するものであり，型判断は以下の形をしている．

ログラム変換である．CPS 形式のプログラムは，計算Γ, α ` M : τ, βの途中結果全てに名前が付けられ，全ての関数呼出し

Γ は型環境，M は項，τ, α, β は型である．これは，Mが末尾呼出しであるという特徴があり，理論的な解析の継続の型が τ → α である時に，計算結果の型は βやコンパイラの中間言語等で幅広く利用されている．

であることを表す．shift/reset が無ければ α = β でλSm のプログラムに対する CPS 変換は，通常のあるが，shift/reset を導入すると，α 6= β のことがあCPS 変換を m + 1 回繰返すことで与えられる?) ．レベ

る．この型システムの shift と reset の型付け規則は

ル n の shift/reset に対して CPS 変換を行うと，レベ以下の通りである．

ルが n − 1 である shift/reset に変換され，特に n = 1の時は，CPS 変換により shift/reset が消去され，純粋なラムダ項になる．そこで，λSm のプログラムにΓ[k 7→ (τ /δ → α/δ)], σ ` M : σ, β
shift
Γ, α ` Sk.M : τ, β

対して，m + 1 回☆ CPS 変換を繰返すことにより，純粋なラムダ項になる．この繰返し全体を 1 つの変換としたものが CPS 変換 Cm+1 であり，その定義を図??

Γ, σ ` M : σ, τresetΓ, α ` hM i : τ, αで与える．
図??でわかるように，この CPS 変換は，m + 1 個

shift の規則では，k の型は関数型であり，その引数の継続変数 κ1 , · · · , κm+1 を受け取って変換後の項をの型が τ ，関数本体の継続の型が α → δ, 計算結果の生成している．κ2 をメタ継続と呼び, κ3 をメタメタ

型は δ である．この規則を見ると，shift の継続の型

継続等と呼ぶ. この CPS 変換は，型のない λSm の項

τ → α を k の型として割り当て，M の継続の型が全体に対して定義され，CPS 変換後の項は再帰型を

σ → σ となっており，M の継続が初期化されている

利用して型をつけられる．図??の上部にその型を記述ことが分かる．reset の規則では，reset の型 τ を M

した．Cm+1 は，変換前の項 (型は Term) と m + 1の結果の型として，shift で捕える範囲外にして，M個の継続 (型は Cont i ）を受けとり，Answer 型の値の継続の型は σ → σ として初期化している，と見るを返す関数である．変換前の項に型がないことに対応ことができる．このように見ると，shift/reset の計算

して，値の型 Val の定義式で再帰型が現れている☆ ．

が型の上で表現されていることが分かる．

shift と reset 以外の項に対する CPS 変換においては，メタ継続など 2 個目以降の継続を η 変換により消☆

m 回の CPS 変換で，階層化 shift/reset を全て消すことができるが，CPS 形式にならないため，さらにもう 1 回余分に変換を行っている☆
Val の定義の右辺に Val が negative な位置に出現している．
変換前の項に本論文で述べる型が付いている場合は，変換後に再帰型は必要なく，単純型付きラムダ計算の範囲内で型が付けられる．

Murthy?) は，階層化 shift/reset に対する型システ
ムを与えた．彼の型システムでの型判断は

Γ ` M : Kα [T ]という形である．ただし，α は型の列 αm . . . α1 の略記であり，Kα [T ] は以下のように定義される．

K[] [T ] = T
Kατ [T ] = (T → Kα [τ ]) → Kα [τ ]Vol. 48

No. SIG 0(PRO 34)

階層化コントロールオペレータに対する型システムの構築

5

Cm+1 : Term → Cont 1 → . . . → Cont m+1 → Answer
κi ∈ Cont i = Val → Cont i+1 → . . . → Cont m+1 → Answer(1 ≤ i ≤ m)

κm+1 ∈ Cont m+1 = Val → Answer
Val ::= Val → Cont 1 → . . . → Cont m+1 → Answer(x は変数)

Cm+1 [[x]] = λκ1 . . . κm+1 . κ1 xκ2 . . . κm+1

Cm+1 [[λx.M ]] = λκ1 . . . κm+1 .κ1 (λvκ01 . . . κ0m+1 .(Cm+1 [[M ]]{x := v})κ01 . . . κ0m+1 )κ2 . . . κm+1
Cm+1 [[M1 M2 ]] = λκ1 . . . κm+1 .Cm+1 [[M1 ]](λf κ02 . . . κ0m+1 .
Cm+1 [[M2 ]](λaκ002 . . . κ00m+1 .
f aκ1 κ002 . . . κ00m+1 )κ02 . . . κ0m+1 )κ2 . . . κm+1
Cm+1 [[hM in ]] = λκ1 . . . κm+1 .Cm+1 [[M ]]θ1 . . . θn(λvκ0n+2 . . . κ0m+1 .θ0 vκ1 . . . κn+1 κ0n+2 . . . κ0m+1 )κn+2 . . . κm+1
Cm+1 [[Sn k.M ]] = λκ1 . . . κm+1 .(Cm+1 [[M ]]{k := p})θ1 . . . θn κn+1 . . . κm+1
ただし，

p = λvκ01 . . . κ0m+1 .θ0 vκ1 . . . κn (λwκ00n+2 . . . κ00m+1 .θ0 wκ01 . . . κ0n+1 κ00n+2 . . . κ00m+1 )κ0n+2 . . . κ0m+1
θi = λvκi+1 . . . κm+1 .κi+1 vκi+2 . . . κm+1

(0 ≤ i ≤ m)

θm+1 = λv.v
図 1 λSm の CPS 変換
Fig. 1 CPS-translation for λSm
表 1 先行研究との比較
Table 1 Comparison of our work and previous work

Answer Type の変化
非対応
階
層
化

対応

2 種類の継続の型と結果の型を含む必要があったため，以下の形になっている．

Γ; α1 , α2 , α3 ` M : τ, β1 , β2 , β3
項 M の 1 個目の継続の型が τ → (α1 → α2 ) → α3

非対応Filinski の実装 (1994)

対応

Murthy (1992)

Danvy,Filinski(1989)

であり，2 個目の継続の型が β1 → β2 , 結果の型は β3となる．例として，この型システムにおけるレベル 2

本研究の型システム

例として m = 1 の場合は，

Γ ` M : (T → α1 ) → α1となる．この例からわかるように，上記の Danvy-

Filinski の型システムに比べ，継続の返す型と計算結果の型が同じという制約が加わっている．これらの型が異なるような項 (いわゆる Answer Type が変化する項) に対して，Murthy の型システムでは型をつけることができない．ML における printf の型付け?)を shift/reset で表現した場合など，興味深いプログ
ラムで，Murthy の制約のもとでは型付けができないものが存在するため，より多くの項を型付けできる型システムが必要である．
これらの先行研究と今回提案する型システムの関係を表??にまとめる．
これまで我々は，Danvy-Filinski の型システムを拡張し，レベル 2 の階層化 shift/reset に対応した型シ
ステムを構築した?) ．型判断は，レベル 2 に対応しての shift に対する型付け規則をあげる．

Γ0 ; γ1 , γ2 , γ2 ` M : γ1 , γ3 , γ3 , βshift2Γ; α ` S2 k.M : τ, α1 , α2 , β
ただし，Γ0 = Γ[k 7→ (τ /δ → α3 /δ)] とする．
このようにして，レベル 2 の shift/reset に対応した型システムを構築したが，これをレベル n まで単純に拡張すると型判断に含まれる型の個数が非常に多くなり，型付け規則を表現することだけでも簡単なこと
ではなくなってしまう．レベル 1 で 3 個, レベル 2 で7 個の型が必要であり，一般にレベル n の型システム
では，必要な型の個数が O(2n ) となる．型の爆発をおさえるには，これらの多くの型を適切に表現する記法が不可欠である．

3.4 λSm に対する型システム
本研究では，型システム構築にあたって，以下の原則を設定した．

• 型 シ ス テ ム の 健 全 性 (Subject Reduction とProgress) が成立すること．
• 意味をもつ項は，できる限り多く型付けできるこ情報処理学会論文誌：プログラミング

6

2007

と．少なくとも応用上，有用な項は型付けできる以上の深さの型の構造を記述する必要はないという事こと．

実に基づき，複雑な型を ∗ を使って簡潔に記述するた第一の要求は，静的な型システムをもつプログラム
言語のコアとなる体系を目指している以上，当然のこめに使われる．
型スキーム T に対して T [l] は左部分木，T [r] は右部分木を表す．また，T [r l ] を以下のように定義するとであろう．
第二の要求も当然のことであるが，「意味をもつ項」(T [ll ] も同様に定義する)．

が何かについては検討を要する．階層化 shift/reset のT [r0 ] = T

意味は，CPS 変換により与えられており，CPS 変換

T [rl ] = (T [rl−1 ])[r]n(l > 0)nをほどこした後の項は，通常の (shift/reset のない)型スキーム T と s = l, r, l , r

ラムダ項になる．そこで，我々は，「項 M を CPS 変

分木 T [s] を型スキーム S で置き換えた型スキームを換したときに，単純型付きラムダ計算の項になる (単T [s ← S] と表記する. よく現れる型スキームの略記~ を以下のように定義する．たとして init(n,T , ~γ ,S)

純型付きラムダ計算で型が付く) こと」を「項 M が意味をもつ」ことと定めた．
この考え方は，Danvy-Filinski の型システムにおける考え方と同じであるが，上述したように，shift/resetの型システムに関する既存の研究の多くは，この要求を満たしていない．本論文で提案する型システムは，に対して，その部

だし，0 ≤ n ≤ m, T は型スキーム, ~γ は n 個の型~ は n 個の 型スキーム S1 , · · · , Sn
γ1 , · · · , γn の列，Sの列である．

~ =T
init(0, T, ~γ , S)
~ =init(n + 1, T, ~γ , S)

れまで考えられてきたプログラム例を (我々が試みた~ 0 ))(γ1 ,(γ1 , S1 , S1 ), init(n, T, ~γ 0 , S~ の先頭要素を
ただし，~γ と S は，それぞれ ~γ と S

範囲では) すべて型付けできるという意味で既存の研取り除いた列である．後に述べる型付け規則において既存の研究で型付けできる範囲を全て含んだ上で，こ究より強力である．

0~0

init を使うときは，第 3, 第 4 引数は，型や型スキー

3.4.1 型と型スキーム

ムをあらわすフレッシュなメタ変数の列を取る．これ

本論文では，レベル m の shift/reset に対する型シは，レベル n の shift や reset の型付けにおいて，レ

ステムを表現するため，型スキーム を導入した．これ

ベル n 未満の部分は，(γ, (γ, S, S), ) の形であること

は，複数ある継続の型を木構造で表現するとともに，を意味する．

必要以上に型情報を型判断に加える必要が無い工夫を型スキームの例を図??に示す．ここで，a, b, c, d, γi加えたものである．また，shift/reset の型付け規則がは型，A, B, C, D, X, Si は 型スキーム, T [r] は T の

λSm の m によらず同じ形である，という特徴を持っ

右の部分木を，T [r 2 ] はそのさらに右部分木を取る操ている．

作である．また，T [r ← X] は T の右部分木を X に型 τ と型スキーム T を以下のように定義する．

τ ::= b
|τ →T
T ::= ∗(基本型)

X に置き換えた木を表す．init(2, X, , ) は図??のよ(関数型)

うな木を構成する．init の第一引数が大きくなると，(基本型スキーム)| (τ, T1 , T2 )置き換えた木を表し，同様に T [r2 ← X] は T [r2 ] を(3 つ組)

木がより下へ伸びることになる．

3.4.2 型付け規則

型スキームにおける 3 つ組 (τ, T1 , T2 ) は，2 分木

本研究で提案する λSm に対する型システムの型判を表現しており，木の根は型 τ であり，左部分木は断と型文脈を，それぞれ以下のように定義する．ただT1 , 右部分木は T2 である．これは，直感的には，CPS

し，M は項，T は型スキーム, x は変数，t は型である．

変換により，(τ 0 → T10 ) → T20 と変換される型を表Γ`M :T0

現したものである. (ただし，τ 等は τ 等を CPS 変

Γ ::= [ ] | Γ[x 7→ τ ]換して得られる型である). 型スキーム ∗ は，“don’t

型判断 Γ ` M : T は，型環境 Γ 下で項 M の型スキー

care” を意図した定数であり，Answer Type (図??のムが T であることを表す．

型 Answer ) を含む任意の型に CPS 変換される型を表

型付け規則の定義を図??に与える．

現している．すなわち，n 未満のレベルの shift/reset

図??において, shift と reset の規則で現れる init

しか持たないプログラムを型付けするとき，(厳密には，n 番目までの継続が初期化されることに対応する

は，さらに，そのプログラムに含まれる自由変数があ型である．shift や reset に対する型スキームが右部分

らわすエフェクトも レベル n 未満であるとき)，n + 1

木と左部分木で共通しているところは，1 番目の継続

Vol. 48

階層化コントロールオペレータに対する型システムの構築

No. SIG 0(PRO 34)

T = (a,(b,A,B),(c,C,D)) T[r

7

X]=
a

a
b
T =

c

b

A
A

B C

B

D
T[r

X ]=
a

T[r] =
C

S1

D

S1
S2

D

A

γ2

X

c

b
T[r ] =

γ2

γ1
2

c

2

init(2,X,γ,S)=
γ1

X

B C

S2

X

図 2 型スキームの例
Fig. 2 Examples of Type Scheme

Γ(x) = τvarΓ ` x : (τ, T, T )Γ[x 7→ τ ] ` M : TλΓ ` λx.M : (τ → T, S, S)

Γ ` M1 : (α → (τ, T, S), U, W ) Γ ` M2 : (α, S, U )appΓ ` M1 M2 : (τ, T, W )~Γ ` M : init(n, (τ, T [rn ], S), ~γ , S)
resetn , n ≤ mnΓ ` hM in : (τ, T, T [r ← S])0~Γ ` M : init(n, U [rn−1 ], ~γ , S)Γ ` Sn k.M : (τ, U [rn−1 ← (α, T, S)], U )shift n , n ≤ m0

Γ = Γ[k 7→ τ → (α, W [rn ← T ], W [rn ← S])]
図 3 型付け規則
Fig. 3 Typing Rulesに 2 番目以降の継続を適用できることに対応している．

3.4.3 型付けの例
前節で定義した型システムを用いて，実際のプログ
ラムの型付けを行った例を示す．ここで型付けを行ったプログラム M は以下のものである．

まず，関数 choice に対して次の型が導出できる．

` choice : (int → (int,(string, T, T ),(string, T, T )), T, T )この時，図??に示す導出により，` M : (list int, U, U )M = hhemit2 (choice 3); “no”i1 ; nili2が導出できる．ただし，list int は自然数のリスト型

choice は?? 節で定義した関数であり，emit2 はレベであり，U は任意の型スキームである．この導出にル 2 の shift を用いた emit を表している．ここでは，おける emit2 の本体の型を見ると，深さ 1 の Answer

整数などの基本型や if-then-else 等に対する型付け規Type (string) と深さ 2 の Answer Type (list int) が則が適宜追加されていると仮定する．

異なっており，階層化 shift/reset に対応した型システムであることがわかる．
この例は階層化レベルが 2 であるが，Biernacka らによる Normalization by Evaluation?) は，階層化レ情報処理学会論文誌：プログラミング

8

ベルが 5 の例題であり，我々の型システムはこの例に対しても型がつけられることを確認している．このような例は，実用的なプログラムにおいては頻出するも2007

が，特に問題は生じない．
定理 1 (CPS 変換による型付けの保存) λSm において Γ ` M : T が導けるならば，のと考えられるが，従来研究では型付けすることがで[[Γ]] `λ→ Cm+1 [[M ]] : [[T ]]m+1

きず，本研究による型システムの優位性を示すものでが導ける．ここで，`λ→ は，単純型付きラムダ計算

ある．

λ→ における型の導出である．
定理??は，本論文の型システムで型が付く項は，

4. 型システムの性質

CPS 変換すると λ→ で型が付く項になることを示し

この章では，前章で定義した λSm に対する型シスている．証明は，付録の??節と??節に記載した．

テムに対して望ましい性質が成立することを示す．

定理 2 (CPS 変換による項の等しさの保存) λSm

4.1 λSm と CPS の対応

に対して, Γ ` M : T が導け，さらに M → N であ

前節の型システムが，CPS 変換と整合していることるならば，を示す．すなわち，λSm で型付けされた項は，CPS変換により単純型付きラムダ計算 λ→の項に変換され，また，λSm での計算は，CPS 変換により単純型付きラムダ計算 λ→ における計算に変換されること

Cm+1 [[M ]] =βη Cm+1 [[N ]]である．ここで，=βη は単純型付きラムダ計算 λ→ における βη-equality をあらわす．
証明. 文献?) は，階層化 shift/reset に対する型のfreeない体系 λSmを与え，本論文で述べた CPS 変換にを示す．
型と型スキームに対する CPS 変換を次のように定関して健全かつ完全な等式系を与えた．この等式系の義する．ただし，λSm の基本型は，単純型付きラム

一部は以下の通りである．
（ただし，j ≥ n とし，記法→

ダ計算の基本型であると仮定する．また，X は λは本論文のものに合わせた．
）(λx.M )V = M {x := V }における特定の型を 1 つ選んで固定したものであり，

i ≤ m + 1 とする (i ≥ 0 とは限らない)．

hV in = V→[[ ]]i : 型スキーム→ λ の型{[[∗]]i =hE [Sn k.M ]ij = hM {k := λx.hE n [x]in }ij
nXi ≤ 0 の時

free
これらの等式から，λSm で M → N であれば，λSm(X → [[∗]]i−1 ) → [[∗]]i−1

i > 0 の時

free
で M = N である．さらに，λSmに対する CPS 変[[(τ, T, S)]]i = ([[τ ]] → [[T ]]i−1 ) → [[S]]i−1

換の健全性?) より，型のない純粋なラムダ計算の体系
において，Cm+1 [[M ]] =βη Cm+1 [[N ]] である．この式→[[ ]] : 型 → λ の型[[b]] = b[[τ → T ]] = [[τ ]] → [[T ]]m+1の両辺は，定理??と後述する定理??より λ→ で型付け可能なので，λ→ において Cm+1 [[M ]] =βη Cm+1 [[N ]]である．(証明終わり)

4.2 型システムの健全性→[[ ]] : 型環境 → λ の型環境[[[ ]]] = [ ][[Γ[x 7→ τ ]]] = [[Γ]][x 7→ [[τ ]]]上記の定義で，型スキーム T に対する変換は，i というインデックスを持ち，[[T ]]i という形で与えられている．その理由は，我々の型システムにおいては，型ス

型システムの健全性は，型の保存 (Subject Reduc-tion, Preservation) と計算の進行 (Progress) の 2 つの性質から構成される．
定理 3 (型の保存) λSm の項 M, N , 型環境 Γ, 型
スキーム T に対し，Γ ` M : T が導出できて M → N
であれば，Γ ` N : T が導出できる．

キームが煩雑になるのを避ける工夫として，∗ を使っ

この定理により，項に型が付くならば，その項の実て「任意の型スキーム」を表現できるようにしたが，行中に型エラーが起きないことが保証される．証明はCPS 変換の際にはそのような型 ∗ を展開して，高さ付録??を参照されたい．

m + 1 の木にする必要があるためである☆ ．なお，上記の定義を展開していくと，i < 0 となることもある

定理 4 (計算の進行) λSm の項 M , 型スキーム Tに対して [ ] ` hM im : T が導けるならば，hM im は，評価規則を適用して計算を進めることができる．

☆

CPS 変換の定義からわかるように，CPS 変換後の項は必ず(m + 1) 個の継続を受けとるため，その型を木として見た場合，高さが (m + 1) 以上になる．

この定理で，hM im の形をした項に限定しているのは，reset で囲われていない shift を持つ項は，いわばopen term であり，計算が進まないためである．たとVol. 48

No. SIG 0(PRO 34)

階層化コントロールオペレータに対する型システムの構築

9以下の導出における W と U は任意の型スキーム, T, S, Γ はそれぞれ以下の型スキームと型環境を表す．

T = (list int, (list int, W, W ), (list int, W, W ))S = (string, (list int, W, W ), (list int, W, W ))
Γ = [n 7→ int, k 7→ (list int → (list int, T, T ))]..
..
Π ` choice 3 : (int, S, S)` emit2 (choice 3) : (list int, S, S) ` “no” : (string, S, S)` emit2 (choice 3); “no” : (string, S, S)` hemit2 (choice 3); “no”i1 : (string, T, T )` nil : (list int, T, T )` hemit2 (choice 3); “no”i1 ; nil : (list int, T, T )` hhemit2 (choice 3); “no”i1 ; nili2 : (list int, U, U )Γ ` k : (list int → (list int, T, T ), T, T ) Γ ` nil : (list int, T, T )Γ ` n : (int, T, T )Γ ` k(nil) : (list int, T, T )Π=Γ ` cons(n, k(nil)) : (list int, T, T )[n 7→ int] ` S2 k.cons(n, k(nil)) : (list int, S, S)` emit2 : (int → (list int, S, S), S, S)
図 4 型付けの例
Fig. 4 Example of Type Derivation

えば，S1 k.x は，そのままでは評価が進まない．この体系のプログラムは，自由変数がなく，かつ，プログ
ラム全体がレベル m の reset で囲われているものと定めれば，上記の定理を適用することができる．

5. まとめと今後の課題継続を扱うためのコントロールオペレータである

shift/reset は様々なプログラムの制御を表現できる

上記の定理により，hM im が型が付くならば，その上，形式的に扱いやすいという特徴がある．1 つのプ項の計算が進むことが示される．証明は付録??を参照

ログラムの中で shift/reset を複数の目的に用いると，されたい．

互いに干渉を起こし，意図通りに動作しないことがあこれら 2 つの定理を組み合わせると，次の健全性定理が得られる．
定理 5 (型システムの健全性) λSm の項 M と 型

るため，階層化 shift/reset が提案された．これまで，
この階層化 shift/reset に対する型システムとして十分なものは提案されてこなかった．

スキーム T に対し，[ ] ` hM im : T が導けるなら

本研究は，型スキームのアイディアに基づき，階層化

ば，M は値であるか，あるいは，ある項 N が存在し

shift/reset に対する型システムを与えた．また，そのて hM im → hN im かつ [ ] ` hN im : T が導ける．

性質について検討し，今回定義した型システムが CPS

証明. [ ] ` hM im : T が導けたと仮定すると，定変換と整合し，かつ，健全であることを示した．この理??から，hM im は 1 ステップ計算可能である．M型システムは，階層化 shift/reset と Answer Type のが値でなければ，この 1 ステップの計算によって一番変化の両方に対応した初めてのものである．

外側の reset がなくなることはない．従って，ある N

本研究は，今後さまざまな研究に発展していくことに対して，hM im → hN im となる．さらに定理??かが考えられる．以下では，そのような課題のいくつか

ら，[ ] ` hN im : T が導ける．(証明おわり)に言及する．

静的に型付けされたプログラミング言語にとって，• 型推論: 本研究の型システムは主型 (principal型システムの健全性は必要最低限の性質であり，このtype) を持つ．これに基づき，第 1 著者はこの型性質だけで十分であるとは言えないが，本研究の型シシステムに対する型推論アルゴリズムを実装しステムは，階層化 shift/reset を静的に型付けされたプた?) ．しかし，これはプロトタイプ実装であり，ログラム言語で用いるための基礎となると考えられる．

本格的プログラムに対する有効性の検証は今後の情報処理学会論文誌：プログラミング

10

課題である．

• 多相性との共存: 多相型と call/cc などの副作用が共存すると，型の健全性に問題が生じることが古くから論じられており，ML 言語では多相性を制限する方法が取られている．本論文の shift/resetについても同様の制限のもとで多相性と共存できると予想している．また，ソース言語の多相性だけ
でなく，CPS 変換後の多相性 (いわゆる Answer

Type 多相性) との関連も興味深い課題である．
• 強正規化性:
本論文では，停止性 (強正規化可能性) について議論することができなかった．これは，いわゆる管理レデックス (CPS 変換の際に生じるレデックス) を生成しない CPS 変換を定義することにより証明できるという見通しを持っており，検討中

2007(2003).
9) Kiselyov, O., c. Shan, C. and Sabry, A.: Delimited Dynamic Binding, Proc. International
Conference on Functional Programming, pp.
26–37 (2006).
10) Murthy, C.: Control Operators, Hierarchies, and Pseudo-Classical Type Systems:
A-Translation at Work, Proc. First ACM
Workshop on Continuations, Technical Report
STAN-CS-92-1426, Stanford University, pp.
49–72 (1992).
11) 鈴木輝信：階層化コントロールオペレータに対する型システムの構築，修士論文，筑波大学大学
院システム情報工学研究科 (2007).
12) 鈴木輝信，亀山幸義：階層化コントロールオペ
レータに対する型システムの構築，日本ソフト
ウェア科学会第 23 回大会講演論文集, 8 ページ(2006).

である．
謝辞 第 2 著者は，科学研究費補助金 基盤研究 (C)(No. 16500004) の援助を受けている．

参

考 文

献

1) Biernacka, M., Biernacki, D. and Danvy, O.:
An Operational Foundation for Delimited Continuations in the CPS Hierarchy., Logical Methods in Computer Science, Vol.1, No.2 (2005).
2) Danvy, O.: Functional Unparsing, Journal of
Functional Programming, Vol.8, No.6, pp.621–
625 (1998).
3) Danvy, O. and Filinski, A.: A Functional Abstraction of Typed Contexts, Technical Report 89/12, DIKU, University of Copenhagen(1989).
4) Danvy, O. and Filinski, A.: Abstracting Control, Proceedings of the 1990 ACM Conferenceon LISP and Functional Programming, Nice,New York, NY, ACM, pp.151–160 (1990).
5) Felleisen, M.: The Theory and Practice ofFirst-Class Prompts, Proc. 15th Symposium on
Principles of Programming Languages, pp.180–
190 (1988).
6) Filinski, A.: Representing Layered Monads,
Proc. 26th Symposium on Principles of Programming Languages, pp.175–188 (1999).
7) Kameyama, Y.: Axioms for Delimited Continuations in the CPS Hierarchy, CSL’04, Lecture Notes in Compuer Science 3210, Karpacz,
Poland, pp.442–457 (2004).
8) Kameyama, Y. and Hasegawa, M.: A Soundand Complete Axiomatization of Delimited
Continuations., Proc. International Conference on Functional Programming, pp.177–188

付

録

A.1 準

備

まず，定理の証明で必要となる定義と補題を述べる．
単純型付きラムダの型 t に対して, t のアリティ

arity(t) を以下のように定義する．
arity(b) = 0(b が基本型の時)

arity(t1 → t2 ) = 1 + arity(t2 )(それ以外の時)

t のアリティは，型 t をもつ項が受け取る引数の個数を表す．
補題 1 型 ス キ ー ム T と i > 0 に 対 し て ，arity([[T ]]i ) ≥ i である．
証明. T に関する帰納法で証明できる．
補題 2 値 V に対して，Γ ` V : (φ, S, S) が導ければ，任意の型スキーム T に対して Γ ` V : (φ, T, T )を導くことができる．
証明. 値は変数かラムダ式であり，任意の T に対して上記の形の型付けができることがわかる．
補題 3 Γ[x 7→ φ] ` M : T と Γ ` V : (φ, S, S) が導ければ，Γ ` M {x := V } : T が導ける．
証明. M に関する帰納法で証明できる．
補題 4 レベル n の評価文脈 E n と，型環境 Γ, 項

M , 型 τ , 型スキーム T, S に対して，Γ ` E n [M ] :(τ, T, S) が導出できれば，型 φ と型スキーム U, W が存在して，Γ ` M : (φ, U, W [rn−1 ← S[rn−1 ]]) が導出できる．
証明. レベル n の評価文脈 E n に関する帰納法で証明できる．

A.2 定理??の証明Γ ` M : T の導出の大きさに関する帰納法で証明すVol. 48

No. SIG 0(PRO 34)

階層化コントロールオペレータに対する型システムの構築

る．スペースの都合上，M = x, shift, reset のケース

11Σ, Π `λ→ θ0 vκ1 . . . κn+1 κ0n+2 . . . κ0m+1 : t0
Σ `λ→ N : [[τ ]] → [[T [rn ]]]m−nのみを掲載する.

(i) M = x の時が言える．さらに，

仮定より，Γ ` x : (τ, T, T ) が言える．このとき∆ = [kn+2 7→ s1 , kn+3 7→ s2 , . . . km+1 7→ sm−n ]Γ(x) = τ となる．よって，(x 7→ [[τ ]]) ∈ [[Γ]] である．

とおき，`λ→ θi : wi (1 ≤ i ≤ n) に注意すると，

任意の型スキーム T に対して，次の型判断を導出
したい．

[[Γ]], Σ, ∆ `λ→ Cm+1 [[M 0 ]]θ1 . . . θn N κn+2 . . . κm+1 : s0となる．以上から，[[Γ]] `λ→ Cm+1 [[x]] : ([[τ ]] → [[T ]]m ) → [[T ]]m
CPS 変換の定義から，Cm+1 [[x]] は以下のようになる．
Cm+1 [[x]] = λκ1 . . . κm+1 .κ1 xκ2 . . . κm+1
補題??より，arity([[T ]]m ) ≥ m なので，適当な型

a1 , . . . , am , b に対して，[[T ]]m = a1 → . . . → am → bとおける．そこで，[[Γ]] `λ→ Cm+1 [[hM 0 in ]] : [[(τ, T, T [rn ← S])]]m+1が導けて，このケースの証明を終了する．

(v)M = Sn k.M 0 の場合
仮定から

Γ ` Sn k.M 0 : (τ, U [rn−1 ← (α, T, S)], U )かつ，

Σ = [κ1 7→ [[τ ]] → [[T ]]m , κ2 7→ a1 , . . . κn+1 7→ an ]~
Γ0 ` M 0 : init(n, U [rn−1 ], ~γ , Z)とおくと，

Γ0 = Γ[k 7→ τ → (α, W [rn ← T ], W [rn ← S])][[Γ]], Σ `λ→ κ1 xκ2 . . . κm+1 : bとなり，が言える．これに帰納法の仮定を適用すると，以下が得られる．

[[Γ]] `λ→ Cm+1 [[x]] : ([[τ ]] → [[T ]]m ) → [[T ]]myi = [[γi ]] → [[(γi , Zi , Zi )]]m+1−i とすると，~ m+1[[init(n, U [rn−1 ], ~γ , Z)]]

が言える．
0

(ii) M = λx.M の時，省略．

= y1 → y2 → . . . → yn → [[U [rn−1 ]]]m−n+1(iii) M = M1 M2 の時，省略．
(iv) M = hM 0 in の時0仮定から，Γ ` hM in : (τ, T, T [r~ m+1[[Γ0 ]] ` Cm+1 [[M 0 ]] : [[init(n, U [rn−1 ], ~γ , Z)]]となる．補題 ??より，[[U ]]m ,[[W ]]m はそれぞれ m 個n← S]) および

~ ) が導出できる．
Γ ` M 0 : init(n, (τ, T [rn ], S), ~γ , W
帰納法の仮定により，~ )]]m+1[[Γ]] `λ→ Cm+1 [[M 0 ]] : [[init(n, (τ, T [rn ], S), ~γ , Wが得られる．ここで，1 ≤ i ≤ n に対して，

wi = [[γi ]] → [[(γi , Wi , Wi )]]m−i+1とすると，

以上，[[T ]]m−n ,[[S]]m−n はそれぞれ m − n 個以上の引数を取るので以下のように表現できる．

[[U ]]m = u1 → u2 → . . . → um → u0[[W ]]m = w1 → w2 → . . . → wm → w0[[T ]]m−n = t1 → t2 → . . . → tm−n → t0[[S]]m−n = s1 → s2 → . . . → sm−n → s0
この時，~ )]]m+1[[init(n, (τ, T [rn ], S), ~γ , W[[U [rn−1 ]]]m+1−n=w1 → . . . → wn → ([[τ ]] → [[T [rn ]]]m−n ) → [[S]]m−n= un → un+1 → . . . → um → u0と表せる．補題 ??より，[[T ]]m と [[S]]m−n はそれぞ[[U [rn−1 ← (α, T, S)]]]m

れ m 個以上と m − n 個以上の引数をもつので，= u1 → u2 → . . . → un−1[[T ]]m = t1 → t2 → . . . → tm → t0[[S]]m−n = s1 → s2 → . . . → sm−n → s0と置けて，以下のようになる．

[[T [rn ]]]m−n = tn+1 → tn+2 → . . . → tm → t0[[T [rn ← S]]]m = t1 → . . . → tn
→ s1 → . . . → sm−n → s0

→ ([[α]] → [[T ]]m−n ) → [[S]]m−n[[W [rn ← T ]]]m
= w1 → w2 → . . . → wn → [[T ]]m−n[[W [rn ← S]]]m= w1 → w2 → . . . → wn → [[S]]m−nとなる．ここで，Σ = [v 7→ [[τ ]],ここで，Σ = [k1 7→ [[τ ]] → [[T ]]m ,k2 7→ t1 , k3 7→ t2 , . . . kn+1 7→ tn ]
Π = [v 7→ [[τ ]],
0
0
0
kn+2
7→ tn+1 , kn+3
7→ tn+2 , . . . km+1
7→ tm ]
N = λvκ0n+2 . . . κ0m+1 .θ0 vκ1 . . . κn+1 κ0n+2 . . . κ0m+1とすると，

κ01 7→ [[α]] → [[W [rn ← T ]]]m ,κ02 7→ w1 , . . . , κ0n+1 7→ wn ,
κ0n+2 7→ s1 , . . . , κ0m+1 7→ sm−n ]Π = [w 7→ [[α]],κ00n+2 7→ t1 , . . . , κ00m+1 7→ tm−n ]情報処理学会論文誌：プログラミング

12

2007

(ii) hV in → Vとすると，Σ, Π `λ→ θ0 wκ01 . . . κ0n+1 κ00n+2 . . . κ00m+1 : t0が言える．ここで，仮定より，Γ ` hV in : (α, T, T [r n ← U ]) である．

reset の規則より，以下が得られる．

N = λwκ00n+2 . . . κ00m+1 .θ0 wκ01 . . . κ0n+1 κ00n+2 . . . κ00m+1とすると，以下の型判断が導出できる．

Σ `λ→ N : [[α]] → [[T ]]m−nさらに，∆ = [κ1 7→ [[τ ]] → [[U [rn−1 ← (α, T, S)]]]m ,κ2 7→ u1 , . . . , κn 7→ un−1 ]~)Γ ` V : init(n, (α, T [rn ], U ), ~γ , WnΓ ` hV in : (α, T, T [r ← U ])~ ) の部分は，値に
ここで，init(n, (α, T [rn ], U ), ~γ , W
対する型スキーム なので，その左部分木と右部分木の型スキームは等しくなる．よって，以下の関係が得
られる．

とすると，

[[Γ]], ∆, Σ `λ→ θ0 vκ1 . . . κn N κ0n+2 . . . κ0m+1 : s0が得られる．ここで，

p = λvκ01 . . . κ0m+1 .θ0 vκ1 . . . κn N κ0n+2 . . . κ0m+1~ 2)(γ1 , W1 , W1 ) = init(n − 1, (α, T [rn ], U ), γ~2 , W~~
ただし，γ~i , Wi はそれぞれ ~γ , W の i 番目以降の変数列とする．ここで，~ 2)
init(n − 1, (α, T [rn ], U ), γ~2 , Wとすると，以下の型判断が得られる．

=(γ2 , (γ2 , W2 , W2 ),[[Γ]], ∆ `λ→ p :[[τ ]] → ([[α]] → [[W [rn ← T ]]]m )→ [[W [r ← S]]]m~ 3 ))
init(n − 2, (α, T [rn ], U ), γ~3 , Wnであるから，これらの関係式から以下の等式が得らとなる．一方，~ m+1[[Γ0 ]], ∆ `λ→ Cm+1 [[M 0 ]] : [[init(n, U [rn−1 ], ~γ , Z)]]れる．

γ1 = γ20が成立するので，L = (Cm+1 [[M ]]){k := p} と置くと，上記の型判断から以下が得られる．

[[Γ]], ∆ `λ→ L : [[init(n, U [rn−1W1 = (γ2 , W2 , W2 )~ 3)= init(n − 2, (α, T [rn ], U ), γ~3 , W~ m+1], ~γ , Z)]]

この W1 に対しての等式より，最初と同じような関係

さらに，`λ→ θi : yi であり，

Ψ = [κn+1 7→ un , . . . , κm+1 7→ um ]とすると，[[Γ]], ∆, Ψ `λ→ Lθ1 . . . θn κn+1 . . . κm+1 : u0が成立するので，が出てくる．このような計算を同様に繰り返していくと，結局，以下の等式が得られる．

γi = γi+1
Wi = (γi+1 , Wi+1 , Wi+1 )[[Γ]] `λ→ Cm+1 [[Sn k.M ]]: [[(τ, U [rn−1 ← (α, T, S)], U )]]m+1となるため，このケースでも定理は成立する．

(証明終わり)Wn = T [rn ] = U
この関係より，それぞれの型判断は以下のように書き換えられる．

Γ ` hV in : (α, T, T )A.3 定理??の証明
それぞれの評価規則ごとに証明する．なお，E[R] →E[M ] の形の評価規則では，外側の評価文脈 E を除去して (E = [ ] と仮定して) R → M に対する型の保存を証明すればよいことがすぐにわかるので，以下ではその形で証明する．

(i) (λx.M )V → M {x := V }Γ ` (λx.M )V : T より，以下の導出を得る．ただし，
T = (α, S, U )，X ∗ = (X, U, U ) とする．
Γ[x 7→ β] ` M : (α, S, U )Γ ` λx.M : (β → (α, S, U ))∗ Γ ` V : β ∗Γ ` (λx.M )V : (α, S, U )補題??と Γ[x 7→ β] ` M : (α, S, U ), Γ ` V :(β, U, U ) より，以下が導ける．
Γ ` M {x := V } : (α, S, U )よって，定理は成立する．

(1 ≤ i ≤ n − 1)γn = α0Γ ` V : (α, W1 , W1 )補題??より，Γ ` V : (α, W1 , W1 ) から Γ ` V :(α, T, T ) が言える．よって，定理は成立する．
(iii) hE n [Sn k.M ]ij → hM {k := λx.hE n [x]in }ij(n ≤ j)
まず，仮定と型付け規則から，以下の導出を得る．
~
Γ ` E n [Sn k.M ] : init(j, (τ, T [rj ], X), ~γ , S)Γ ` hE n [Sn k.M ]ij : (τ, T, T [rj ← X])
以下では, 煩雑さを避けるため, init の第 3, 第 4 引数
~ の記述を省略する．補題??から，(~γ , S)Γ ` Sn k.M: (φ, U, V [rn−1 ← init(j − n, (τ, T [rj ], X))])を得る．この判断を結論とする導出を考えると，最後に適用する規則は shift であるので，

U = V [rn−1 ← (ψ, W, Y )](1)

Vol. 48

No. SIG 0(PRO 34)

階層化コントロールオペレータに対する型システムの構築

13

能なので，適当な型スキーム T1 , T2 に対して，[ ] `となり，以下の判断を得る．

Γ0 ` M : init(n, init(j − n, (τ, T [rj ], X)))

N1 : T1 と [ ] ` N2 : T2 が導ける．そこで帰納法の仮Γ = Γ[k 7→ φ → (ψ, Z[r ← W ], Z[r ← Y ])]定を使うと，N1 , N2 は，上記の 1, 2, 3, 4, 5 のいず

0

n

n

k に λx.hE n [x]in を代入しなくてはいけないので，それぞれが同じ型を持たなくてはいけないが，それは，れかの形である．

N1 が 2, 3, 4, 5 のいずれかの形のときは，評価文

以下の導出で確認できる．ただし，A = (ψ, Z[r ←脈 E を EN2 に置き換えれば M 全体が 2, 3, 4, 5 のW ], Z[rn ← Y ]) とする．

形であることが言える．N1 が 1 の形で，N2 が 2, 3,

n4, 5 のいずれかの形のときは，E を N1 E に置き換え
Γ[x 7→ φ] ` x : (φ, U, V [rn−1 ← (ψ, W, Y )])Γ[x 7→ φ] ` E n [x] : init(n, (ψ, W, Y ))
Γ[x 7→ φ] ` hE n [x]in : AΓ ` λx.hE n [x]in : (φ → A, Z0 , Z0 )(??) より，U = V [rn−1 ← (ψ, W, Y )] なので，この型判断は正しい．補題??と，ればよい. N1 も N2 も 1 の形のときは，M に自由変数がないので N1 は変数ではあり得ず，ラムダ抽象である．従って，N1 N2 は 2 の形になっている．(証明おわり)
定理??の証明:[ ] ` hM im : T が導けると仮定する．hM im は，上Γ0 ` M : init(n, init(j − n, (τ, T [rj ], X)))記の補題で述べた 1, 2, 3, 4, 5 のいずれかの形である

Γ ` λx.hE n [x]inが，1 と 4 はあり得ない．従って，2, 3, 5 のいずれか: (φ → (ψ, Z[rn ← W ], Z[rn ← Y ]), Z0 , Z0 )より，以下の判断が得られる．

Γ ` M {k := λx.hE n [x]in }: init(n, init(j − n, (τ, T [rj ], X)))
これに reset 規則を適用すると，の形であり，これらはいずれも評価規則の左辺になっているので，1 ステップの計算が可能である．(証明おわり)(平成 18 年 12 月 16 日受付)
(平成 19 年 4 月 1 日採録)

Γ ` hM {k := λx.hE n [x]in }ij : (τ, T, T [rj ← X])となり，定理は成立する．(証明終わり)

A.4 定理??の証明

鈴木 輝信
筑波大学大学院システム情報工学

この定理をやや一般化した以下の補題を証明する．

研究科コンピュータサイエンス専攻

補題 5 項 M , 型スキーム T に対して [ ] ` M : T

博士前期課程在学．プログラム言語が導けるならば，以下のいずれかが成立する．

1. M は値.

の型システムに関する研究を行う．
日本ソフトウェア科学会会員．

2. M は E[(λx.M 0 )V ] の形．
3. M は E[hE n [Sn k.M 0 ]ij ] の形 (ただし，j ≥ n)．

亀山 幸義（正会員）
筑波大学大学院システム情報工学

4. M は E n [Sn k.M 0 ] の形．

研究科コンピュータサイエンス専攻

5. M は E[hV in ] の形．

助教授．プログラムの論理とソフト

証明. M に関する帰納法で証明する．

ウェア検証に興味をもつ．ACM，日M = N1 N2 の場合だけを述べる．M が型付け可

本ソフトウェア科学会 各会員．