階層化コントロールオペレータに対する型システムの構築
13
0
0
全文
(2) Vol. 48. No. SIG 10(PRO 33). 階層化コントロールオペレータに対する型システムの構築. 139. れぞれの shift/reset の計算が干渉しあって，プログラ. ラム中で利用することができる．call/cc と shift/reset. マの意図どおりに実行されないことがある．これを解. の違いは，call/cc が獲得する継続はプログラムが終. 決するために階層化 shift/reset 4) が提案された．階層. 了するまでの計算すべてであるが，shift/reset が獲得. 化 shift/reset は，階層化されない shift/reset と同様. する継続は，プログラムが終了するまでの計算の一部. に，その意味が CPS 変換により厳密に与えられてい. 分にできることである．後者の継続を限定継続（de-. るという利点があるが，その複雑さのため，型システ. limited continuation）と呼び，より精密にプログラ. ムやその性質に関しては十分には検討されてこなかっ. ムを制御することができる．. た．階層化 shift/reset に対する型システムは，型のあ グラムを抽象化することによりプログラムの理解を助. shift オペレータは，k を変数，M を式とするとき， Sk.M という形で表現される．この式はその（限定） 継続を k に束縛して，M を計算するという式であ. けるという効果もある．我々は階層化 shift/reset に. る．一方，継続を束縛する際にその範囲を限定するの. 対する型システムについて研究しており，先行研究12). が reset であり M と表す．shift で継続を捕捉する. においてレベル 2 の階層化 shift/reset に対して型シ. 際には，reset までの範囲の継続が対象となる．. る言語への導入のためだけではなく，型によってプロ. ステムを提案した．しかし，この型システムでは，1. これらの式の意味を以下の例で考える．. 2 + Sk.(3 + 4) + 1. つの型判断が，レベルの指数関数の個数の型を必要と し，この多数の型を適切に記述する記法がなかったた め，レベル 3 以上の階層化 shift/reset に対応するの. = (3 + 4) + 1 = 8 2 + Sk.(3 + (k(k4))) + 1. ことにより上記の問題点を克服し，任意のレベルの. = (3 + (2 + (2 + 4))) + 1 = 12 最初の式は，shift でとらえた継続を利用しない場合 である．Sk.(3 + 4) を実行する際の残りの計算は，. shift/reset に対する型システムを提案する．さらに， この型システムが型の健全性や CPS 変換による型の保. 2 + [ ] + 1 であるが，shift がとらえる継続は最も近 い reset までであるため，2 + [ ]（2 を加える）とい. 存など，型システムとして必要とされる良い性質を満. う継続（を関数で表現したオブジェクト）が k に束. たすことを証明する．これにより，階層化 shift/reset. 縛される．次に，shift の内側の計算 (3 + 4) を行い，. は難しかった． 本研究では，型スキームと呼ばれる記法を導入する. を静的な型システムを持つ言語に導入できるようにな. この部分の計算が終わると reset の継続 ([ ] + 1) に飛. ると考えている．. ぶ．結果として，2 を加える部分は実行されず，8 と. 本論文の構成は以下のとおりである．2 章では，. shift/reset の概要と階層化について述べる．3 章で は，対象とする λ 計算に階層化 shift/reset を追加し. いう計算結果を得る．. 2 つ目の式は，shift の内側の計算で k を利用した場 「2 を加える」という関数が束縛さ 合である．k には，. た言語 λSm と CPS 変換の定義を与えた後，本論文が. れており，この計算を 2 回行った後に 3 を足す．この. 提案すると型システムの形式的な定義を述べる．4 章. 時点で shift の内側の式の計算が終わったので，reset. では，本論文の型システムが満たす性質を示し，5 章. の外側に飛んで残りの計算を行い，計算結果は 12 に. で，まとめと今後の課題を述べる．. なる．. 2. shift/reset と階層化 この章では，shift/reset の概要，簡単なプログラム 例，階層化の必要性について述べる．. 2.1 コントロールオペレータ shift/reset 前章で，shift/reset は継続を扱うためのコントロー ルオペレータであると述べた．継続は，対象となる式 の計算後からプログラム終了までの計算を表す概念で あり，shift/reset はこの継続をプログラムの中から利 用する機構を与える．. 2.2 shift/reset の階層化 階層化 shift/reset は，前節の shift/reset に自然数 のレベルを割り当て，使用目的の異なる shift と reset を区別できるようにしたコントロールオペレータであ る4) ．階層化した shift は Sn k.M ，reset は M n と いう形になり，それぞれの n がその shift，reset のレ ベルになる． 階層化 shift/reset の例を以下に示す．. 1 + (S2 k. k(k1)) + 31 + 22 もし，この式の shift/reset のレベルがないとする. これと同様のコントロールオペレータとして，. と，k に束縛される継続は 3 を足す部分だけなので，. Scheme などのプログラム言語における call/cc がある． call/cc は，継続を変数に束縛するため，継続をプログ. 1 +(((1 +3) +3) +2) = 10 になるが，この場合，shift のレベルが 2 なので，レベルが 1 の reset を無視して，.
(3) 140. 外側のレベルが 2 の reset までの継続をとらえること になり，計算結果は 1 + ((1 + 3 + 2) + 3 + 2) = 12 になる．この例ではレベル 2 までしかないが，一般 に n > 0 なる任意の自然数に対して，レベル n の. shift/reset が定義される． 2.3 階層化 shift/reset の例 階層化 shift/reset の利用法を説明するため，文献. 4) の例を取り上げる．まず，非決定的な計算を行うプ ログラムを shift/reset で表現したものを以下に示す． filp(x) = S1 k.(k(true); k(false); fail( )) fail(x) = S1 k.“no” choice(n) = if n < 1 then fail( ). ここで. June 2007. 情報処理学会論文誌：プログラミング. else if filp( ) then choice(n − 1) else n は任意の値であり，a; b は式 a と式 b を順. 番に実行して b の値を結果とする式である．. と本論文で提案する型システムについて述べる．. 3.1 構文と評価 m を正の自然数とする．本論文が対象とする言語 λSm は，λ 計算に m 以下のレベルの shift と reset を追加した言語である．λSm の項 M と値 V は以下 のように定義される．. M ::= x | λx.M | M1 M2. (変数) (λ-抽象) (適用). | Sn k.M | M n. (shift, 1 ≤ n ≤ m) (reset, 1 ≤ n ≤ m). V ::= x | λx.M Sn k.M はレベル n の shift を用いた項であり，この 項の中で，変数 k が束縛される．shift が獲得する継. このような関数を定義し，print(choice(3))1 とい. 続の範囲を限定するのが reset であり，M n と表現. うプログラムを実行すると，1，2，3 がこの順で印刷. される．変数は λ あるいは Sn により束縛され，α 同. される．すなわち，関数 flip は非決定的選択を実現す. 値性や代入 M {x := M } は，通常のラムダ計算と同. る関数である．. 様に定義する．また，α 同値な項は同一視する．. 次に，生成された数を収集するための関数を以下の. 次に，λSm に対する文脈を 3 種類導入する．. ように定義する．. C ::= [ ] | λx.C | M C | CM | Cn | Sn k.C. emit(n) = S1 k.cons(n, k(nil)) たとえば，emit(1); emit(2); emit(3)1 という計算を 行うと自然数のリスト [1; 2; 3] を返す．. (文脈) E ::= [ ] | V E | EM | En (評価文脈). そこで，emit(choice(3))1 とすると，自然数のリ スト [1; 2; 3] を返すことを期待する．しかし，実際に. E n ::= [ ] | V E n | E n M | E n i (i < n) (レベル n の評価文脈). 計算してみると，[1]，[2]，[3] という別々のリストは. C は一般の文脈であり，[ ] は穴（hole）を表す．E は. 生成されるが，これらが収集されて 1 つのリストにな. 値呼び計算戦略における評価文脈である．ただし，穴. ることはない．. を取り囲む reset があってもよいように拡張している．. このように，shift/reset を用いた関数を複数組み合 わせることにより，これらが干渉して意図どおりにプ. E n は，穴を囲む reset のレベルを n より小さいレベ ルに制限した評価文脈であり，次に述べる shift の評. ログラムが動かなくなってしまうことがある．そこで，. 価規則において利用する．文脈 C に対し，C[M ] は. 階層化 shift/reset を用いて，emit の定義を以下のよ. 文脈 C の穴を項 M で埋めた項を表す．. うに変更する．. emit(n) = S2 k.cons(n, k(nil)) emit(choice(3))2 を実行すると，期待どおり [1; 2; 3]. λSm の評価規則を次に示す．ただし，n ≤ j とする． E[(λx.M )V ] → E[M {x := V }] E[E n [Sn k.M ]j ] → E[M {k := λx.E n [x]n }j ] E[V n ] → E[V ]. というリストが返る． 階層化していない shift/reset を複数用いる場合，. shift/reset どうしの干渉は容易に起きる問題であり， その解決のために階層化することは，現実のプログラ ミングを行う際には非常に重要であると考える．. 3. 階層化 shift/reset の形式化と型システム. 最初の規則は，値呼び λ 計算の通常の β 簡約で ある．. 2 番目の規則は shift の計算を表すもので，shift から 見て一番内側の reset（ただし，reset のレベルは n 以 上）までの継続 E n を捕捉し，それを関数 λx.E n [x]n に変形して変数 k に束縛する．レベル n の shift が. この章では λ 計算に階層化 shift/reset を追加した. 獲得する継続は，レベル n 以上の reset によって限定. 言語 λSm を形式的に定義し，さらにその CPS 変換. されるので，n ≤ j という条件がついている．たとえ.
(4) Vol. 48. No. SIG 10(PRO 33). 階層化コントロールオペレータに対する型システムの構築. Cm+1 : Term → Cont 1 → . . . → Cont m+1 → Answer κi ∈ Cont i = Val → Cont i+1 → . . . → Cont m+1 → Answer. 141. (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κ1 . . . κm+1 .(Cm+1 [[M ]]{x := v})κ1 . . . κm+1 )κ2 . . . κm+1. Cm+1 [[M1 M2 ]] = λκ1 . . . κm+1 .Cm+1 [[M1 ]](λf κ2 . . . κm+1 . Cm+1 [[M2 ]](λaκ2 . . . κm+1 .. f aκ1 κ2 . . . κm+1 )κ2 . . . κm+1 )κ2 . . . κm+1 Cm+1 [[M n ]] = λκ1 . . . κm+1 .Cm+1 [[M ]]θ1 . . . θn (λvκn+2 . . . κm+1 .θ0 vκ1 . . . κn+1 κn+2 . . . κm+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κ1 . . . κm+1 .θ0 vκ1 . . . κn (λwκn+2 . . . κm+1 .θ0 wκ1 . . . κn+1 κn+2 . . . κm+1 )κn+2 . . . κm+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 .. ば，E 2 [E 1 [S2 k.M ]1 ]2 という式における S2 が獲. グラムに対して，m + 1 回☆ CPS 変換を繰返すことに. 得する継続は，外側のレベル 2 の reset までである．. より，純粋なラムダ項になる．この繰返し全体を 1 つ. n. k に束縛される関数として λx.E [x]n のかわりに. の変換としたものが CPS 変換 Cm+1 であり，その定. λx.E n [x] を採用すると，shift/reset とは意味が異な る control/prompt と呼ばれるコントロールオペレー タになる5) ．control/prompt は，部分継続を表現す. の継続変数 κ1 , · · · , κm+1 を受け取って変換後の項を. る最初のコントロールオペレータであるが，その意味. 生成している．κ2 をメタ継続と呼び，κ3 をメタメタ. 義を図 1 で与える． 図 1 で分かるように，この CPS 変換は，m + 1 個. 論が shift/reset より複雑であったことを一因として，. 継続などと呼ぶ．この CPS 変換は，型のない λSm の. 今日では shift/reset が主に使われている．. 項全体に対して定義され，CPS 変換後の項は再帰型を. 評価規則の最後のものは，reset の内側の項が値に なった場合に，その reset を除去する規則である．. 3.2 CPS 変換 CPS 変換は，プログラムを CPS（Continuation. 利用して型を付けられる．図 1 の上部にその型を記述 した．Cm+1 は，変換前の項（型は Term ）と m + 1 個の継続（型は Cont i ）を受け取り，Answer 型の値 を返す関数である．変換前の項に型がないことに対応. Passing Style）とよばれる特別な形式に変換するプ ログラム変換である．CPS 形式のプログラムは，計. して，値の型 Val の定義式で再帰型が現れている☆☆ ．. 算の途中結果すべてに名前が付けられ，すべての関数. は，メタ継続など 2 個目以降の継続を η 変換により. shift と reset 以外の項に対する CPS 変換において. 呼び出しが末尾呼び出しであるという特徴があり，理. 消去することができ，通常の CPS 変換を 1 回行って. 論的な解析やコンパイラの中間言語などで幅広く利用. 得られる項と同じである．shift は 1 個目から n 個目. されている．. までの継続をまとめて k に割り当て，M の 1 個目か. λSm のプログラムに対する CPS 変換は，通常の. ら n 個目までの継続は初期化される．また，reset で. CPS 変換を m + 1 回繰返すことで与えられる4) ．レ ベル n の shift/reset に対して CPS 変換を行うと， レベルが n − 1 である shift/reset に変換され，特に. は 1 個目から n 個目の継続を n + 1 個目の継続にま. n = 1 のときは，CPS 変換により shift/reset が消去 され，純粋なラムダ項になる．そこで，λSm のプロ. ☆. ☆☆. m 回の CPS 変換で，階層化 shift/reset をすべて消すことが できるが，CPS 形式にならないため，さらにもう 1 回余分に 変換を行っている． Val の定義の右辺に Val が negative な位置に出現している． 変換前の項に本論文で述べる型が付いている場合は，変換後に 再帰型は必要なく，単純型付きラムダ計算の範囲内で型が付け られる．.
(5) 142. June 2007. 情報処理学会論文誌：プログラミング. とめる．これにより，レベルが n 以下の shift では継 続が束縛されない．. 3.3 先行研究の型システム 本研究の型システムについて述べる前に，先行研究 の shift/reset に対する型システムについて述べる． Danvy らは文献 3) において，階層化していない shift/reset に対する型システムを与えた．彼らの型シ ステムでは，項の型を考える際に継続の型を考慮する. 表 1 先行研究との比較 Table 1 Comparison of our work and previous work.. Answer Type の変化 非対 応 階 層 化. 対応. 非 対 応. Filinski の実装 (1994). Danvy,Filinski (1989). 対 応. Murthy (1992). 本研究の型システム. ものであり，型判断は以下の形をしている．. Γ, α M : τ, β Γ は型環境，M は項，τ ，α，β は型である．これは， M の継続の型が τ → α であるときに，計算結果の型 は β であることを表す．shift/reset がなければ α = β であるが，shift/reset を導入すると，α = β のこと がある．この型システムの shift と reset の型付け規 則は以下のとおりである．. で，Murthy の制約のもとでは型付けができないもの が存在するため，より多くの項を型付けできる型シス テムが必要である． これらの先行研究と今回提案する型システムの関係 を表 1 にまとめる． これまで我々は，Danvy-Filinski の型システムを拡 張し，レベル 2 の階層化 shift/reset に対応した型シ. Γ[k → (τ /δ → α/δ)], σ M : σ, β shift Γ, α Sk.M : τ, β. ステムを構築した12) ．型判断は，レベル 2 に対応し. Γ, σ M : σ, τ reset Γ, α M : τ, α. め，以下の形になっている．. て 2 種類の継続の型と結果の型を含む必要があったた. Γ; α1 , α2 , α3 M : τ, β1 , β2 , β3. shift の規則では，k の型は関数型であり，その引数 の型が τ ，関数本体の継続の型が α → δ ，計算結果. 項 M の 1 個目の継続の型が τ → (α1 → α2 ) → α3. の型は δ である．この規則を見ると，shift の継続の. となる．例として，この型システムにおけるレベル 2. 型 τ → α を k の型として割り当て，M の継続の型. の shift に対する型付け規則をあげる．. が σ → σ となっており，M の継続が初期化されてい. Γ ; γ1 , γ2 , γ2 M : γ1 , γ3 , γ3 , β shift2 Γ; α S2 k.M : τ, α1 , α2 , β ただし，Γ = Γ[k → (τ /δ → α3 /δ)] とする．. ることが分かる．reset の規則では，reset の型 τ を. M の結果の型として，shift でとらえる範囲外にして，. であり，2 個目の継続の型が β1 → β2 ，結果の型は β3. M の継続の型は σ → σ として初期化している，と. このようにして，レベル 2 の shift/reset に対応し. 見ることができる．このように見ると，shift/reset の. た型システムを構築したが，これをレベル n まで単. 計算が型のうえで表現されていることが分かる．. 純に拡張すると型判断に含まれる型の個数が非常に多. Murthy 10) は，階層化 shift/reset に対する型シス テムを与えた．彼の型システムでの型判断は. くなり，型付け規則を表現することだけでも簡単なこ. Γ M : Kα [T ]. とではなくなってしまう．レベル 1 で 3 個，レベル 2 で 7 個の型が必要であり，一般にレベル n の型シス. という形である．ただし，α は型の列 αm . . . α1 の略. テムでは，必要な型の個数が O(2n ) となる．型の爆. 記であり，Kα [T ] は以下のように定義される．. 発をおさえるには，これらの多くの型を適切に表現す. K[] [T ] = T Kατ [T ] = (T → Kα [τ ]) → Kα [τ ] 例として m = 1 の場合は，. Γ M : (T → α1 ) → α1. る記法が不可欠である．. 3.4 λSm に対する型システム 本研究では，型システム構築にあたって，以下の原 則を設定した．. Filinski の型システムに比べ，継続の返す型と計算結 果の型が同じという制約が加わっている．これらの型. • 型 シ ス テ ム の 健 全 性（Subject Reduction と Progress）が成立すること． • 意味を持つ項は，できる限り多く型付けできるこ. が異なるような項（いわゆる Answer Type が変化す. と．少なくとも応用上，有用な項は型付けできる. となる．この例から分かるように，上記の Danvy-. る項）に対して，Murthy の型システムでは型を付け. こと．. ることができない．ML における printf の型付け2) を. 第 1 の要求は，静的な型システムを持つプログラム. shift/reset で表現した場合など，興味深いプログラム. 言語のコアとなる体系を目指している以上，当然のこ.
(6) Vol. 48. No. SIG 10(PRO 33). 階層化コントロールオペレータに対する型システムの構築. 143. 型スキーム T に対して T [l] は左部分木，T [r] は右. とであろう． 第 2 の要求も当然のことであるが， 「意味を持つ項」 が何かについては検討を要する．階層化 shift/reset の 意味は，CPS 変換により与えられており，CPS 変換 をほどこした後の項は，通常の（shift/reset のない）. 部分木を表す．また，T [rl ] を以下のように定義する （T [ll ] も同様に定義する）．. T [r0 ] = T T [rl ] = (T [rl−1 ])[r]. (l > 0). ラムダ項になる．そこで，我々は， 「項 M を CPS 変. 型スキーム T と s = l，r，ln ，rn に対して，その. 換したときに，単純型付きラムダ計算の項になる（単. 部分木 T [s] を型スキーム S で置き換えた型スキーム. 純型付きラムダ計算で型が付く）こと」を「項 M が. を T [s ← S] と表記する．よく現れる型スキームの略 を以下のように定義する．た 記として init(n,T , γ ,S). 意味を持つ」ことと定めた． る考え方と同じであるが，上述したように，shift/reset. だし，0 ≤ n ≤ m，T は型スキーム， γ は n 個の型 は n 個の 型スキーム S1 , · · · , Sn γ1 , · · · , γn の列，S. の型システムに関する既存の研究の多くは，この要求. の列である．. この考え方は，Danvy-Filinski の型システムにおけ. を満たしていない．本論文で提案する型システムは， 既存の研究で型付けできる範囲をすべて含んだうえで， これまで考えられてきたプログラム例を（我々が試み. =T init(0, T, γ , S) = init(n + 1, T, γ , S) )) (γ1 , (γ1 , S1 , S1 ), init(n, T, γ , S. た範囲では）すべて型付けできるという意味で既存の 研究より強力である．. は，それぞれ γ と S の先頭要素を ただし， γ と S. 3.4.1 型と型スキーム 本論文では，レベル m の shift/reset に対する型シ ステムを表現するため，型スキームを導入した．これ. 取り除いた列である．後に述べる型付け規則において ムを表すフレッシュなメタ変数の列をとる．これは，. は，複数ある継続の型を木構造で表現するとともに，. レベル n の shift や reset の型付けにおいて，レベル. init を使うときは，第 3，第 4 引数は，型や型スキー. 必要以上に型情報を型判断に加える必要がない工夫を. n 未満の部分は，(γ, (γ, S, S), ) の形であることを意. 加えたものである．また，shift/reset の型付け規則が. 味する．. λSm の m によらず同じ形である，という特徴を持っ. 型スキームの例を図 2 に示す．ここで，a，b，c，d， γi は型，A，B ，C ，D，X ，Si は 型スキーム，T [r]. ている． 型 τ と型スキーム T を以下のように定義する．. τ ::= b |τ →T T ::= ∗ | (τ, T1 , T2 ). (基本型) (関数型) (基本型スキーム) (3 つ組). 型スキームにおける 3 つ組 (τ, T1 , T2 ) は，2 分木を 表現しており，木の根は型 τ であり，左部分木は T1 ，. は T の右の部分木を，T [r2 ] はそのさらに右部分木を とる操作である．また，T [r ← X] は T の右部分木 を X に置き換えた木を表し，同様に T [r2 ← X] は. T [r2 ] を X に置き換えた木を表す．init(2, X, , ) は 図 2 のような木を構成する．init の第 1 引数が大き くなると，木がより下へ伸びることになる．. 3.4.2 型付け規則 本研究で提案する λSm に対する型システムの型判. 右部分木は T2 である．これは，直感的には，CPS 変. 断と型文脈を，それぞれ以下のように定義する．ただ. 換により，(τ → T1 ) → T2 と変換される型を表現し. し，M は項，T は型スキーム，x は変数，t は型で. たものである（ただし，τ などは τ などを CPS 変. ある．. 換して得られる型である）．型スキーム ∗ は，“don’t. ΓM :T Γ ::= [ ] | Γ[x → τ ]. care” を意図した定数であり，Answer Type（図 1 の 型 Answer ）を含む任意の型に CPS 変換される型を表. 型判断 Γ M : T は，型環境 Γ 下で項 M の型ス. 現している．すなわち，n 未満のレベルの shift/reset. キームが T であることを表す．. しか持たないプログラムを型付けするとき（厳密には，. 型付け規則の定義を図 3 に与える．. さらに，そのプログラムに含まれる自由変数が表すエ. 図 3 において，shift と reset の規則で現れる init. フェクトもレベル n 未満であるとき），n + 1 以上の. は，n 番目までの継続が初期化されることに対応する. 深さの型の構造を記述する必要はないという事実に基. 型である．shift や reset に対する型スキームが右部分. づき，複雑な型を ∗ を使って簡潔に記述するために使. 木と左部分木で共通しているところは，1 番目の継続. われる．. に 2 番目以降の継続を適用できることに対応している．.
(7) 144. June 2007. 情報処理学会論文誌：プログラミング. 図 2 型スキームの例 Fig. 2 Examples of type scheme.. Γ(x) = τ var Γ x : (τ, T, T ). Γ[x → τ ] 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 ≤ m n Γ M n : (τ, T, T [r ← S]) . Γ M : init(n, U [rn−1 ], γ , S). Γ Sn k.M : (τ, U [rn−1 ← (α, T, S)], U ). shift n , n ≤ m. . Γ = Γ[k → τ → (α, W [rn ← T ], W [rn ← S])] 図 3 型付け規則 Fig. 3 Typing rules.. 3.4.3 型付けの例. ており，階層化 shift/reset に対応した型システムで. 前項で定義した型システムを用いて，実際のプログ. あることが分かる．. ラムの型付けを行った例を示す．ここで型付けを行っ. この例は階層化レベルが 2 であるが，Biernacka ら. たプログラム M は以下のものである．. による Normalization by Evaluation 1) は，階層化レ. M = emit2 (choice 3); “no”1 ; nil2 choice は 2.3 節で定義した関数であり，emit2 はレベ. ベルが 5 の例題であり，我々の型システムはこの例に. ル 2 の shift を用いた emit を表している．ここでは，. うな例は，実用的なプログラムにおいては頻出するも. 整数などの基本型や if-then-else などに対する型付け. のと考えられるが，従来研究では型付けすることがで. 規則が適宜追加されていると仮定する．. きず，本研究による型システムの優位性を示すもので. まず，関数 choice に対して次の型が導出できる．. choice : (int → (int, (string, T, T ), (string, T, T )), T, T ) 図 4 に示す導出により， M : (list int, U, U ) が導 出できる．ただし，list int は自然数のリスト型であ り，U は任意の型スキームである．この導出における. emit2 の本体の型を見ると，深さ 1 の Answer Type (string) と深さ 2 の Answer Type (list int) が異なっ. 対しても型が付けられることを確認している．このよ. ある．. 4. 型システムの性質 この章では，前章で定義した λSm に対する型シス テムに対して望ましい性質が成立することを示す．. 4.1 λSm と CPS の対応 前章の型システムが，CPS 変換と整合していること を示す．すなわち，λSm で型付けされた項は，CPS 変換により単純型付きラムダ計算 λ→ の項に変換さ.
(8) Vol. 48. No. SIG 10(PRO 33). 階層化コントロールオペレータに対する型システムの構築. 145. 以下の導出における 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 → int, k → (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) emit2 (choice 3); “no”1 : (string, T, T ) nil : (list int, T, T ) emit2 (choice 3); “no”1 ; nil : (list int, T, T ) emit2 (choice 3); “no”1 ; nil2 : (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 → 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.. れ，また，λSm での計算は，CPS 変換により単純型 付きラムダ計算 λ. →. における計算に変換されること. 使って「任意の型スキーム」を表現できるようにした が，CPS 変換の際にはそのような型 ∗ を展開して，高 さ m + 1 の木にする必要があるためである☆ ．なお，. を示す． 型と型スキームに対する CPS 変換を次のように定 義する．ただし，λSm の基本型は，単純型付きラム ダ計算の基本型であると仮定する．また，X は λ→ における特定の型を 1 つ選んで固定したものであり，. 上記の定義を展開していくと，i < 0 となることもあ るが，特に問題は生じない． 定理 1（CPS 変換による型付けの保存） λSm に おいて Γ M : T が導けるならば，. i ≤ m + 1 とする（i ≥ 0 とは限らない）． [[ ]]i : 型スキーム → λ の型. . [[∗]]i =. X (X → [[∗]]i−1 ) → [[∗]]i−1. [[Γ]] λ→ Cm+1 [[M ]] : [[T ]]m+1 が導ける．ここで，λ→ は，単純型付きラムダ計算. →. i ≤ 0 のとき i > 0 のとき. [[(τ, T, S)]]i = ([[τ ]] → [[T ]]i−1 ) → [[S]]i−1 [[ ]] : 型 → λ→ の型 [[b]] = b [[τ → T ]] = [[τ ]] → [[T ]]m+1 [[ ]] : 型環境 → λ→ の型環境 [[[ ]]] = [ ] [[Γ[x → τ ]]] = [[Γ]][x → [[τ ]]] 上記の定義で，型スキーム T に対する変換は，i と いうインデックスを持ち，[[T ]]i という形で与えられ ている．その理由は，我々の型システムにおいては， 型スキームが煩雑になるのを避ける工夫として，∗ を. λ→ における型の導出である． 定理 1 は，本論文の型システムで型が付く項は， CPS 変換すると λ→ で型が付く項になることを示し ている．証明は，付録の A.1 節と A.2 節に記載した． 定理 2（CPS 変換による項の等しさの保存）λSm に対して，Γ M : T が導け，さらに M → N であ るならば，. Cm+1 [[M ]] =βη Cm+1 [[N ]] である．ここで，=βη は単純型付きラムダ計算 λ→ に おける βη-equality を表す． 証明．文献 7) は，階層化 shift/reset に対する型の. free を与え，本論文で述べた CPS 変換 ない体系 λSm ☆. CPS 変換の定義から分かるように，CPS 変換後の項は必ず (m + 1) 個の継続を受け取るため，その型を木として見た場合， 高さが (m + 1) 以上になる．.
(9) 146. 情報処理学会論文誌：プログラミング. に関して健全かつ完全な等式系を与えた．この等式系 の一部は以下のとおりである（ただし，j ≥ n とし， 記法は本論文のものに合わせた）．. N に対して，M m → N m となる．さらに定理 3 から，[ ] N m : T が導ける． （証明終わり） 静的に型付けされたプログラミング言語にとって，. (λx.M )V = M {x := V } V n = V. 型システムの健全性は必要最低限の性質であり，この 性質だけで十分であるとはいえないが，本研究の型シ. E n [Sn k.M ]j = M {k := λx.E n [x]n }j free これらの等式から，λSm で M → N であれば，λSm で M = N である．さらに，λS free に対する CPS 変 m. 換の健全性7) より，型のない純粋なラムダ計算の体系 において，Cm+1 [[M ]] =βη Cm+1 [[N ]] である．この式 の両辺は，定理 1 と後述する定理 3 より λ. June 2007. →. ステムは，階層化 shift/reset を静的に型付けされたプ ログラム言語で用いるための基礎となると考えられる．. 5. まとめと今後の課題 継続を扱うためのコントロールオペレータである. 可能なので，λ→ において Cm+1 [[M ]] =βη Cm+1 [[N ]]. shift/reset は様々なプログラムの制御を表現できるう え，形式的に扱いやすいという特徴がある．1 つのプ. である． （証明終わり）. ログラムの中で shift/reset を複数の目的に用いると，. で型付け. 4.2 型システムの健全性 型システムの健全性は，型の保存（Subject Reduc-. 互いに干渉を起こし，意図どおりに動作しないことが あるため，階層化 shift/reset が提案された．これま. tion，Preservation）と計算の進行（Progress）の 2 つ. で，この階層化 shift/reset に対する型システムとし. の性質から構成される．. て十分なものは提案されてこなかった．. 定理 3（型の保存） λSm の項 M ，N ，型環境 Γ，. 本研究は，型スキームのアイディアに基づき，階層化. 型スキーム T に対し，Γ M : T が導出できて. shift/reset に対する型システムを与えた．また，その. M → N であれば，Γ N : T が導出できる．. 性質について検討し，今回定義した型システムが CPS. この定理により，項に型が付くならば，その項の実. 変換と整合し，かつ，健全であることを示した．この. 行中に型エラーが起きないことが保証される．証明は. 型システムは，階層化 shift/reset と Answer Type の. 付録 A.3 を参照されたい．. 変化の両方に対応した初めてのものである．. 定理 4（計算の進行） λSm の項 M ，型スキーム T に対して [ ] M m : T が導けるならば，M m. えられる．以下では，そのような課題のいくつかに言. は，評価規則を適用して計算を進めることができる．. 及する．. 本研究は，今後様々な研究に発展していくことが考. この定理で，M m の形をした項に限定しているの. • 型推論：本研究の型システムは主型（principal. は，reset で囲われていない shift を持つ項は，いわば. open term であり，計算が進まないためである．たと. type）を持つ．これに基づき，第 1 著者はこの 型システムに対する型推論アルゴリズムを実装し. えば，S1 k.λx.x は，そのままでは評価が進まない．こ. た11) ．しかし，これはプロトタイプ実装であり，. の体系のプログラムは，自由変数がなく，かつ，プロ. 本格的プログラムに対する有効性の検証は今後の. グラム全体がレベル m の reset で囲われているもの. 課題である．. 上記の定理により，M m が型が付くならば，その. • 多相性との共存：多相型と call/cc などの副作用が 共存すると，型の健全性に問題が生じることが古. 項の計算が進むことが示される．証明は付録 A.4 を. くから論じられており，ML 言語では多相性を制. 参照されたい．. 限する方法がとられている．本論文の shift/reset. と定めれば，上記の定理を適用することができる．. これら 2 つの定理を組み合わせると，次の健全性定 理が得られる． 定理 5（型システムの健全性） λSm の項 M と 型 スキーム T に対し，[ ] M m : T が導けるならば，. についても同様の制限のもとで多相性と共存でき ると予想している．また，ソース言語の多相性だけ でなく，CPS 変換後の多相性（いわゆる Answer. M は値であるか，あるいは，ある項 N が存在して M m → N m かつ [ ] N m : T が導ける．. Type 多相性）との関連も興味深い課題である． • 強正規化性：本論文では，停止性（強正規化可能 性）について議論することができなかった．これ. 証明．[ ] M m : T が導けたと仮定すると，定理. は，いわゆる管理レデックス（CPS 変換の際に生. 4 から，M m は 1 ステップ計算可能である．M が. じるレデックス）を生成しない CPS 変換を定義. 値でなければ，この 1 ステップの計算によって一番外. することにより証明できるという見通しを持って. 側の reset がなくなることはない．したがって，ある. おり，検討中である．.
(10) Vol. 48. No. SIG 10(PRO 33). 階層化コントロールオペレータに対する型システムの構築. 謝辞 第 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, Proc. 1990 ACM Conference on LISP and Functional Programming, Nice, New York, NY, pp.151–160 (1990). 5) Felleisen, M.: The Theory and Practice of First-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 Sound and Complete Axiomatization of Delimited Continuations., Proc. International Conference on Functional Programming, pp.177–188 (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: ATranslation at Work, Proc. 1st ACM Workshop on Continuations, Technical Report STAN-CS92-1426, Stanford University, pp.49–72 (1992). 11) 鈴木輝信：階層化コントロールオペレータに対 する型システムの構築，修士論文，筑波大学大学 院システム情報工学研究科 (2007). 12) 鈴木輝信，亀山幸義：階層化コントロールオペ レータに対する型システムの構築，日本ソフト ウェア科学会第 23 回大会講演論文集 (2006).. 付. 147. 録. 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 → φ] 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 定理 1 の証明 Γ M : T の導出の大きさに関する帰納法で証明す る．スペースの都合上，M = x，shift，reset のケー スのみを掲載する．. (i) M = x のとき 仮定より，Γ x : (τ, T, T ) がいえる．このとき. Γ(x) = τ となる．よって，(x → [[τ ]]) ∈ [[Γ]] である． 任意の型スキーム T に対して，次の型判断を導出 したい． [[Γ]] λ→ Cm+1 [[x]] : ([[τ ]] → [[T ]]m ) → [[T ]]m CPS 変換の定義から，Cm+1 [[x]] は以下のようになる． Cm+1 [[x]] = λκ1 . . . κm+1 .κ1 xκ2 . . . κm+1 補題 1 より，arity([[T ]]m ) ≥ m なので，適当な型 a1 , . . . , am , b に対して，[[T ]]m = a1 → . . . → am → b とおける．そこで，. Σ = [κ1 → [[τ ]] → [[T ]]m , κ2 → a1 , . . . κn+1 → an ] とおくと，. [[Γ]], Σ λ→ κ1 xκ2 . . . κm+1 : b.
(11) 148. 情報処理学会論文誌：プログラミング. となり，. [[Γ]] λ→ Cm+1 [[x]] : ([[τ ]] → [[T ]]m ) → [[T ]]m がいえる．. (ii) M = λx.M のとき，省略． (iii) M = M1 M2 のとき，省略． (iv) M = M n のとき 仮定から，Γ M n : (τ, T, T [rn ← S]) および ) が導出できる． Γ M : init(n, (τ, T [rn ], S), γ , W 帰納法の仮定により， )]]m+1 [[Γ]] λ→ Cm+1 [[M ]] : [[init(n, (τ, T [r n ], S), γ, W. が得られる．ここで，1 ≤ i ≤ n に対して，. wi = [[γi ]] → [[(γi , Wi , Wi )]]m−i+1. June 2007. Γ M : init(n, U [rn−1 ], γ , Z) n Γ = Γ[k → τ → (α, W [r ← T ], W [rn ← S])] がいえる．これに帰納法の仮定を適用すると，以下が 得られる．. m+1 [[Γ ]] Cm+1 [[M ]] : [[init(n, U [rn−1 ], γ , Z)]] yi = [[γi ]] → [[(γi , Zi , Zi )]]m+1−i とすると， m+1 [[init(n, U [rn−1 ], γ , Z)]] = y1 → y2 → . . . → yn → [[U [rn−1 ]]]m−n+1 となる．補題 1 より，[[U ]]m ,[[W ]]m はそれぞれ m 個 以上，[[T ]]m−n ,[[S]]m−n はそれぞれ m − n 個以上の. とすると，. )]]m+1 [[init(n, (τ, T [rn ], S), γ , W = w1 → . . . → wn → ([[τ ]] → [[T [rn ]]]m−n ) → [[S]]m−n と表せる．補題 1 より，[[T ]]m と [[S]]m−n はそれぞれ. m 個以上と m − n 個以上の引数を持つので， [[T ]]m = t1 → t2 → . . . → tm → t0 [[S]]m−n = s1 → s2 → . . . → sm−n → s0 とおけて，以下のようになる． n. [[T [r ]]]m−n = tn+1 → tn+2 → . . . → tm → t0 [[T [rn ← S]]]m = t1 → . . . → tn → s1 → . . . → sm−n → s0 ここで， Σ = [k1 → [[τ ]] → [[T ]]m , k2 → t1 , k3 → t2 , . . . kn+1 → tn ] Π = [v → [[τ ]], kn+2 → tn+1 , kn+3 → tn+2 , . . . km+1 → tm ] N = λvκn+2 . . . κm+1 .θ0 vκ1 . . . κn+1 κn+2 . . . κm+1 とすると， Σ, Π λ→ θ0 vκ1 . . . κn+1 κn+2 . . . κm+1 : t0 Σ λ→ N : [[τ ]] → [[T [rn ]]]m−n がいえる．さらに，. ∆ = [kn+2 → s1 , kn+3 → s2 , . . . km+1 → sm−n ] とおき，λ→ θi : wi (1 ≤ i ≤ n) に注意すると， [[Γ]], Σ, ∆ λ→ Cm+1 [[M ]]θ1 . . . θn N κn+2 . . . κm+1 : s0. となる．以上から，. [[Γ]] λ→ Cm+1 [[M n ]] : [[(τ, T, T [rn ← S])]]m+1 が導けて，このケースの証明を終了する． . (v) M = Sn k.M の場合 仮定から. Γ Sn k.M : (τ, U [rn−1 ← (α, T, S)], U ) かつ，. 引数をとるので以下のように表現できる．. [[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 このとき， [[U [rn−1 ]]]m+1−n = un → un+1 → . . . → um → u0 [[U [rn−1 ← (α, T, S)]]]m = u1 → u2 → . . . → un−1 → ([[α]] → [[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 → [[τ ]], κ1 → [[α]] → [[W [rn ← T ]]]m , κ2 → w1 , . . . , κn+1 → wn ,. κn+2 → s1 , . . . , κm+1 → sm−n ] Π = [w → [[α]], κn+2 → t1 , . . . , κm+1 → tm−n ] とすると， Σ, Π λ→ θ0 wκ1 . . . κn+1 κn+2 . . . κm+1 : t0 がいえる．ここで， N = λwκ n+2 . . . κm+1 .θ0 wκ1 . . . κn+1 κn+2 . . . κm+1. とすると，以下の型判断が導出できる．. Σ λ→ N : [[α]] → [[T ]]m−n さらに，. ∆ = [κ1 → [[τ ]] → [[U [rn−1 ← (α, T, S)]]]m , κ2 → u1 , . . . , κn → un−1 ] とすると，. [[Γ]], ∆, Σ λ→ θ0 vκ1 . . . κn N κn+2 . . . κm+1 : s0.
(12) Vol. 48. No. SIG 10(PRO 33). 149. 階層化コントロールオペレータに対する型システムの構築. が得られる．ここで，. p = λvκ1 . . . κm+1 .θ0 vκ1 . . . κn N κn+2 . . . κm+1. 2) (γ1 , W1 , W1 ) = init(n−1, (α, T [rn ], U ), γ 2 , W i はそれぞれ γ ，W の i 番目以降の変 ただし，γ i ，W. とすると，以下の型判断が得られる． n. [[Γ]], ∆ λ→ p : [[τ ]] → ([[α]] → [[W [r ← T ]]]m ) → [[W [rn ← S]]]m となる．一方， ]m+1 [[Γ ]], ∆ λ→ Cm+1 [[M ]] : [[init(n, U[r n−1 ], γ , Z)]. が成立するので，L = (Cm+1 [[M ]]){k := p} と置く と，上記の型判断から以下が得られる．. m+1 [[Γ]], ∆ λ→ L : [[init(n, U [rn−1 ], γ , Z)]] さらに，λ→ θi : yi であり，. 数列とする．ここで，. 2) init(n − 1, (α, T [rn ], U ), γ 2 , W = (γ2 , (γ2 , W2 , W2 ), 3 )) init(n − 2, (α, T [rn ], U ), γ 3 , W であるから，これらの関係式から以下の等式が得ら れる．. γ1 = γ2 W1 = (γ2 , W2 , W2 ). Ψ = [κn+1 → un , . . . , κm+1 → um ] とすると， [[Γ]], ∆, Ψ λ→ Lθ1 . . . θn κn+1 . . . κm+1 : u0. 3) = init(n − 2, (α, T [rn ], U ), γ 3 , W この W1 に対しての等式より，最初と同じような関係 が出てくる．このような計算を同様に繰り返していく. が成立するので，. と，結局，以下の等式が得られる．. [[Γ]] λ→ Cm+1 [[Sn k.M ]] : [[(τ, U [rn−1 ← (α, T, S)], U )]]m+1 となるため，このケースでも定理は成立する． （証明終わり）. γi = γi+1 Wi = (γi+1 , Wi+1 , Wi+1 ) γn = α Wn = T [rn ] = U. (1 ≤ i ≤ n − 1). A.3 定理 3 の証明 それぞれの評価規則ごとに証明する．なお，E[R] →. この関係より，それぞれの型判断は以下のように書き. E[M ] の形の評価規則では，外側の評価文脈 E を除 去して（E = [ ] と仮定して）R → M に対する型の 保存を証明すればよいことがすぐに分かるので，以下. Γ V n : (α, T, T ) Γ V : (α, W1 , W1 ) 補題 2 より，Γ V : (α, W1 , W1 ) から Γ V :. ではその形で証明する．. (i) (λx.M )V → M {x := V } Γ (λx.M )V : T より，以下の導出を得る．ただし， T = (α, S, U )，X ∗ = (X, U, U ) とする． Γ[x → β] M : (α, S, U ) Γ λx.M : (β → (α, S, U ))∗ Γ V : β ∗ Γ (λx.M )V : (α, S, U ) 補題 3 と Γ[x → β] M : (α, S, U ), Γ V : (β, U, U ) より，以下が導ける．. Γ M {x := V } : (α, S, U ). 換えられる．. (α, T, T ) がいえる．よって，定理は成立する． (iii) E n [Sn k.M ]j → M {k := λx.E n [x]n }j (n ≤ j) まず，仮定と型付け規則から，以下の導出を得る．. Γ E n [Sn k.M ] : init(j, (τ, T [rj ], X), γ , S) Γ E n [Sn k.M ]j : (τ, T, T [rj ← X]) 以下では，煩雑さを避けるため，init の第 3，第 4 引. の記述を省略する．補題 4 から， 数 ( γ , S). (ii) V n → V. Γ Sn k.M : (φ, U, V [rn−1 ← init(j − n, (τ, T [rj ], X))]) を得る．この判断を結論とする導出を考えると，最後. 仮定より，Γ V n : (α, T, T [rn ← U ]) である．. に適用する規則は shift であるので，. よって，定理は成立する．. reset の規則より，以下が得られる． ) Γ V : init(n, (α, T [rn ], U ), γ , W Γ V n : (α, T, T [rn ← U ]) ) の部分は，値に ここで，init(n, (α, T [rn ], U ), γ , W. U = V [rn−1 ← (ψ, W, Y )]. (1). となり，以下の判断を得る．. Γ M : init(n, init(j − n, (τ, T [rj ], X))) Γ = Γ[k → φ → (ψ, Z[rn ← W ], Z[rn ← Y ])]. 対する型スキームなので，その左部分木と右部分木の. k に λx.E n [x]n を代入しなくてはならないので，そ れぞれが同じ型を持たなくてならないが，それは，以. 型スキームは等しくなる．よって，以下の関係が得ら. 下の導出で確認できる．ただし，A = (ψ, Z[rn ←. れる．. W ], Z[rn ← Y ]) とする．.
(13) 150. June 2007. 情報処理学会論文誌：プログラミング. Γ[x → φ] x : (φ, U, V [rn−1 ← (ψ, W, Y )]) Γ[x → φ] E n [x] : init(n, (ψ, W, Y )) Γ[x → φ] E n [x]n : A Γ λx.E n [x]n : (φ → A, Z0 , Z0 ) (1) より，U = V [rn−1 ← (ψ, W, Y )] なので，この 型判断は正しい．補題 3 と， Γ M : init(n, init(j − n, (τ, T [rj ], X))) Γ λx.E n [x]n : (φ → (ψ, Z[rn ← W ], Z[rn ← Y ]), Z0 , Z0 ). N1 が 2，3，4，5 のいずれかの形のときは，評価 文脈 E を EN2 に置き換えれば M 全体が 2，3，4，. 5 の形であることがいえる．N1 が 1 の形で，N2 が 2，3，4，5 のいずれかの形のときは，E を N1 E に 置き換えればよい．N1 も N2 も 1 の形のときは，M に自由変数がないので N1 は変数ではありえず，ラム ダ抽象である．したがって，N1 N2 は 2 の形になって いる． （証明終わり） 定理 4 の証明：. [ ] M m : T が導けると仮定する．M m は，上. より，以下の判断が得られる．. 記の補題で述べた 1，2，3，4，5 のいずれかの形であ. Γ M {k := λx.E n [x]n }. るが，1 と 4 はありえない．したがって，2，3，5 の. : init(n, init(j − n, (τ, T [rj ], X))) これに reset 規則を適用すると， Γ M {k := λx.E n [x]n }j : (τ, T, T [rj ← X]) となり，定理は成立する． （証明終わり）. A.4 定理 4 の証明. いずれかの形であり，これらはいずれも評価規則の左 辺になっているので，1 ステップの計算が可能である． （証明終わり）. (平成 18 年 12 月 16 日受付) (平成 19 年 3 月 18 日採録). この定理をやや一般化した以下の補題を証明する． 補題 5 項 M ，型スキーム T に対して [ ] M : T が導けるならば，以下のいずれかが成立する．. 鈴木 輝信 筑波大学大学院システム情報工学. 1. M は値． 2. M は E[(λx.M )V ] の形．. 研究科コンピュータサイエンス専攻. 3. M は E[E n [Sn k.M ]j ] の形（ただし， j ≥ n）． 4. M は E n [Sn k.M ] の形．. の型システムに関する研究を行う．. 5. M は E[V n ] の形． 証明．M に関する帰納法で証明する． M = N1 N2 の場合だけを述べる．M が型付け 可能なので，適当な型スキーム T1 ，T2 に対して， [ ] N1 : T1 と [ ] N2 : T2 が導ける．そこで 帰納法の仮定を使うと，N1 ，N2 は，上記の 1，2，3， 4，5 のいずれかの形である．. 博士前期課程在学．プログラム言語 日本ソフトウェア科学会会員． 亀山 幸義（正会員） 筑波大学大学院システム情報工学 研究科コンピュータサイエンス専攻 准教授．プログラムの論理とソフト ウェア検証に興味を持つ．ACM，日 本ソフトウェア科学会各会員．.
(14)
図
関連したドキュメント
この論文の構成は次のようになっている。第2章では銅酸化物超伝導体に対する今までの研
2021] ．さらに対応するプログラミング言語も作
前章 / 節からの流れで、計算可能な関数のもつ性質を抽象的に捉えることから始めよう。話を 単純にするために、以下では次のような型のプログラム を考える。 は部分関数 (
本論文での分析は、叙述関係の Subject であれば、 Predicate に対して分配される ことが可能というものである。そして o
つまり、p 型の語が p 型の語を修飾するという関係になっている。しかし、p 型の語同士の Merge
英語の関学の伝統を継承するのが「子どもと英 語」です。初等教育における英語教育に対応でき
本案における複数の放送対象地域における放送番組の
