20(212)
特集●プログラミング及びプログラミング言語

静的かつ動的な式を許すような部分評価器のための
束縛時解析
浅井 健一

本稿では，関数型言語の部分評価器で構造データの扱いを向上すべく，静的かつ動的な値を許すような束縛時ている [3]．また，近年ではオブジェクト指向言語の最適化等にも利用されるようになってきている [6] [4]．

解析を提案する．静的かつ動的な値を使うと，静的に構

部分評価の中でも oﬄine の部分評価と呼ばれる方法

造データにアクセスしつつ，その構造データを（動的なでは，部分評価をプログラム解析のフェーズ（束縛時解値として）コードに残すことができるようになる．この析 BTA と呼ばれる）とプログラム特化のフェーズに方法は実質的に，従来，許されていなかった構造データわけて行う．解析のフェーズでは，プログラムを部分評の lift を許すようにした，と見ることもできる．本稿で価時に実行可能（静的 static）な部分と不可能（動的提案する束縛時解析は，型システムとして定式化され，dynamic）な部分とにわけ，特化のフェーズでは静的な型推論の際に生成される束縛時に関する制約を解くこと部分を実行する．具体的な例を見てみよう．例えば

で結果を得る．さらに，アルゴリズムの正当性を示すと(lambda (x) ((lambda (y) y) x))

ともに，制約の解消が従来の効率的な束縛時解析と同じという式を考えてみる．この式を束縛時解析に通すと，

くほぼ線形時間でできることを示す．

最初の (lambda (x) ...) の部分はまだ実行できないが，その中の ((lambda (y) y) x) の部分は実行でき

1 はじめにる，という結果が返ってくる．そこで束縛時解析の結果

部分評価 (partial evaluation) [12] とは，プログラム

として，実行できる部分は実行し，実行できない部分はと引数の一部を受け取って，その既知の引数の情報から実行時に実行されるようなコード（あるいはプログラム計算できる部分を先に計算してしまうことでプログラム

テキスト）†1 を出力する．これは簡単には以下のようにの効率をあげるプログラム変換である．部分評価の技法

quasiquote と unquote を使えば良い．

を使うとインタプリタからコンパイラを生成できる [7]，‘(lambda (x) ,((lambda (y) y) ’x))など応用が広いため，特に関数型言語の世界では多くの特化のフェーズでは，単にこれを実行すれば，部分評

研究がなされ，実際にいくつかのシステムが動くに至っ価の結果である (lambda (x) x) というプログラムテ

Binding-Time Analysis for a Specializer that Allows
Both Static and Dynamic Expressions
Kenichi ASAI, 東京大学大学院理学系研究科情報科学専攻/ 科学技術振興事業団 さきがけ研究 21 「情報と知」領域
グループ, Department of Information Science, Graduate School of Science, University of Tokyo / “Information and Human Activity,” PRESTO, Japan
Science and Technology Corporation (JST)コンピュータソフトウェア, Vol.17, No.3 (2000), pp.20–37.
[論文]1999 年 5 月 22 日受付.

キストを得ることができる．このとき，(lambda (x)...) の部分は quasiquote が付いたただのリスト（プログラムテキスト）であるのに対し，(lambda (y) y)
は実行されて closure が作られていることに注意しよう．

†1 本稿では「コード（表現）」と「プログラムテキスト」を同じ意味で使用する．これらは Scheme の場合にはリストである．

(213)

Vol. 17 No. 3 May 2000

(let ((lst (list (cons 1 2) (cons 3 4)
(cons 5 6)))); ペアのリストで表された点列(lambda (r)(define (near? pair rr); (x 座標)2 + (y 座標)2 < r2 かを判定する(< (+ (* (car pair) (car pair))(* (cdr pair) (cdr pair)))
rr))(define (take-near l rr); l の中から原点に近いものを抽出する(cond ((null? l) ’())((near? (car l) rr)(cons (car l)(take-near (cdr l) rr)))(else (take-near (cdr l) rr))))(take-near lst (* r r))))
図1

原点から距離 r 以内の点列を返すプログラム

このように oﬄine の方法は，解析のフェーズであら21(let ((c0 (cons 1 2)) (c1 (cons 3 4))(c2 (cons 5 6)))(lambda (r)(let ((rr (* r r)))(cond ((< 5 rr)(cond ((< 25 rr)(if (< 61 rr)(list c0 c1 c2)(list c0 c1)))((< 61 rr) (list c0 c2))(else (list c0))))((< 25 rr)(if (< 61 rr) (list c1 c2)(list c1)))((< 61 rr) (list c2))(else ’())))))
図2

特化した結果従って (f 3) の実行も行われない．

かじめ実行可能な部分を分離し，それらを特化時に（シ同様の問題は closure 以外の構造データについても起

ンボリックに実行するのではなく）直接実行してしまう

きる．例えば，図 1 の例を見てみよう．このプログラム

ため，特化を効率的に行えるという特徴を持つ．その一は，cons セルのリストで表現された点列 lst のうち，方で，直接実行されるときの実行時データとそのコード

原点から距離 r 以内にある点を抽出するものである．こ表現が食い違うため，分離がきれいにできないと十分な

こでは，このプログラムで点列 lst が具体的に与えら特化ができない，という問題点がある．例えば，れた場合の部分評価を考えている．

((lambda (f) (cons f (f 3)))(lambda (x) x))

今，lst が具体的に与えられているので take-nearの再帰や near? における (x 座標)2 × (y 座標)2 の計算という式を考えてみよう．ここでは部分評価時に (f 3)などを実行して，図 2 のような結果を得たい．これは，を実行したいので cons のみを動的 (lambda (x) x)

各点に関してあらかじめ距離の計算を行っておき，後でを含む他の部分を静的として以下のようにしたい．

r が与えられたときに，素早く結果を返せるようにした，((lambda (f) ‘(cons ,f ,(f 3)))と見ることができる．

(lambda (x) x))

しかし，図 1 のプログラムを従来の束縛時解析にかけ

ところがこの式を実行すると

ると lst の各要素が全て動的となってしまうため take-(cons #[procedure #x1359A08] 3)

near の再帰は展開されるが (x 座標)2 × (y 座標)2 の計のような結果が返ってくる．実行時データとそのコード

算は一切行われない．lst の各要素が動的になってしま表現が異なるため，(lambda (x) x) というコードがう理由は，take-near 中の cond 文の 2 つ目の節（四残って欲しいところに実行時の値である #[procedure

角で囲まれている部分）で，(car l) が最終結果に出#x1359A08] が出てきてしまうのである．ここでの問題

力されているためである．(car l) には lst 中の各要

点は (lambda (x) x) を静的に使うため closure を作

素がきうるが，それらを最終結果のコードに残すため，成したが，実は同時にそのコード表現も必要であった，

そのコード表現が必要となるのである．このことは，仮という点である．このような場合，従来の部分評価器に lst の各要素を静的と分類し，最終結果に残る (carでは（closure からそのプログラムテキストを復元する

l) を静的のまま，特化を実行して見るとわかる．そののが容易でないため）(lambda (x) x) は動的となり，結果は，図 2 とほぼ同じものが得られるが，第１行目が

22

コンピュータソフトウェア(214)(let ((c0 (1 . 2))(c1 (3 . 4))(c2 (5 . 6)))

以下，2 節で本稿で扱う言語を説明し，3 節では特化という誤ったものになってしまう．各要素が静的のため器を示す．4 節で束縛時型を導入した後，5 節に注釈の(cons 1 2) のようにコードにはならず (1 . 2) といついた言語に対する型規則（型チェック規則）を示し，6

う値になってしまうのである．Lift 命令を使って (1 .

節でその健全性を示す．7 節ではこの規則を注釈のつい2) という値を (cons 1 2) というコードに変換するこていない言語のものに変換し，制約生成の規則を得る．

とができれば問題が解決するように感じられるかも知れ

型チェック規則と制約生成規則の等価性は 8 節で示されない．しかし，lift は通常，定数にのみ認められ，構造る．9 節で，制約解消時に使う型の解釈を示し，10 節でデータには使用することができない．これは構造データ

実際に制約解消アルゴリズムを述べる．11 節で制約解に lift を使うと，データ構造の定義が複製される可能性

消の例を示した後，12 節でそのアルゴリズムの正当性があること，closure のようなデータ構造は値からコーを示すとともに，13 節ではその計算量も述べる．関連

ドに変換するのが自明ではないこと，などのためである．

研究を 14 節で述べ，15 節でまとめる．

ここでの問題は，lst の各要素が静的な計算に使われると同時に，コードとして最終結果にも残る（動的にも2 言語

使われている），という点である．このような式を，本本稿で扱う言語は，以下に示すような関数型言語の一稿では静的かつ動的 (both static and dynamic) な式

部で，高階関数，関数適用，primitive の適用，そしてと呼ぶことにする．静的かつ動的な式については，部分

構造データとして cons, car, cdr を扱う．ここでは簡単

評価時にその値を使った計算をしつつ，最終結果に残るのため再帰を扱っていないが，再帰が入っても本稿の枠部分についてはコード表現を出力したい．これを実現す

組は問題なく拡張できることがわかっている．

るため，静的に使われる値とそのコード表現の両方を渡L=x | λx. L | L@L | cons L L |car L | cdr L | 定数 | L + L

す，という方法を提案する．この手法によって，従来，最終結果に残るために動的となっていたデータ構造に対言語 L のプログラムを受け取ると，束縛時解析は注釈

しても，部分評価時にアクセスできるようになる．先のの付いたプログラムを返す．従来の束縛時解析では，注

例では，lst の各要素に部分評価時にアクセスしつつ，

釈は S （静的）または D （動的）の２種類であったが，そのコード表現を最終結果に残し，図 2 の結果を得るこ

これに加えて本稿では B（静的かつ動的）も許す．以下とができるようになる．

に，注釈の付いた言語の定義を示す．

しかし，このように値とコード表現の両方を渡すよM =x | λS x. M | λD x. M | λB x. M |うにすると，従来の片方しか渡さなかった場合に比べて

M @S M | M @D M |オーバーヘッドがかかる．従って，可能な全ての値を静cons S M M | cons D M M | cons B M M |的かつ動的と扱うのは好ましくない．本稿では，束縛時

car S M | car D M | cdr S M | cdr D M |解析を型システムとして定式化し，実際に静的かつ動的定数S | 定数D | 定数B |B
M +S M | M +D M | M↓B
S | M↓Dに使われる可能性のある部分を特定することで，オーバーヘッドをなるべく抑えるようにしている．

B

λ x. M および cons B M M がそれぞれ静的かつ動的同じ式に複数の束縛時を許す一般的な束縛時解析としBな関数，ペアを返す命令である．また，M↓B
S と M↓Dては polyvariant な束縛時解析があげられる．しかし，はそれぞれ，静的かつ動的な値を受け取ったら，その静

polyvariant な解析はコストが非常に高いことが知られ的な部分，動的な部分を返す命令である．この 2 つを本ている [2]．ここでは扱える束縛時を静的かつ動的なもの

稿では型変換命令と呼ぶ．

までに限ることで monovariant な解析の効率を損なうことなく，構造データの扱いを向上することを目指している．実際，本稿で示す束縛時解析は，従来のものと同
じくほぼ線形でできることがわかっている．

以下では，注釈の付いた式 M から，全ての注釈と型変換命令を取り除いた式を |M | と書くことにする．

(215)

Vol. 17 No. 3 May 2000

23

S : Exp → Env→

W + {error}

S [[x]] ρ=ρ(x)S [[λ x. M ]] ρ=

λx′ . S [[M ]] ρ[x′ /x]S [[λD x. M ]] ρ=

build-λ(x⋄ , S [[M ]] ρ[x⋄ /x])S [[λB x. M ]] ρ=

(build-λ(x⋄ , D(S [[M ]] ρ[x⋄ /x])), λx′ . S [[M ]] ρ[x′ /x])

S [[M1 @ M2 ]] ρ=

(S [[M1 ]] ρ)@(S [[M2 ]] ρ)

S [[M1 @ M2 ]] ρ=

build-@(S [[M1 ]] ρ, S [[M2 ]] ρ)S

S [[cons M1 M2 ]] ρ=

(S [[M1 ]] ρ, S [[M2 ]] ρ)S [[cons M1 M2 ]] ρ=

build-cons(S [[M1 ]] ρ, S [[M2 ]] ρ)S [[cons M1 M2 ]] ρ=

let (m1 , m2 ) = (S [[M1 ]] ρ, S [[M2 ]] ρ)

S

S

D

D
B

in (build-cons(D(m1 ), D(m2 )), (m1 , m2 ))S [[car M ]] ρ=

#1 (S [[M ]] ρ)S [[car M ]] ρ=

build-car (S [[M ]] ρ)

S [[定数 ]] ρ=

定数S [[定数 ]] ρ=

lift(定数)S [[定数B ]] ρ=

(lift(定数), 定数)S [[M1 +S M2 ]] ρ=

(S [[M1 ]] ρ) + (S [[M2 ]] ρ)

S [[M1 + M2 ]] ρ=

build-+(S [[M1 ]] ρ, S [[M2 ]] ρ)

S [[M↓B
D ]] ρ

=#1 (S [[M ]] ρ)

S [[M↓B
S ]] ρ

=#2 (S [[M ]] ρ)

S

D

S

D

D

図3

3 特化器

特化器

W

=

WS + WD + WB

図 3 と図 4 に注釈の付いた言語 M に対する特化器をWS=

Int + (W → W ) + (W × W )示す．図中で let x = a in M は (λx. M )@a の略記，

WD

=

Code

D(M ) は M が静的かつ動的だった場合にそのコード部分を取り出す命令†2 ， x⋄ は（Scheme 等の処理系にWB=

WD × WS

Env=

Var → Wある gensym 命令によって）新たに生成された変数（のコード表現），#1 と #2 はペア (A, B) の car 部分，

{
D(M )

=

cdr 部分をとってくる命令である．
#1 (A, B) = A,

#2 (A, B) = B

図4#1 (M )

if M is bothM

if M is dynamic

Semantic Domain と関数 D(·)

また lift は定数やシンボルなどの非構造データの値をプ
ログラムテキストに変換する命令，build- はコードを出力する命令で，例えば Scheme のコードを出力するな
ら図 5 のようになる．
†2 ここでは簡単のため特化時に M の束縛時をチェックする
ように書いているが， M の束縛時は束縛時解析が終了した時点でわかっているので，それに従って規則を（M が静的かつ動的な場合と動的な場合の）2 つに分ければ，特化時に束縛時をチェックする必要はない．

build-λ(x⋄ , N )=(lambda (x⋄ ) N )build-@(N1 , N2 )=(N1 N2 )build-cons(N1 , N2 )=(cons N1 N2 )build-car (N )=(car N )build-+(N1 , N2 )=(+ N1 N2 )図5

Scheme 用の build- 関数

コンピュータソフトウェア

24

(216)

図 3 の特化器はごく標準的なものである．静的な命令については普通のインタプリタと全く同じように実行し，

4 束縛時型と型に対する制限

動的な命令については，そのコードを出力している．従

本稿で扱う束縛時解析は，型システムとして定式化さ来の特化と異なるのは，静的かつ動的な命令で，この場れており，そこで使われる各式の束縛時の値 π と型 τ

合は，後に静的にも動的にも使われる可能性があるので，は以下のように定義される．

両方を作りペアにして渡している．これらは，その後の

π

=

S|D|B

B
特化で必要に応じて型変換命令 M ↓B
D や M ↓S によっτ=Intπ | τ →π τ | τ ×π τてその動的な部分，静的な部分が取り出されることとな

束縛時値 π は S （静的），D （動的），または B （静る．ここで使われるペアは cons 命令で作られるペアと的かつ動的）である．また，束縛時型 τ は，定数（ここ同じものを使用しているが，これらは後に述べる型シス

では代表として整数を扱う），関数，またはペアである．

テムで明確に区別されるので，混同されることはない．

各束縛時型 τ には，束縛時値 π が肩に付与されており，

本稿では，定数も静的，動的，静的かつ動的の３種類

これで束縛時値が π であるような束縛時型を示す．以に厳格に区別しているが，これは，定数を他の構造デー

下，束縛時型 τ の束縛時値が π であることを明示する

タと同じく統一的に扱うためである．しかし，必ずしも，必要があるときには τ π と書き，π を τ の（トップレベ

図 3 にある通り静的かつ動的な定数の表現として，静的ルの）束縛時値と呼ぶ．

な定数と動的な定数の両方を持っておく必要はない．静的な定数のみを持っておき，

ここでは，簡単のため部分評価されるプログラムは，束縛時値を取り除いた型に関して simply typed であS [[定数↓B
D ]] ρ

=lift(定数)

る，と仮定する．すると，束縛時解析は，従来通りの手

S [[定数↓B
S ]] ρ

=定数法を使って（束縛時値なしの）型を求めたあと，各型にとすることで，従来と同様に定数を扱うことができる．

つく束縛時値を決定するのが主要な仕事となる．

図 3 では簡単のため，コードを残す際に let 文の挿入

上記で定義される束縛時型は，全てが有効な束縛時を行っていない．そのため，プログラムによってはコー型である，というわけではない．例えば，動的なペア型

ドの複製，消去，実行順の入れ換えが起きる可能性があτ1 ×D τ2 に現れる τ1 , τ2 はともに束縛時値 D を持たる．この問題を避けるためには，従来通りの方法を使っなくてはいけない．これは，ペア全体が最終結果にコーて，コードが生成されるたびに（具体的には build- 命

ドとして残るなら，ペアの各要素も残るためである．こ令が呼ばれるたびに）let 文を挿入すれば良い．

のように構造データ（関数，ペア）については，全体の図 3 の特化器は，関数以外のものを適用したり，コー

束縛時値と要素の束縛時値の間に制約がある．そこで，

ド以外のものから build- によってコードを作ろうとする

有効な束縛時型を以下のように定義する．

とエラーを起こす．6 節では，プログラムの注釈がきち

定義 1 束縛時型は以下の場合にのみ有効である．

んと付けられていれば，そのプログラムの特化でエラー

1. Intπ は（π の値にかかわらず）有効．

が起きることはないことを見る．

2. τ1π1 →π τ2π2 は，π ▷′ π1 かつ π ▷ π2 なら有効．

プログラム M が与えられたときに，その特化を行う

3. τ1π1 ×π τ2π2 は，π ▷ π1 かつ π ▷ π2 なら有効．

には，初期環境 ρinit を使って S [[M ]] ρinit を計算する．

ここで，π1 ▷ π2 と π1 ▷′ π2 が構造データに関する制約

ここで初期環境 ρinit は，全ての変数に対して未定義で

で，以下のように定義される．

ある（エラーを返す）ような環境である．
（特化する式

S▷S

S▷D

S▷B

D▷D

B▷D

が閉じた式ではなく，あらかじめ定義された大域変数等

′

′

′

S▷ S S▷ D S▷ B′′

がある場合には，それに対する束縛が ρinit に入ってもπ1 が S のときは π2 は何でも良いが，π1 が D のとよい．
）

きは π2 も D でなくてはならない．これは，構造データ

D▷ D

B▷B

B▷ D

のトップレベルの束縛時値が S ならその各要素は何でも良いが，トップレベルの束縛時値が D になったら各(217)

Vol. 17 No. 3 May 2000

25

要素も D になる，ということを意味している．ここまるときに引数に関して何も仮定できないので，引数は動では，従来の場合と同様である．

的とせざるを得ない．monovariant な解析ではプログ

π1 が B だったときには，π2 として D と B を許す′

ラム各部に 1 つの束縛時しか割り当てられないので，こもの (▷) と D のみしか許さないもの (▷ ) の２種類がのλ式が別のところで静的に使われ，そこで静的な引数

ある．どちらの場合も π2 として S が許されないのは，を渡されたとしても，それは動的とせざるを得ないので構造データの束縛時値が B になったら，その各要素のある．

コード表現が必要となるためである．例えば，図 3 のB

解析を monovariant にしているのは効率のためであcons M1 M2 の規則を見てみよう．この規則では，将る．polyvariant な解析はコストが非常に高いことが来，コード表現が必要になるのに備えて，全体のコード知られている [2] ので，ここでは，より効率的に行える表現を build-cons によって作っているが，このとき Mi

monovariant な解析を採用した．実際，13 節ではこのの束縛時値が S だと，そのコード表現が得られないた解析が効率的にほぼ線形時間で行えることを見る．まめ全体のコードを作ることができなくなってしまう．一た，上のような制限が付いていても，従来，静的かつ動方，Mi の束縛時値が D あるいは B なら，必ず Mi の的なλ式は全て動的と扱われてきていたので，従来のコード部分を取ってくることができるので大丈夫である．

monovariant な部分評価と比べればより部分評価できπ
π
これが，ペア型 τ1 1 ×π τ2 2 に対して π ▷ π1 , π ▷ π2 とるようになっている．

いう制約がついている理由である．
一方，関数型 τ1 1 →π τ2 2 の引数部分については，よ
π

π

5 型規則

り強力な制約 π ▷′ π1 がついている．これは「関数の束図 6 に注釈の付いた言語に対する型規則（型チェック

縛時値が B になったら，その引数の束縛時値は D でな規則）を示す．図中 Γ `1 M : τ π は，型環境 Γ のもと

くてはいけない」ということを意味している．この制限

で注釈の付いた式 M が型 τ π を持つことを示す．
（Γ がは，本稿の枠組からやむを得ず出てくるものである．

空の型環境のときは Γ を省略して `1 M : τ π と書く．
）

まず，この制限の意味するところを見るため，

静的かつ動的な値の型の有効性にだけ注意しておけば，

P = (λf. cons f (f @2))@(λx. x + 3)

これらの規則はいずれも標準的なものである．τ↓B
D の規という式を考えてみよう．λx. x + 3 は静的に適用さ則に出てくる [τ ]D というのは，τ D 中に出てくる全てれるとともに最終結果に残るので静的かつ動的であの束縛時値を D にしたものである．図中，唯一，特殊る．そこで静的な部分は計算し，動的な部分は残してなのは静的な加算の結果の型で，これらはいつも静的と

cons (λx. x + 3) 5 を結果として得たい．しかし，上のはせず，その使われ方によって何でも良いことにしてい制限から静的かつ動的な関数 λx. x + 3 の引数 x は動る．これは静的な定数はいつでも動的な定数に（従来の的となってしまうのである．これは λx. x + 3 が動的

lift 命令によって）変換できるからである．

な値として使われる場合に備えてそのコード表現を用

定義 2 注 釈 の 付 い た プ ロ グ ラ ム pann に 対 し `1

意する必要があるが，そのときは x に関する静的な情

pann : τ D が導けるとき，その注釈は有効である，と報が何もないためである．結果として + も動的となりいう．

cons (λx. x + 3) (2 + 3) しか得ることができないのである†3 ．

定義 3 同じプログラム p に対する有効な注釈 pann の

この静的かつ動的なλ式に対する制限は，本稿で扱う

うちで，以下の 2 つの性質を満たす注釈 p∗ann を最も望ましい注釈と呼ぶ．

束縛時解析が monovariant であることによる．λ式を

1. p の全ての部分式について，その束縛時値が pann

最終結果に残すためには，そのλ式の本体部分を解析すにおいて S なら， p∗ann においても S である．

†3 x を静的かつ動的とすることも不可能である．静的かつ動的な値は常に静的にも動的にも使用可能な値だが，λ式がコードに残るときの x は動的な情報しか持っていない．

2. pann と p∗ann で束縛時値が S である部分式が同一の場合には，それ以外の全ての部分式について，
その束縛時値が p∗ann において B なら，pann におコンピュータソフトウェア

26Γ, x : τ1π1 `1 M : τ2π2
Γ `1 λSΓ, x : τ1D `1 M : τ2π2

Γ, x : τ1D `1 M : τ2D

x. M : τ1π1 →S τ2π2

Γ `1 λD

x. M : τ1D →D τ2DΓ `1 M1 : τ2π2 →S τ1π1
Γ `1 M1 @Γ `1 M2 : τ2π2

Γ `1 M1 : τ1π1

Γ `1 M2 : τ2π2

Γ `1 M : τ1π1 ×S τ2π2

Γ `1 cons S M1 M2 : τ1π1 ×S τ2π2

Γ `1 car S M : τ1π1

Γ `1 M1 : τ1DSΓ `1 cons D M1 M2 : τ1D ×D τ2DΓ `1 car D M : τ1D

Γ `1 consB

πi ∈ {B, D}

M1 M2 : τ1π1 ×B τ2π2
図6

Γ `1 M2 : τ2DDΓ `1 M : τ1D ×D τ2DΓ `1 M2 : τ2π2

Γ `1 M1 : τ2D →D τ1D

M2 : τ1π1

Γ `1 M2 : τ2D

Γ `1 M1 : τ1π1

π2 ∈ {B, D}Γ `1 λB x. M : τ1D →B τ2π2

Γ `1 M1 @ M2 : τ1DΓ, x : τ `1 x : τ

π

π

(218)

Γ `1 M : τ BSΓ `1 M↓B
S: τΓ `1 M1 : IntSΓ `1 M2 : IntSΓ `1 M1 +S M2 : IntπΓ `1 M1 : IntDΓ `1 M2 : IntDΓ `1 M1 +D M2 : IntDΓ `1 M : τ BDΓ `1 M↓B
D : [τ ]Γ `1 定数π : Intπ

注釈の付いた言語に対する型規則（型チェック規則）

Γ1 `1 f : D →B DS
Γ1 `1 f↓B
Γ1 `1 2D : D
S: D → DDS DBBΓ1 `1 f↓D : D → DΓ1 `1 f↓S @ 2 : DΓ2 `1 x : D Γ2 `1 3D : D
S D
D
D
B
D
B
Γ1 `1 cons f↓D (f↓S @ 2 ) : (D → D) × DΓ2 `1 x +D 3D : D
S D
B
S
D
D
B
S
D
B
`1 λ f. cons f↓D (f↓S @ 2 ) : (D → D) → (D → D) × D `1 λB x. x +D 3D : D →B D
S D
S
B
D D
D
B
D) ×D D
`1 (λS f. cons D f↓B
D (f↓S @ 2 ))@ (λ x. x + 3 ) : (D →

Γ1 `1 f : D →B D

図7型チェックの例（Γ1 = f : D →B D, Γ2 = x : D, Int

いても B である．
直観的に解釈すると，第１点は S となっている部分がπを π と表記）

現在 S になっている部分を D にすることなく B を減らすことはできないので最も望ましい注釈である．

より多い，と言っており，これは，より多くの部分を部
分評価時に実行できることを示している．また，第２点6 型システムの健全性

は，S となっている部分が同じだったら， B となって

図 3 の特化器 S は，注釈の付いたプログラムに対しいる部分がより少ない，と言っており，これは，部分評て，図 4 に示されているドメイン上の表示的意味記述を

価時に静的かつ動的な値を作るオーバーヘッドがより少与えている，と見ることができる†4 ．図 6 に示された型ないことを示している．

システムが，この表示的意味記述に対して健全である，

束縛時解析は，注釈の付いていないプログラム p が与とは，ある式が型システムで型 τ π を持つことがわかっえられたときに，有効な注釈の付いたプログラム pannたら S は（エラーを起こすことなく）その型の値を返のうち，上の意味で最も望ましい注釈を返すもの，といす，と定義される．

うことができる．
型チェックの例として前節に出てきたP = (λf. cons f (f @2))@(λx. x + 3)という項を考えてみよう．この式は λx. x + 3 を静的かつ動的として図 7 のように注釈を付けることができる．
この注釈は，これ以上 S を増やすことができず，また，

ここで Vτ π を図 8 のように定義しよう．すると，型システムの健全性は，型 τ π の値の特化の結果が Vτ π に含まれている，と言い換えることができる．ここでは，†4 新たな変数の生成があるので，厳密には表示的意味記述ではないが，各関数に変数生成用の引数を 1 つ余計に渡すという標準的な方法でこの問題は回避できる．

(219)

Vol. 17 No. 3 May 200027⋄

合するので，帰納法の仮定により S [[M ]] ρ[x /x] ∈

VIntS

=

Int

Vτ π1 →S τ π2=

Vτ π1 → Vτ π2

Vτ π1 ×S τ π2=

Vτ π1 × Vτ π2

Vτ D

=

Code

Vτ B

=

Vτ D × Vτ S

図8

Vτ π の定義

1

2

1

1

2

Vτ D が成り立つ．従って，build-λ の引数がコード2となっているので

2

1

2

S [[λD x. M ]] ρ=

build-λ(x⋄ , S [[M ]] ρ[x⋄ /x])

∈

Code

=

Vτ D →D τ D
1

2（λB x. M の場合） 証明木の最後は

Γ, x : τ1D `1 M : τ2π2

これを証明していく．

π2 ∈ {B, D}Γ `1 λB x. M : τ1D →B τ2π2以下，型環境 Γ で x が τ π 型であるとき τ π = Γ(x)と書く．

となる．ρ が Γ に適合しているとしよう．x′ ∈ Vτ D

定義 4 特 化 時 の 環 境 ρ が 型 環 境 Γ に 適 合 し て い

なる全ての x′ に対して ρ[x′ /x] は Γ, x : τ1D に適る，とは，ρ(x) が定義されている全ての x について合するので，帰納法の仮定により S [[M ]] ρ[x′ /x] ∈ρ(x) ∈ VΓ(x) が成り立つことを言う．

Vτ π2 (π2 ∈ {B, D}) が成り立つ．従って，

12型規則の健全性は以下のように述べられる．

λx′ . S [[M ]] ρ[x′ /x]定理 1 （型規則の健全性） 図 6 の規則で Γ `1 M : τ π
が 導 け る な ら ，Γ に 適 合 す る 全 て の ρ に つ い て ，∈Vτ D → Vτ π2=

Vτ D →S τ π2

1

2

1

2

⋄

S [[M ]] ρ ∈ Vτ π が成り立つ．

また，x ∈ Vτ D なる全ての x に対して ρ[x⋄ /x]

証明： Γ `1 M : τ π の証明木の深さに関する帰納法で証は Γ, x : τ1D に適合するので，帰納法の仮定によ明する．以下，M として x, λS x. M , λD x. M , λB x. M

り S [[M ]] ρ[x⋄ /x] ∈ Vτ π2 (π2 ∈ {B, D}) が成り立の場合について証明する．他も同様である．

つ．従って D(·) の引数の束縛時値が B あるいは

⋄

1

2

（x の場合） 証明木は Γ, x : τ π `1 x : τ π となる．

Γ, x : τ π に適合するような ρ に対しては ρ(x) ∈Vτ π が成り立つ．従って，S [[x]] ρ = ρ(x) ∈ Vτ π
（λS x. M の場合） 証明木の最後はD となっているので D(S [[M ]] ρ[x⋄ /x]) ∈ Code ．
よってbuild-λ(x⋄ , D(S [[M ]] ρ[x⋄ /x]))

Γ, x : τ1π1 `1 M : τ2π2
Γ `1 λ

S

∈

Code

=

V τ D → D τ π2
1

x. M : τ1π1 →S τ2π2

2

以上より
′

となる．ρ が Γ に適合しているとしよう．x ∈ Vτ π1

S [[λB x. M ]] ρ

1

なる全ての x′ に対して ρ[x′ /x] は Γ, x : τ1 1 に適π合するので，帰納法の仮定により S [[M ]] ρ[x′ /x] ∈Vτ π2 が成り立つ．従って，
2

S [[λ x. M ]] ρ
S

=

′

′

λx . S [[M ]] ρ[x /x]∈Vτ π1 → Vτ π2=

Vτ π1 →S τ π2
1(build-λ(x⋄ , D(S [[M ]] ρ[x⋄ /x])),λx′ . S [[M ]] ρ[x′ /x])∈(Vτ D →D τ π2 ) × (Vτ D →S τ π2 )=Vτ D →B τ π2

1

1

2

2

1

2

2

この定理より `1 M : τ D が導けるなら，必ずその特

2

1

=

化の結果は Vτ D = Code となり，エラーを起こすこと

2（λD x. M の場合） 証明木の最後はなく，部分評価の結果のコードを得られることがわかる．
系 1 `1 M : τ D が導けるなら S [[M ]] ρinit ∈ Vτ D

Γ, x : τ1D `1 M : τ2D
Γ `1 λD x. M : τ1D →D τ2D

証明： ρinit が空の型環境に適合しているため．
⋄となる．ρ が Γ に適合しているとしよう．x ∈ Vτ D
1なる全ての x⋄ に対して ρ[x⋄ /x] は Γ, x : τ1D に適

2

コンピュータソフトウェア

28

(220)

Γ `2 定数 : Intπ ; 定数πΓ, x : τ π `2 x : [τ ]π′{ π ≥ π′ }; x↓ππ′Γ, x : τ1π1 `2 L : τ2π2 ; MΓ `2 λx. L : τ1π1 →π τ2π2 ; λπ x. MΓ `2 L1 : τ2π2 →π τ1π1 ; M1

{π ▷′ π1 , π ▷ π2 }Γ `2 L2 : τ2π2 ; M2{′

Γ `2 L1 @L2 : [τ1 ]π1 ; (M1 @π M2 )↓ππ1′

π1 ≥ π1′ ,π ▷′ π2 ,π ∈ {S, D},π ▷ π1}1

Γ `2 L1 : τ1π1 ; M1

Γ `2 L2 : τ2π2 ; M2π1
π π2
Γ `2 cons L1 L2 : τ1 × τ2 ; cons π M1 M2{

Γ `2 L : τ1π1 ×π τ2π2 ; M′Γ `2 car L : [τ1 ]π1 ; (car π M )↓ππ1′{π ▷ π1 , π ▷ π2 }}π1 ≥ π1′ ,π ▷ π1 ,π ∈ {S, D},π ▷ π21

Γ `2 L1 : Intπ1 ; M1 Γ `2 L2 : Intπ2 ; M2
Γ `2 L1 + L2 : Intπ ; M1 +π M2
図9}{
π1 ▷ π, π2 ▷ π, π1 ▷ π2 , π2 ▷ π1 ,π1 ∈ {S, D}, π2 ∈ {S, D}

注釈の付いていない言語に対する型規則（制約生成規則）

十分なことは 8 節の補題 1 で見る．
）ここに出てくる

7 制約の生成π ≥ π ′ という制約は型の変換可能性を示すもので以下

図 6 の規則は注釈の付いた言語に対する型規則なののように定義される．
（S > D は成り立たないことにで，これを使って注釈の付いていないプログラムに注釈

注意．
）

を付けることはできない．注釈の付いていないプログラ

B > S,

B>D

ムに注釈を付けるためには，図 6 の型規則を注釈の付

π ≥ π ′ ⇐⇒ (π > π ′ ) ∨ (π = π ′ )

いていないプログラムに対するものに書き換える必要

束縛時解析終了時に π ≥ π ′ の制約の等号が成り立たずがある．この書き換えは（１）同じ命令に対する規則を

π > π ′ となったときには，π ′ に対応する項に注釈としまとめ，（２）B から S や D への型変換規則を他の規

′
π
て ↓B
π ′ が付く．逆に π = π の場合は M↓π ′ = M と解則に埋め込むこと，で行われる．書き換えた結果を図 9

釈する．

に示す．この規則を本稿では制約生成規則と呼ぶ．図中

制約生成規則は注釈の付いていない言語に対する規則

Γ `2 L : τ ; M は，型環境 Γ のもとで注釈の付いてとなっているが，各式を具体的にどういう束縛時値にすπいない式 L が型 τ

πを持ち，その結果，もとの式 L がれば良いかは明らかではない．束縛時解析は，まず制約

M という注釈の付いた式に変換されることを示す．ま

生成規則で束縛時値に関する制約を生成し，それを解く

た [τ ]π は，π = D のときは τ π 中に出てくる全ての束ことで行われる．

縛時値を D にしたもの，π 6= D のときは τ

π

そのもの

を表す．
図 9 の規則の中で四角で囲んである部分が型変換が起きる可能性のある場所である．
（型変換がこれだけで

例えば，項 P に対しては，従来通りの型推論を行って図 10 のような推論木を作ることができる．この推論
木の各推論を制約生成規則と照らしあわせると以下のような制約を得ることができる．

(221)

Vol. 17 No. 3 May 2000

29

′′

′
π4

Γ1 `2 f : π1 →π3

Γ1 `2 f : π1 →π4 π3 Γ1 `2 2 : π1
Γ1 `2 f @2 : π3′′

Γ1 `2 cons f (f @2) : (π1 →π4 π3 ) ×π5 π3′′`2 λf. cons f (f @2) : (π1 →π4 π3 ) →π6 (π1 →π4 π3 ) ×π5 π3′

Γ2 `2 x : π1′ Γ2 `2 3 : π2
Γ2 `2 x + 3 : π3`2 λx. x + 3 : π1 →π4 π3′′`2 (λf. cons f (f @2))@(λx. x + 3) : (π1 →π4 π3 ) ×π5 π3′図 10型推論の例（Γ1 = f : π1 →π4 π3 , Γ2 = x : π1 , Intπ を π と表記．; M の部分は省略）

有効性を保証するために用いられる．π = S のとき

π1 ≥ π1′ ,′π4 ▷ π1 ,π3 ≥ π3′ ,は，これらの制約は制約にはならないので λS x. M

π1′ ▷ π3 ,π4 ▷ π 3 ,π5 ▷ π4′ ,の規則が得られ，π = D のときは π1 = π2 = D

π2 ▷ π3 ,π4 ≥ π4′ ,π5 ▷ π3′ ,となって λD x. M の規則が得られ，π = B のとき

π1′ ▷ π2 ,π4 ≥ π4′′ ,π6 ▷′ π4 ,は π1 = D, π2 ∈ {B, D} となって λB x. M の規π2 ▷ π1′ ,

π4′′ ▷′ π1 ,π6 ▷ π5 ,則が得られる．

π1′ ∈ {S, D},

π4′′ ▷ π3 ,π5 ≥ π5′ ,π2 ∈ {S, D},

π4′′ ∈ {S, D},

π6 ∈ {S, D}（L1 @L2 の場合） π = S, D だった場合に，それぞれ M1 @S M2 , M1 @D M2 の規則を使えば良い．そのとき π ▷′ π2 , π ▷ π1 の 2 つの制約が型の有効性

この制約は（9 節以降で説明する方法を使って）π4′ = Dを保証するために用いられる．また，π1 > π1′ が成り立った場合には，直後に ↓B
π ′ の規則を使えば良という初期条件のもとで解くと

1π4′′ = π6 = S,

い．具体的には，

π4 = B,

π1 = π1′ = π2 = π3 = π3′ = π4′ = π5 = π5′ = Dという解が得られ，これよりΓ `2 L1 : τ2π2 →S τ1B ; M1

Γ `2 L2 : τ2π2 ; M2′
π1

Γ `2 L1 @L2 : τ1 ; (M1 @S M2 )↓B
π′

B
S D
S
B
D D
(λS f. cons D f↓B
D (f↓S @ 2 ))@ (λ x. x + 3 )という注釈が得られる．ここで π4 ≥ π4′ と π4 ≥ π4′′ の1をΓ `1 M1 : τ2π2 →S τ1B

2 つの制約の等号が成り立たなかったので，それに対応

Γ `1 M2 : τ2π2

Γ `1 M1 @S M2 : τ1B

B
する項に ↓B
D と ↓S が挿入されている．

′

π1
Γ `1 (M1 @S M2 )↓B
π ′ : [τ1 ]1

8 型チェック規則と制約生成規則の等価性
本節では，図 6 の規則（型チェック規則）と図 9 の規に変換すればよい．
（L1 + L2 の場合） π1 = π2 = S だった 場 合 に

M1 +S M2 の規則を，π1 = π2 = D だった場則（制約生成規則）の等価性を見ていく．
次の定理は，制約生成規則で得られる注釈は型チェッ

合に M1 +D M2 の規則を使えば良い．それ以外の

ク規則でも得ることができることを示している．

場合は，π1 ▷ π2 , π2 ▷ π1 の 2 つの制約によって除定理 2 Γ `2 L : τ

外されている．また，π1 ▷ π, π2 ▷ π の 2 つの制約

π

; M ならば Γ `1 M : τ ．
π

証明： 制約生成規則を使って得られた証明木が型チェッ
ク規則を使って得られる証明木に変換できることを示す．

によって π1 = π2 = D だったら π = D を保証している．

2

以下 λx. L, L1 @L2 , L1 + L2 の３つの規則についての補題 1 最も望ましい注釈の導出木において，型変換規変換を示す．他も同様である．

則は，x，M1 @π M2 ， car π M （または cdr π M ）に対（λx. L の場合） π = S, D, B だった場合に，それしてのみ使われ，定数 π ，λπ x. M ，cons π M1 M2 ，まぞれ λS x. M , λD x. M , λB x. M の規則を使えば良たは M1 +π M2 に対して使われることはない．

い．そのとき π ▷′ π1 , π ▷ π2 の 2 つの制約が型の

証 明：

λπ x. M の 場 合 に つ い て 証 明 す る ．
（定 数π ，

コンピュータソフトウェア

30
π

π

cons M1 M2 ，M1 + M2 の場合も同様に証明できる．
）
πλ x. M に対して型変換規則が使われる場合というのは，
B
B(λB x. M )↓B
D または (λ x. M )↓S のどちらかである．
D

(222)

う扱っても部分評価の結果には影響しないのだが，ここでは ⊥ とした†5 ．
このように束縛時値を解釈すると，最も望ましい注釈

いずれの場合も，型変換規則を使わずに λ x. M またはの定義は次のように言い換えることができる．

λS x. M とすれば，λ式の束縛時値が（他の束縛時値を

定義 5 同じプログラム p に対する有効な注釈 pann の変えることなく）B から D あるいは S になっている

うちで，以下の 2 つの性質を満たす注釈 p∗ann を最ものでより望ましい注釈となっている．従って，最も望ま

望ましい注釈と呼ぶ．

しい注釈においては，型変換規則がλ式に直接，使われ

1. p の全ての部分式について，その d の値が pann2において false なら， p∗ann においても false でることはない．

次の定理は，型チェック規則を使って得られる注釈で，ある．

それが最も望ましい注釈になっているならば，その注釈

2. pann と p∗ann の全ての部分式で d の値が同一のは制約生成規則でも得ることができることを示している．

場合には，s の値が pann において false なら，p∗ann

定理 3 Γ `1 M : τ π かつ M の注釈が最も望ましいにおいても false である．

ものであるならば Γ `2 |M | : τ

π

; M．

より直観的に述べれば，d の値はなるべく false の方が証明： 型チェック規則を使って得られた証明木が，最も良く，d の値で区別できないときは s の値がなるべく望ましい注釈に対するものであったなら，制約生成規則

false の方が良い，ということである．
定義 5 は s = d = false の場合の解釈を ⊥ ではなを使って得られる証明木に変換できることを示す．
型変換以外の規則については，対応する制約生成規則

く S とすれば，定義 3 と一致する．あえて ⊥ を使用

をそのまま使えば良い．問題になるのは，型変換規則がしているのは，部分評価の結果に影響を与えない部分に使われた場合である．補題 1 より，注釈が最も望まし

柔軟性を持たせることで後の制約解消をやりやすくする

いものであった場合，型変換の規則が使われるのは x，ためである．このためにある式の束縛時値が ⊥ になっ

π

π

π

M1 @ M2 ， car M （または cdr M ）のいずれかであてしまった場合は，特化時にその式を（void 値などの）′適当な定数と解釈すればよい．以下では，定義 5 を最る．これらに対応する制約生成規則にはいずれも π ≥ πの制約がついているので，型変換規則をあわせて制約生

2

成規則に対応させれば良い．

も望ましい注釈の定義として使用する．

(s, d) を使って，図 9 に出てくる π 上の制約を以下のように (s, d) 上の制約に変換する．
（以下では π = (s, d),

9 型のペアによる解釈

πi = (si , di ) とする．
）

本稿で行う制約の解消は，まず束縛時値 π を (s, d)π1 ▷ π 2 :′π1 ▷ π2 :d = trues = false⊥Ds = trueSB(d1 = true) ⇒ (d2 = true)∧(d1 = true) ⇒ (s2 = false)

S, D, B と (s, d) の関係は以下のように定義される．
d = false∧(s1 = false) ⇒ (s2 = false)という真偽値のペアで表現する．そして π 上の制約をこ
れらの変数の上の制約に変換し，そこで制約解消を行う．

(d1 = true) ⇒ (d2 = true)

π1 ≥ π2 :(d2 = true) ⇒ (d1 = true)∧(s1 = false) ⇒ (s2 = false)π ∈ {S, D} :(s = false) ⇒ (d = true)∧(d = true) ⇒ (s = false)s = true は静的に使われ得る，すなわち S あるいは B

いずれの制約も（型が ⊥ となる場合を除けば）もとのであることを示し，d = true は動的に使われ得る，すな

制約と同じ制約を表している．このことは (s, d) の真偽

わち D あるいは B であることを示す．s = d = falseの場合は，その値が静的に使われることもなければ最終結果にも残らないことを示す．この場合は，その値をど†5 例えば car (cons 1 2) の 2 など．束縛時値が ⊥ である
ような式は，特化時には任意の定数，例えば void 値に置
き換えることができる．

(223)

Vol. 17 No. 3 May 200031

値の全ての場合を確かめれば確認できる．ここで，上の第１段階で d だけではなく s も考慮に入れているの制約中には d = true と s = false しか出てきておらず，

は s の値が d の値に影響を及ぼすことがあるからであd = false や s = true は出てきていないことに注意しる．それは，具体的には（関数適用など）π ∈ {S, D}

よう．このことは制約解消アルゴリズムの正当性を見るの制約が現れるところである．関数適用は S か D のど上で重要な役割を果たす．以降の節ではこれらの制約をちらかでなくてはならないが，S とはなり得ない場合に′′(p = x) ⇒ (p = x ) のように表現する．ここで，p, p′′

は s または d であり，x, x は true または false である．

のみ D としたい．そこで，まず S または B （つまりs = true）という仮定からはじめ，S または B とはな
り得ない（s = false）ことがわかったときのみ D とす

10 制約の解消るのである．

プログラムが与えられたら前節までの方法に従って制

ここで「関数適用等は可能なら S としたい」という約を生成する．そして，そのプログラム自体の束縛時値

要求と「D としてしか使われていない値を不必要に B（トップレベルの束縛時値）を πtop = (stop , dtop ) とすにはしたくない」という要求は相容れないことに注意しれば dtop = true という制約を加えた上で制約解消をよう．前者は s をなるべく true にし，後者は s をなる行う．この dtop = true という制約は，このプログラム

べく false にする方向である．このため，本稿の制約解を部分評価した結果が全体としてコードになる，という消アルゴリズムは２段階に分かれている．2 つの要求のもので，初期条件のようなものである．

うちより重要な前者が第１段階で満たされ，後者の要求制約の解消は，より望ましい注釈の２条件にそって２は第２段階で満たされる．

段階で行う．どちらも，制約を書き換え規則と見なして第２段階では，第１段階で B となったもののうち，順次，解を更新していくことで制約解消を行う．アルゴ

実際に静的かつ動的に使われているものを特定する．

リズムを直観的に説明すると以下のようになる．

そのためにまず，第１段階で B （または D ）と判断し第１段階 まず（初期条件に使われる dtop を除く）

たものを全て D として，B としては使われていない

全ての d に false，全ての s に true を代入する．そ（s = false）と仮定する．そして，その中で S の計算を′行うために必要なものを B に戻している（s = true）．

′

して，制約 (p = x) ⇒ (p = x ) を「p = x が成り′′立っていたら p = x が成り立つように値を変更す

制約解消のアルゴリズムをより形式的に書くと以る」と解釈して適用し，これを変化がなくなるまで

下のようになる．ここで，Cinit は 7 節で生成され続ける．

た π 上の制約を 9 節で述べた方法で変換した s と第２段階 d の値は第１段階で確定したものを使用し，∗は Cinit 中の制約の対偶をとった
d 上の制約，Cinit

s の値は全て false として制約の適用を変化がなくものとする．
（(p1 = x1 ) ⇒ (p2 = x2 ) の 対 偶 は ，なるまで行う．この際，制約は全て対偶をとって解(p2 = ¬x2 ) ⇒ (p1 = ¬x1 ) で与えられる．
）また，プロ′′′

釈する．つまり (p = x) ⇒ (p = x ) を「p = x′が成り立っていなかったら p = x が成り立たない
ように値を変更する」と解釈する．
第１段階では s = true, d = false すなわち全ての値をまず S と仮定し，その中で d = true すなわち最終結果に残すため，そのコード表現が必要な部分を特定する．直観的には，全ての値が静的に使用可能（s = true）

グラム全体の束縛時値を (stop , dtop ) とする．
第１段階 初期制約集合 CI と初期解 θI を以下のように定義する．

CI = Cinit
θI = {dtop = true}∪ {d = false | 全ての d(6= dtop ) について }∪ {s = true | 全ての s について }と仮定しても，最終結果にコードとして残さざるを得

hCI , θI i に対して，以下の書き換え規則を適用できない部分を特定している．逆からとらえると，ここでなくなるまで適用する．

d = true と特定されなかった部分はコード表現が不要ということなので S とすることができる．

コンピュータソフトウェア

32h{(p = x) ⇒ (p′ = x′ )} ∪ C,
{p = x, p′ = x′′ } ∪ θi
→I hC, {p = x, p′ = x′ } ∪ θiすなわち，p = x が成り立っており，(p = x) ⇒(p′ = x′ ) という制約があったら，その制約を取り除き，p′ の値を更新する．最終的に得られた制約集
合と解を hC̃I , θ˜I i とする．
第２段階 初期制約集合 CII と初期解 θII を以下のように定義する．

CII

=

∗
Cinit

θII

=

{d = x | d = x ∈ θ˜I }∪{s = false | 全ての s について }hCII , θII i に対して第１段階と同じ書き換え規則を適用できなくなるまで適用する．
（第２段階の書き換
えは →II で表す．
）最終的に得られた制約集合と解を hC˜II , θ˜II i とする．
初期解と書き換え規則の作り方から θ には同じ p に(224)

π1′ ∈ {S, D} : s′1 = f ⇒ d′1 = t ∧ d′1 = t ⇒ s′1 = f
π2 ∈ {S, D} : s2 = f ⇒ d2 = t ∧ d2 = t ⇒ s2 = f
π4 ▷′ π1 : d4 = t ⇒ d1 = t ∧ d4 = t ⇒ s1 = f
π4 ▷ π3 : d4 = t ⇒ d3 = t ∧ s4 = f ⇒ s3 = f
π4 ≥ π4′ : d′4 = t ⇒ d4 = t ∧ s4 = f ⇒ s′4 = f
π4 ≥ π4′′ : d′′4 = t ⇒ d4 = t ∧ s4 = f ⇒ s′′4 = f
π4′′ ▷′ π1 : d′′4 = t ⇒ d1 = t ∧ d′′4 = t ⇒ s1 = fπ4′′ ▷ π3 : d′′4 = t ⇒ d3 = t ∧ s′′4 = f ⇒ s3 = fπ4′′ ∈ {S, D} :s′′4 = f ⇒ d′′4 = t ∧ d′′4 = t ⇒ s′′4 = f

π3 ≥ π3′ : d′3 = t ⇒ d3 = t ∧ s3 = f ⇒ s′3 = f
π5 ▷ π4′ : d5 = t ⇒ d′4 = t ∧ s5 = f ⇒ s′4 = f
π5 ▷ π3′ : d5 = t ⇒ d′3 = t ∧ s5 = f ⇒ s′3 = f
π6 ▷′ π4 : d6 = t ⇒ d4 = t ∧ d6 = t ⇒ s4 = f
π6 ▷ π5 : d6 = t ⇒ d5 = t ∧ s6 = f ⇒ s5 = f
π5 ≥ π5′ : d′5 = t ⇒ d5 = t ∧ s5 = f ⇒ s′5 = f
π6 ∈ {S, D} : s6 = f ⇒ d6 = t ∧ d6 = t ⇒ s6 = f

対して複数の p = x が含まれることはない．従って θ が

初期条件は d′5 = true である．それ以外の全ての d に求まれば，制約生成規則の ; M の部分から注釈を求め対して d = false，全ての s に対して s = true を代入

ることができる．

し，上の制約を使って d′5 = true を伝搬していくと，四以下 p = x が θ に含まれるとき θ(p) = x と書く．
′

また θ から p = x を取り除いて p = x を加えて得角で囲んだ制約が適用されて，以下のような結果を得る．

d1 = d′1 = d2 = d3 = d′3 = d4 = d′4= d5 = d′5 = trueられる解を θ[p 7→ x] と書く．書き換え規則を適用する時，どの制約を取り除いたかが重要となる場合には，d′′4 = d6 = falsec : (p = x) ⇒ (p′ = x′ ) のように制約に名前を付けた

s4 = s′4 = s′′4 = s5 = s′5 = s6 = true

c

′

′

上で，hC, θi −→I hC , θ i のように書く．

s1 = s′1 = s2 = s3 = s′3 = false
これを π 上の制約に戻すと11 制約解消の例

π4′′ = π6 = S,

π4 = π4′ = π5 = π5′ = B,

7 節で得られた項 P に対する制約を例にとって制約解

π1 = π1′ = π2 = π3 = π3′ = D

消を実際にやってみよう．まず π に関する制約を (s, d)となり，これは以下のような注釈を得たことに相当する．

に関する制約に変換すると以下のようになる．ここではtrue を t，false を f と書いている．
π1 ≥ π1′ : d′1 = t ⇒ d1 = t ∧ s1 = f ⇒ s′1 = f
π1′ ▷ π3 : d′1 = t ⇒ d3 = t ∧ s′1 = f ⇒ s3 = f
π2 ▷ π3 : d2 = t ⇒ d3 = t ∧ s2 = f ⇒ s3 = f
π1′ ▷ π2 : d′1 = t ⇒ d2 = t ∧ s′1 = f ⇒ s2 = f
π2 ▷ π1′ : d2 = t ⇒ d′1 = t ∧ s2 = f ⇒ s′1 = f

S D
B B
B
(λB f. (cons B f↓B
D (f↓S @ 2 ))↓D )↓S@S (λB x. x +D 3D )第１段階は d = true すなわち D あるいは B となる部分を特定するが，逆に見るとこれは S となる部分を特定していることになる．上の結果を見ると，きちんと全体の関数適用と f の適用は静的とされていることがわかる．しかし，最初のλ式と cons 文については無駄に静的かつ動的とされていることがわかる．この無駄な部分は第２段階で取り除かれる．第２段階は s の値を

(225)

Vol. 17 No. 3 May 2000

33

false に戻した以下の状態から始める．
d1 = d′1 = d2 = d3 = d′3 = d4 = d′4= d5 = d′5 =d′′4 = d6 =π4′′ = π6 = S,

true

π4 = B,

π1 = π1′ = π2 = π3 = π3′ = π4′ = π5 = π5′ = Dとなり，これで以下の最も望ましい注釈を得る．

false

s4 = s′4 = s′′4 = s5 = s′5 = s6 =

B
S D
S
B
D D
(λS f. cons D f↓B
D (f↓S @ 2 ))@ (λ x. x + 3 )false

s1 = s′1 = s2 = s3 = s′3 = false
また，適用する制約は全て対偶が取られて以下のように12 アルゴリズムの正当性なる．

こ こでは前節のアルゴリズムが実際，期待通り動π1 ≥ π1′ : d1 = f ⇒ d′1 = f ∧ s′1 = t ⇒ s1 = t
π1′ ▷ π3 : d3 = f ⇒ d′1 = f ∧ s3 = t ⇒ s′1 = t
π2 ▷ π3 : d3 = f ⇒ d2 = f ∧ s3 = t ⇒ s2 = t
π1′ ▷ π2 : d2 = f ⇒ d′1 = f ∧ s2 = t ⇒ s′1 = t
π2 ▷ π1′ : d′1 = f ⇒ d2 = f ∧ s′1 = t ⇒ s2 = t
π1′ ∈ {S, D} : d′1 = f ⇒ s′1 = t ∧ s′1 = t ⇒ d′1 = f
π2 ∈ {S, D} : d2 = f ⇒ s2 = t ∧ s2 = t ⇒ d2 = f
π4 ▷′ π1 : d1 = f ⇒ d4 = f ∧ s1 = t ⇒ d4 = f
π4 ▷ π3 : d3 = f ⇒ d4 = f ∧ s3 = t ⇒ s4 = t
π4 ≥ π4′ : d4 = f ⇒ d′4 = f ∧ s′4 = t ⇒ s4 = t
π4 ≥ π4′′ : d4 = f ⇒ d′′4 = f ∧ s′′4 = t ⇒ s4 = tπ4′′ ▷′ π1 : d1 = f ⇒ d′′4 = f ∧ s1 = t ⇒ d′′4 = f
π4′′ ▷ π3 : d3 = f ⇒ d′′4 = f ∧ s3 = t ⇒ s′′4 = tπ4′′ ∈ {S, D} : d′′4 = f ⇒ s′′4 = t ∧ s′′4 = t ⇒ d′′4 = f
π3 ≥ π3′ : d3 = f ⇒ d′3 = f ∧ s′3 = t ⇒ s3 = t
π5 ▷ π4′ : d′4 = f ⇒ d5 = f ∧ s′4 = t ⇒ s5 = tπ5 ▷ π3′ : d′3 = f ⇒ d5 = f ∧ s′3 = t ⇒ s5 = tπ6 ▷′ π4 : d4 = f ⇒ d6 = f ∧ s4 = t ⇒ d6 = f
π6 ▷ π5 : d5 = f ⇒ d6 = f ∧ s5 = t ⇒ s6 = t
π5 ≥ π5′ : d5 = f ⇒ d′5 = f ∧ s′5 = t ⇒ s5 = tπ6 ∈ {S, D} : d6 = f ⇒ s6 = t ∧ s6 = t ⇒ d6 = f

くことを見ていく．以下では真偽値の間の大小関係をtrue > false とする．
第１段階では，解 θ に対して θ ≤I θ ′ ⇐⇒ ∀s.θ(s) ≥def

θ′ (s) ∧ ∀d.θ(d) ≤ θ′ (d) という大小関係を考える．すると解 θ は，この大小関係のもとで束となる．次の補題
は，第１段階の制約の適用はこの束のもとで解が減少しないことを示している．
補題 2 hC, θi →I hC ′ , θ ′ i なら θ ≤I θ ′ ．
証明： θ = θ ′ なら補題は満たされている．θ 6= θ ′ としよう．θ 6= θ ′ となるのは，ある s について θ(s) = trueかつ θ ′ (s) = false となっているか，ある d について

θ(d) = false かつ θ′ (d) = true となっているかのど
ちらかである．これは制約 (p = x) ⇒ (p′ = x′ ) の

p′ = x′ の部分には s = false あるいは d = true という形しか現れていないためである．どちらの場合も

θ ≤I θ′ となっているので補題が満たされている． 2
補題 3 第１段階終了時の解 θ˜I は Cinit 中の制約を全て満たしている．
証明： Cinit 中の制約 (p = x) ⇒ (p′ = x′ ) は，第１段階終了時の制約集合 C̃I に含まれているものとそうでないものに分けられる．前者は θ˜I において制約の前提条件である p = x が満たされなかった，ということをこれに対して d′′
4 = d6 = false を伝搬させていくと，示しているので，この制約は自明に満たされている．後上の四角で囲んだ制約が適用されて以下の結果を得る．

者の場合は，制約適用の過程で

d1 = d′1 = d2 = d3 = d′3 = d4 = d′4h{(p = x) ⇒ (p′ = x′ )} ∪ C,

= d5 = d′5 = true

{p = x, p′ = x′′ } ∪ θid′′4 = d6 = false→I hC, {p = x, p′ = x′ } ∪ θiのような書き換えが行われ，制約 (p = x) ⇒ (p′ = x′ )s4 = s′′4 = s6 = trues1 = s′1 = s2 = s3 = s′3 = s′4 = s5 = s′5 =falseが取り除かれるとともに，解が p′ = x′ のように更d の値は第１段階終了時から変化していないことに注意

新 さ れ た ，と い う こ と を 示 し て い る ．こ こ で ，制 約

しよう．上の結果を π 上の制約に戻すと(p = x) ⇒ (p′ = x′ ) の p′ = x′ の部分には s = false
あるいは d = true という形しか現れていないことにコンピュータソフトウェア

34

(226)

注意しよう．従って，ここで解は s = false あるいはしである．

d = true という形に書き換えられている．第１段階中

補題 5 hC, θi →∗I hC̃I , θ˜I i かつ hC, θi →∗I hC̃I′ , θ˜I′ i な

これらは，補題 2 により s = true あるいは d = false

らば hC̃I , θ˜I i = hC̃I′ , θ˜I′ i ．

→I の適用回数に関する帰納法で証明する．

となることはない．これより，第１段階終了時にも制約証明：(p = x) ⇒ (p′ = x′ ) の p′ = x′ が成り立っている，す一 度 も 適 用 し な い 場 合 は ，hC, θi = hC̃I , θ˜I i か つ2

なわちこの制約が満たされていることがわかる．

hC, θi = hC̃I′ , θ˜I′ i なので成り立つ．

次の補題は，2 つの制約を適用できるときには，それ複数回，適用する場合を考える．hC, θi →∗I hC̃I , θ˜I i でらをどのような順番で適用しても結果は変わらないこと

最初に適用する制約を c : (p = x) ⇒ (p′ = x′ ) としよを示している．

う．hC, θi においてこの制約が適用可能なので θ(p) = xc1c2である．ここで p = x は d = true あるいは s = falsec2のどちらかの形であり，かつ C 中の他の制約の結論部分

補題 4 hC0 , θ0 i −→I hC1 , θ1 i か つ hC0 , θ0 i −→I

hC2 , θ2 i なら，ある hC3 , θ3 i が存在して hC1 , θ1 i −→I
c1

hC3 , θ3 i かつ hC2 , θ2 i −→I hC3 , θ3 i．

も d = true あるいは s = false という形なので，θ で成

証明： c1 , c2 をそれぞれ (p1 = x1 ) ⇒ (p2 = x2 ), (p3 =り立っている p = x という関係は，その後の制約の適用

x3 ) ⇒ (p4 = x4 ) とおく．hC0 , θ0 i からは c1 も c2 もで満たされなくなることはない．従って，hC, θi から始適用可能なので θ0 (p1 ) = x1 かつ θ0 (p3 ) = x3 が成りまる全ての書き換えにおいてずっと p = x が成り立って立っている．

いる．これより hC, θi →∗I hC̃I′ , θ˜I′ i においても，制約 cc1

まず c1 を先に適用する場合を考えよう．hC0 , θ0 i −→I

はいつでも適用可能で，かつ必ずどこかで適用されている

hC1 , θ1 i よ り θ1 = θ0 [p2 7→ x2 ] で あ る ．こ こ でことがわかる．どこで適用されていても，補題 4 を複数

p2 6= p3 なら θ1 (p3 ) = θ0 (p3 ) = x3 なので hC1 , θ1 i

回使用することで，hC, θi →I hC1 , θ1 i →∗I hC̃I′ , θ˜I′ i のcに c2 を適用することができ，θ3 = θ1 [p4 7→ x4 ] =ように最終状態を変えることなく c を最初に適用するよθ0 [p2 7→ x2 ][p4 7→ x4 ] となる．また，p2 = p3 の場

うにすることができる．hC, θi →I hC1 , θ1 i →∗I hC̃I , θ˜I i

合は（制約に出てくる pi = xi は d = true あるいであったので，hC1 , θ1 i に対して帰納法の仮定を使うこは s = false のどちらかの形なので）x2 = x3 となり，とができ hC̃I , θ˜I i = hC̃I′ , θ˜I′ i が言える．

c2

θ1 (p3 ) = θ1 (p2 ) = x2 = x3 から，やはり c2 を適用

このアルゴリズム（の第１段階）は，解として全てのすることができ，同じ θ3 = θ0 [p2 7→ x2 ][p4 7→ x4 ] を

s が false，d が true の場合を考えると，自明に全ての得る．

制約を満たしているので，解は存在する．第１段階のア

全 く 同 様 に し て c2 を 先 に 適 用 す る 場 合 を 考 え る

ルゴリズムは，最小の解から必要なもののみについて単と，c1 も続いて適用できることがわかり，その結果

調に解を更新することで制約を満たしているので，いずθ3′ = θ2 [p2 7→ x2 ] = θ0 [p4 7→ x4 ][p2 7→ x2 ] を得る．

れ最小の解に到達する．従って，結果は期待通り制約を

p2 =6 p4 の場合は，θ3′= θ0 [p4 7→ x4 ][p2 7→ x2 ] =満たすもののうちで d が false となっているものが最θ0 [p2 7→ x2 ][p4 7→ x4 ] = θ3 ．また，p2 = p4 の場も多いものとなっていることがわかり，次の定理が導か合は（制約に出てくる pi = xi は d = true あるいれる．

は s = false のどちらかの形なので）x2 = x4 とな定理 4 第１段階終了時の解 θ˜I から得られる注釈は，

り，θ3′ = θ0 [p4 7→ x4 ][p2 7→ x2 ] = θ0 [p2 7→ x2 ] =定義 5 の最も望ましい注釈の条件のうち，最初の条件

θ0 [p2 7→ x2 ][p4 7→ x4 ] = θ3 となる．

を満たしたものとなっている．

ま た ，C3 に つ い て は ，ど ち ら の 経 路 を 通って も次に第２段階である．今度は s = true，d は第１段

C0 \ {c1 , c2 } となるので等しい．以上により証明さ階で得られたものに設定して制約（の対偶）を適用する．

2

次の補題は，第２段階では d はもはや変化しないことをれた．

次の補題は，第１段階で得られる解は一意的であるこ∗とを示している．ここで → は → の０回以上の繰り返示す．
補題 6 全ての d について θII (d) = θ˜II (d)．

(227)

Vol. 17 No. 3 May 2000

35′

証明： 書き換えの長さに関する帰納法で，第２段階中

下を参照）．従って θ = θ[dn 7→ false] = θ となり

全ての θ について θ(d) = θII (d) であることを証明する．
書き換えがなかった場合には θII (d) = θ˜II (d) なので成り(s = true) ⇒ (d = false) の形の場合も証明できた．
θ(dn ) = false であることは，第１段階終了時の解 θ˜I∗立つ．今，書き換えが hCinit, θII i から hC, θi まで進んが全ての制約を満たしている（補題 3 ）ことからわかる．

だところで補題が成り立っている，すなわち，全ての d仮に θ(dn ) = true であったとしよう．帰納法の仮定よりについて θ(d) = θII (d) である，としよう．このとき，そθ˜I (dn ) = θII (dn ) = θ(dn ) = true である．上で適用し′た制約の対偶を考えると (dn = true) ⇒ (sn = false),ても θ (d) = θ(d) = θII (d) であることを示す．

(si = false) ⇒ (si−1 = false) (n ≥ i ≥ 1),c′の θ からもう一度，書き換え hC, θi → hC , θ i を行っ′

第２段階で使われる制約 (p1 = x1 ) ⇒ (p2 = x2 )は，第１段階の制約の対偶となっているので pi = xi(s0 = false) ⇒ (d0 = true) となり，これらは第１段階終了時にはみな満たされていたので，θ˜I (d0 ) = trueの部分は s = true または d = false のどちらかの形であったはずだが，これは上で θ˜I (d0 ) = θII (d0 ) = false′

で あ る ．こ の う ち ，制 約 の 適 用 の 結 果 θ(d) 6= θ (d)2と仮定したことに矛盾する．

と な り 得 る の は ，制 約 の 結 論 部 分 が d = false のこれにより，第２段階では s についてのみ考えれば良形，すなわち (d1 = false) ⇒ (d2 = false) またはい．これは「第２段階では無駄な B を D にする」とい(s = true) ⇒ (d = false) のどちらかの形である．そう直観にも合致している†6 ．

れぞれについて考えてみよう．

第２段階では，解 θ に対して θ ≤II θ ′ ⇐⇒ ∀s.θ(s) ≤def

第１段階終了時の解 θ˜I は Cinit 中の全ての制約をθ′ (s) ∧ ∀d.θ(d) = θ′ (d) という大小関係を考える．s に∗中の制約満たしているので，その対偶をとった Cinit

関する大小関係が第１段階とは逆になっていることに注も全て満たしている．d の値については θ˜I (d) = θII (d)意しよう．また，第２段階では制約の対偶をとるので，であり，かつ帰納法の仮定から θ(d) = θII (d) なので制約の p = x の部分に現れるのは s = true あるいは

θ は (d1 = false) ⇒ (d2 = false) の形の制約についd = false という形である．これらのことに注意すれば，ては全て満たしている．すなわち θ(d1 ) = true であ以下の４つの補題は第１段階と全く同じようにして証明るか θ(d1 ) = false かつ θ(d2 ) = false である．前者

することができる．

の場合はこの制約が適用不可能であり，後者の場合は補題 7 hC, θi →II hC ′ , θ ′ i なら θ ≤II θ ′ ．
（第２段階の適用により θ ′ = θ[d2 7→ false] = θ である．従って

制約の適用で解は減少しない．
）(d1 = false) ⇒ (d2 = false) の場合は証明された．

∗
中の制約を全補題 8 第２段階終了時の解 θ˜II は Cinit(s = true) ⇒ (d = false) の場合を考えよう．このて満たしている．
（従って Cinit 中の制約も全て満たして制約が適用されるためには θ(s) = true でなければないる．
）

らないが，第２段階の開始時の解 θII では全ての s は

補題 9 hC0 , θ0 i −→II hC1 , θ1 i か つ hC0 , θ0 i −→IIfalse である．θ(s) が true となるのは，ある d につい2hC2 , θ2 i なら，ある hC3 , θ3 i が存在して hC1 , θ1 i −→IIて θ(d) = false のもとで (d = false) ⇒ (s = true) の1
hC3 , θ3 i かつ hC2 , θ2 i −→（制約の適用順に
II hC3 , θ3 i．

形の制約を適用した場合と，その後 (s = true) ⇒ (s′ =よって結果は変わらない．
）

true) の形の制約を適用した場合のみである．今，第２補題 10 hC, θi →∗II hC˜II , θ˜II i かつ hC, θi →∗II hC˜I′I , θ˜I′I i

段階開始時において θII (d0 ) = false が成り立っているとならば hC˜II , θ˜II i = hC˜I′I , θ˜I′I i ．
（第２段階で得られる解は仮定しよう．そのもとで (d0 = false) ⇒ (s0 = true),

一意的である．
）

c1

c2
c

c

(si−1 = true) ⇒ (si = true) (1 ≤ i ≤ n) という∗第１段階の結果である θ˜II を持ってくれば，Cinit
中順番で制約を適用して θ(sn ) = true となり，ここでの制約は全て満たされているので，解は存在する．s に(sn = true) ⇒ (dn = false) を適用したとしよう．

ついて最小の解から始めて，必要なもののみについて単すると実はすでに θ(dn ) = false であり，制約を適用しても dn の値は変化しないことが証明できる（以†6 加えて，無駄な S を ⊥ にもしている．

36

コンピュータソフトウェア(228)

調に解を更新することで制約を満たしているので，いず

２段階で制約を解消しているのに相当している．本研究

れ最小の解に到達する．d の値は第１段階で得られるもでは，彼らの仕事を型システムとして定式化するととものと同じなので，第２段階の結果は期待通り，制約を満に，高階関数についても制限付きながら同様のことが行たすもののうちで d が false となっているものが最もえることを示した．

多く，その中で s が false となっているものが最も多い

本稿で示した型システムとその制約解消系は，Hen-ものとなっていることがわかる．よって次の定理が導か

glein [9] の作成した従来の束縛時解析を静的かつ動的なれる．

束縛時を許すように拡張したものと見ることができる．

定理 5 第２段階終了時の解 θ˜II から得られる注釈は，

静的かつ動的な値が入ったことで制約解消は２段階に

定義 5 の最も望ましい注釈の条件を満たしたものとなったが，制約解消の計算量は従来のものと同じくほぼなっている．

線形で行うことができる．

Sperber [13] は，静的，動的，そして未知，という３13 計算量つの束縛時を扱う部分評価器を作成している．これは，ここでは，アルゴリズムがプログラムの長さに対して

静的，動的以外の値を扱う，という点では本研究と類似

ほぼ線形時間であることを見ていく．まず，生成される制しているが，内容的には異なっている．Sperber の部分

約の数は各命令に対して定数なので，全体としてプログラ

評価器は，条件分岐のそれぞれの束縛時が異なるときに，ムの長さに対して線形である．しかし，制約を生成する過

その条件文の束縛時を動的とはせずに未知としておき，

程で変数の単一化が起きるため，そのときに union/ﬁnd

online にその束縛時を判断する，というもので，「静的

アルゴリズム [15] が必要となる．union/ﬁnd アルゴリ

または動的」な式を online の手法で扱おうというもの

ズムの計算量は，union/ﬁnd が適用される回数を m，である．

union/ﬁnd の対象となる変数の数を n，アッカーマン「静的かつ動的」な式を扱う部分評価器は，筆者が [1]関数の逆関数を α とすると O(mα(m, n)) である [15]．

において発表している．本稿では，そのうちコアとなるプログラムの大きさを N とすると，m も n も N で押部分について正当性の証明を行った．本稿の仕事をよりえられるので，union/ﬁnd アルゴリズムに必要な計算発展させたものとして，住井ら [14] による束縛時解析

量は全体で O(N α(N, N )) であるが，実際的なプログがあげられる．彼らは，本稿の枠組と Sperber の枠組

ラムに対しては α(N, N ) は 4 以下であることがわかっを統合する形でより一般的な束縛時解析手法を提案してている [15] ので，ほぼ線形と言うことができる．

いる．

第１段階は，初期条件の dtop = true から始めて，以
後 d = true あるいは s = false を順に伝搬していくこ

15 おわりにとで線形時間で終了する．これは，各制約が一度適用さ本稿では，関数型言語の部分評価器で構造データの扱れたらその後はずっと満たされ続けるため，高々制約のいを向上すべく，静的かつ動的な値を許すような束縛時数しか適用する必要がないためである．第２段階も同様解析を提案した．静的かつ動的な値を使うと，静的に構で，d = false であるもの全てについて s の値を true

造データにアクセスしつつ，その構造データをコードとにするか調べ，それを伝搬していくことで，線形時間でして最終結果に残すことができるようになる．この方法終了する．

は実質的に，従来許されていなかった構造データの liftを許すようにした，と見ることもできる．本稿で提案し14 関連研究

た束縛時解析は，型システムとして定式化され，型推論

本研究は，Hornof [11] らが C で行った束縛時解析との際に生成される束縛時に関する制約を解くことで結果密接な関係がある．彼らは，抽象解釈に基づいて構造を得る．さらに，型システムの正当性を示すとともに，データの使用と定義を前向き解析と後向き解析を使って制約の解消が従来の効率的な束縛時解析と同じくほぼ線求めている．これは，ちょうど本稿で s と d を使って

形時間でできることを示した．これに基づいて処理系を

(229)

Vol. 17 No. 3 May 2000

作成中であり，現在ほぼ動くに至っている．
ここで示した枠組には「静的かつ動的な関数の引数は動的」という強い制限がある．現在，この制限を取り除くべく，本稿の仕事と多相束縛時解析 [10] [5] との関係を調査中である．また，本稿ではベースとなる言語は

simply typed であると仮定したが，そこに多相性を導入するとどうなるか，というのも興味深い．その他には，
実際に大きなプログラムを使った部分評価の実験と評価，枠組の多段の部分評価 [8] への拡張などが今後の課題としてあげられる．

謝辞
日頃より本研究について多くのコメントを頂いている
増原英彦氏，およびいろいろなコメントを頂いた査読者の方々に感謝いたします．

参考文献[ 1 ] Asai, K.：Binding-Time Analysis for Both Staticand Dynamic Expressions，SAS’99，Static Analysis(LNCS 1694)，1999，pp. 117–133．
[ 2 ] Ashley, J. M. and Consel, C.：Fixpoint Computation for Polyvariant Static Analyses of Higher-OrderApplicative Programs，ACM Transactions on Programming Languages and Systems，Vol. 16，No. 5(1994)，pp. 1431–1448．
[ 3 ] Bondorf, A.：Similix 5.0 Manual，DIKU，University of Copenhagen，1993．
[ 4 ] Dean, J., Chambers, C. and Grove, D.：Identifying Proﬁtable Specialization in Object-Oriented
Languages，ACM SIGPLAN Workshop on Partial
Evaluation and Semantics-Based Program Manipulation (PEPM ’94)，1994，pp. 85–96．
[ 5 ] Dussart, D., Henglein, F. and Mossin, C.：37

Polymorphic Recursion and Subtype Qualiﬁcations:
Polymorphic Binding-Time Analysis in Polynomial
Time，SAS’95，Static Analysis (LNCS 983)，1995，
pp. 118–135．
[ 6 ] 藤波順久：オブジェクト指向言語を利用した自動的かつ効率的な実行時コード生成，コンピュータソフトウェア，
Vol. 15，No. 5 (1998)，pp. 25–37．
[ 7 ] Futamura, Y.：Partial evaluation of computation
process – an approach to a compiler-compiler，Systems，Computers，Controls，Vol. 2，No. 5 (1971)，
pp. 45–50．
[ 8 ] Glück, R. and Jørgensen, J.：An Automatic Program Generator for Multi-Level Specialization，Lisp
and Symbolic Computation，Vol. 10，No. 2 (1997)，
pp. 113–158．
[ 9 ] Henglein, F.：Eﬃcient Type Inference for HigherOrder Binding-Time Analysis，Functional Program-ming Languages and Computer Architecture (LNCS
523)，1991，pp. 448–472．
[10] Henglein, F. and Mossin, C.：Polymorphic
Binding-Time Analysis，ESOP’94，5th European
Symposium on Programming (LNCS 788)，1994，pp. 287–301．
[11] Hornof, L., Consel, C. and Noyé, J.：Eﬀective
Specialization of Realistic Programs via Use Sensitivity，SAS’97，Static Analysis (LNCS 1302)，1997，
pp. 63–73．
[12] Jones, N. D., Gomard, C. K. and Sestoft, P.：
Partial Evaluation and Automatic Program Generation，Prentice-Hall，New York，1993．
[13] Sperber, M.：Self-Applicable Online Partial Evaluation，Partial Evaluation (LNCS 1110)，1996，
pp. 465–480．
[14] Sumii, E. and Kobayashi, N.：Online-and-Oﬄine
Partial Evaluation: A Mixed Approach，ACM
SIGPLAN Workshop on Partial Evaluation and
Semantics-Based Program Manipulation (PEPM’00)，2000，pp. 12–21．
[15] Tarjan, R.：Data Structures and Network Flow
Algorithms，Regional Conference Series in Applied
Mathematics，Vol. CMBS 44 (1983)，SIAM．