限定継続のための TDPE に向けて
対馬 かなえお茶の水女子大学
tsushima.kanae@is.ocha.ac.jp

Abstract

浅井 健一
お茶の水女子大学
asai@is.ocha.ac.jp

限定継続のための命令としては control/prompt、

shift/reset など様々なコントロールオペレータがあるが、本研究では shift/reset [6] を用いた。

TDPE (Type-directed partial evaluation) は部
分評価の一種であり、プログラムとその型を用いる

その理由として、shift/reset は CPS と密接なことによって、プログラム内部の構造に触れずに部関係があり、明確な意味論を持っているため、非分評価を進めることが出来る。そのため、他の部分

決定性プログラミング [6] 、部分評価における let-

評価器と比較して高速である。

insertion [12] 、typed printf の記述 [2] など多くの本研究は TDPE の対象言語に限定継続の一種研究に使われているからである。

である shift/reset を導入し、その正当性を証明

以前の論文 [13] では、従来の λ 計算のためのすることを目的にしている。
まず、shift/reset と CPS 変換の関係性に着目

TDPE を限定継続の命令 shift/reset を使えるように拡張し、TDPE の表現力を広げることを目して、CPS 変換後の型を持つプログラムが TDPE的とした。概要としては、CPS の型を持つ項が従でどのように部分評価されるかを観察し、それを直来の call-by-value の TDPE でどのように扱われ接形式に戻すことで shift/reset を含む TDPE

るのかを観察し、それを直接形式に戻すことによっを導いた。また、shift/reset の影響を受けないて、限定継続のための TDPE を求めた。

部分については従来の TDPE と同じように部分評

本論文では、その論文で求めた限定継続のため価されるようにした。

の TDPE を改良し、shift/reset の影響を受け

次に call-by-name の TDPE の正当性を示し、ない部分については従来の TDPE と同じように部

今後の他の TDPE の証明への展望を示す。

分評価されるようにした。また、この限定継続のための TDPE の正当性への足掛かりとなる、call-1

by-name の TDPE の正当性を証明し、その後の展

導入

望を示す。
次の節では shift/reset について簡単に説明

Type-directed partial evaluation (TDPE) はする。3 節で Danvy の TDPE を、4 節で call-by-

Danvy によって提案された Normalization by evaluation の一例である [4]。TDPE に入力として項

value の TDPE を振り返った後、5 節で以前の論文からの shift/reset のための TDPE を改良しを与えると、その項に η-expanding を施し、結果たものを説明する。6 節で call-by-name の TDPE

として正規形へ部分評価された項を出力する。

の正当性を証明してその先の証明についての展望

他の部分評価と比べた特徴として、TDPE は入を示し、7 節で結論を述べる。

力された項を直接実行するので、項の構造に触れることなく部分評価を行うことが出来る。そのた2

shift/reset

め、他の部分評価に比べて高速であり、速さという点で魅力的なプログラム最適化の一つである。

shift/reset は限定継続を扱うための命令であ

他方で、コントロールオペレータは CPS 変換なる。shift は Scheme の call/cc のように現在のしに継続を扱うことが出来る便利なツールである。

継続を切り取るが、reset に囲まれた一部分の継続

1

のみを切り取るため、 範囲が限定されない Schemet ∈ Type ::= b | t1 → t2 | t1 × t2
v ∈ Value ::= c | x | λx.v | v0 @ v1 |の call/cc とは異なる。
具体的には、(shift k M) は現在の継続を切り

pair(v1 , v2 ) | f st v | snd v
e ∈ Expr ::= c | x | λx.e | e0 @ e1

取って、それを k に束縛し、M を空の継続で実行する。(reset M) は M を空の継続で実行する。

reify

=
:

pair(e1 , e2 ) | f st e | snd e
λt.λv : t.↓t v
Type → Value → TLT↓b v↓t1 →t2 v==v
λx¦1 . ↓t2 (v @ ↑t1 x¦1 )↓t1 ×t2 v=pair(↓t1 f st v, ↓t2 snd v)

reﬂect=λt.λe : t.↑t e

切り取られた継続 k は (k (k 3)) のように shift

↑b e

:
=

Type → Expr → TLT
e

式の中で二度使われている。reset の本体の式が↑t1 →t2 e↑t1 ×t2 e==

λv1 . ↑t2 (e @ ↓t1 v1 )pair(↑t1 f st e, ↑t2 snd e)

residualize=:

statically-reduce ◦ reify
Type → Value → Expr

例えば、次の式を考えてみる。

(+ 1 (reset (+ 2 (shift k (k (k 3)))))); (+ 1 (reset (+ 2 (+ 2 3)))); (+ 1 (reset 7)); (+ 1 7);8
一行目で切り取られる継続は、shift 式が reset
で囲まれているため (+ 2 []) である。この式では実行されて value になったとき、reset 式は本体の式の value へ評価される。よって、(reset 7) は7 になる。
正確な shift/reset の意味論については CPS変換を使うことで定義されている。[6]図 1. Danvy の λ 計算のための Type-

Directed Partial Evaluation[4]λ 計算の TDPE

3

部分評価 [10] とはプログラムの実行時間短縮のは Scheme のような datatype constructors を持つ

ために、与えられたプログラムの static な部分を

call-by-value の言語で表現されていると仮定している。
型は基本型 (b)、関数型 (t1 → t2 )、積の型 (t1 ×あらかじめ出来るだけ実行しておくプログラム最適化の一種である。

Type-directed partial evaluation (TDPE) は部

t2 ) の三種である。オーバーラインは static であることを意味し、TDPE のコンテキストでは中身

分評価の一種であるが、通常の部分評価とは二つの点で異なる。まず、TDPE は式の型の構造に着を調べていない compiled representation を意味す

目した部分評価である。なので、TDPE は実行する。逆にアンダーラインは dynamic であることをる時に式だけでなく、その式の型も必要とする。次意味し、datatype constructors で表された式を意に、TDPE は式の構造を操作することなく、代わ味する。TLT は Expr と Value の 2 レベルの項をりに受け取ったプログラムを実際に実行すること持つ。上付き文字 ¦ がついた変数は、新しく作らによって結果を求める。よって、TDPE が部分評れた変数であることを意味している。

価を実行するためにかかる時間は普通のインタプ
リタが基になっている部分評価に比べて短い。これ

3.2

Reify と Reflect

はコンパイルされたプログラムの方がインタプリ
タで実行するより速いのと似たような理由である。

3.1

TDPE は reify と reﬂect の二つの関数によって行われる。下向き矢印 (↓t ) は reify と呼ばれ、型 t を使うことで、compiled representation を構文

datatype に変換する。例えば、compiled representation f が関数型 b → b を持つとする。型が b → b

図 1 は、Danvy の Type-directed partial eval-uation であり、これは λ 計算を定数とペアで拡なので、 f はある M に対して λx1 .M という形張したものを対象としている。また、この TDPEを持っていることが分かる。その本体 M を求める

2

↓t1 →((t1 →t2 )→t2 ) (λx.λf.(f @((λa.a)@x)))= λx1 . ↓(t1 →t2 )→t2 ((λx.λf.(f @((λa.a)@x)))@(↑t1 x1 ))= λx1 . ↓(t1 →t2 )→t2 ((λx.λf.(f @((λa.a)@x)))@x1 )= λx1 .λx2 . ↓t2 (((λx.λf.(f @((λa.a)@x)))@x1 )@(↑t1 →t2 x2 ))= λx1 .λx2 . ↓t2 ((λx.λf.(f @((λa.a)@x)))@x1 )@(λv1 . ↑t2 (x2 @(↓t1 v1 )))= λx1 .λx2 . ↓t2 ((λx.λf.(f @((λa.a)@x)))@x1 )@(λv1 . ↑t2 (x2 @v1 ))= λx1 .λx2 . ↓t2 ((λx.λf.(f @((λa.a)@x)))@x1 )@(λv1 .(x2 @v1 ))= λx1 .λx2 .((λx.λf.(f @((λa.a)@x)))@x1 )@(λv1 .(x2 @v1 )); λx1 .λx2 .(λf.(f @((λa.a)@x1 )))@(λv1 .(x2 @v1 )); λx1 .λx2 .(λv1 .(x2 @v1 ))@((λa.a)@x1 ); λx1 .λx2 .(λv1 .(x2 @v1 ))@x1; λx1 .λx2 .x2 @x1
図 2. 例: (λx.λf.(f @((λa.a)@x))) of type t1 → ((t1 → t2 ) → t2 ) の TDPEには、f に新しく作った dynamic な変数 x1 を適という形なので、部分評価後にはある M に対して用してみれば良い。もし、f が完全に polymorphic

λx1 .λx2 .M という形を持つことが分かる。
M を求めるには、 入力の項に x1 と λv1 .x2 @v1という 2 つの引数を与える必要がある。なぜなら、な型を持つならば、f は x1 の値を使うことはな
く、安全に f に適用することが出来る。すると、fx2 は t1 → t2 という型を持ち、関数として中で使われる必要があるため x2 自身を適用することは出の本体を得ることが出来、この場合は x1 となり、

λx1 .x1 を得ることが出来る。

来ない。しかし、reﬂect を使ってそれを static な

上向き矢印 (↑t ) は reﬂect と呼ばれる。これはreify の逆であり、datatype representation をコンパイルされた実行可能な値に変換する。

項に変換したら、つまり 2 レベル η 拡張した結果の項 λv1 .x2 @v1 なら適用することが出来るからで

reify を使うことで、TDPE は完全に static な
入力の項を、dynamic な項に変換する。入力の式ある。

や TDPE における全ての static な部分は reify (ま実行すると、残余の項として λx1 .λx2 .x2 @x1 を得たその中での reﬂect) によって全て簡約され、結果ることが出来る。これは入力の項を部分評価した項として全て dynamic な項が得られる。

になっていて、入力の項に存在していた (λa.a)@x

結果として得られた項の全ての static な部分をという redex が評価されている。

3.3

例

4
例として (λx.λf.f @((λa.a)@x)) という式を

call-by-value の TDPE

TDPE で実行することを考えてみる。この式の型は t1 → ((t1 → t2 ) → t2 ) である。

えば、3 節の TDPE で (int → α) → int という型

この項に対する TDPE の実行結果は図 2 に示を持つ式 λx.((λy.1)@(x@2)) を実行すると、結果した。入力の項は全て static な項として考える。

は (x@2) という関数適用を捨てて、(λx.1) となる。

3 節での TDPE は call-by-name であった。例↓t1 →((t1 →t2 )→t2 ) を (λx.λf.f @((λa.a)@x)) に適用

しかし、call-by-value では、関数適用を捨てるこすることで、２レベルの項:とはできない。代わりに let 文として残す必要がある。

λx1 .λx2 .(λx.λf.f @((λa.a)@x))@x1 @ λv1 .x2 @v1

以前の論文 [13] で我々は、call-by-value の

TDPE を導入するために state-based let-insertionを行うものを示した。ここでは、それを紹介するとともに shift/reset-based let-insertion を行う方法

を得ることが出来る。
この２レベルの項の意味について考えてみると、入力として与えた項の型が t1 → ((t1 → t2 ) → t2 )3reify= λt.λv : t.↓t v: Type → Value → TLT

t1 →t2↓b v
v= v= λx¦1 .init; wrap(↓t2 (v @ ↑t1 x¦1 ))↓t1 ×t2 v= pair(↓t1 f st v, ↓t2 snd v)↓

reﬂect =init = wrapstack ← () :: wrapstackwrap(e)wrap-gen(f, e)

λt.λe : t.↑t e[e] =let f :: rest = wrapstack inwrapstack ← ((g ¦ , e) :: f ) :: rest;g¦: Type → Expr → TLT↑b e = e↑t1 →t2 e = λv1 . ↑t2 [e @ ↓t1 v1 ]↑t1 ×t2 e = pair(↑t1 f st e, ↑t2 snd e)
residualize= let f :: rest = wrapstack inwrapstack ← rest;

wrap-gen ([], body) = body
wrap-gen (lst, body)= statically-reduce ◦ reify: Type → Value → Expr

= let (l, r) :: rest = lst in
wrap-gen(rest, h let l = r in body i)

図 3. λ 計算のための call-by-value の

図 4. state-based let-insertion の wrap,

TDPE[...] and init の定義
init ≡ ; 何もしないについても触れる。なお、これらの実装はいずれも Filinski の実装 [9] に基づくものである。Filin-

wrap(e)ski の実装では、例外や gensym、state-based letinsertion [11] などの全てのモナドは Scheme のnative eﬀects を使うことで実現されている。

4.1

≡ hei

[e] ≡ Sk.hlet x¦ = e in k@x¦ i
図 5. shift/reset-based let-insertion のResidualization

wrap, [...] and init の定義

call-by-value の TDPE の構文は call-by-nameの TDPE と同じなので図 1 に、call-by-value のた

実現するか、shift/reset を使って実現するかでめの reify と reﬂect は図 3 に示した。

あって、どちらの方法でも可能である。図 4 に state-call-by-value の TDPE を実現するためには、先ほどの例では捨てられてしまったような dynamic
な関数適用を dynamic な let 文として残す (let-based の let-insertion の定義を示す。shift/resetbased let-insertion では、e を特定のコンテキスト

based の let-insertion の定義を、図 5 に shift/reset-

insertion) 必要がある。let-insertion をするにはstate を使って行う方法と、shift/reset を使って行の中で実行しなくてはならないので、wrap や [...]
は関数ではなくマクロとして定義されている。

う方法がある。

図 3 の init、wrap、[...] を無視すると、reify と

let-insertion を行うには、図 3 で使用している[..]、wrap、init というオペレータを使えばよい。

reﬂect は Danvy の TDPE のように完全な対称性を持っている。

それぞれの役割として、[..] は let 文に残さなくてはならない dynamic な関数適用を登録するもの、

4.2

例

init は (state-based let-insertion において) 状態を初期化するもの、wrap は登録された dynamic な関数を順次、let 文にして展開するものである。

じめの例 λx.((λy.1)@(x@2)) (型は (int → α) →state-based と shift/reset-based の let-insertionの違いはこれら 3 つのオペレータを state を使ってint) は λx. let y = x@2 in 1 へと部分評価される。
dynamic な関数適用 x@2 は捨てられずに、let 文

call-by-value の TDPE を使うと、この節のは

4

t1 /α → t2 /β のための TDPE を求める方法について説明する。
まず、t1 /α → t2 /β は CPS 変換で (t1 × (t2 →t ∈ Type::= b | t1 → t2 | t1 /α → t2 /β
t1 × t2v ∈ Value ::= c | x | λx.v | v0 @v1 | h v i | Sk.v
e ∈ Exprα)) → β という型に対応している。そのため、CPSの関数型の項がどのように変換されるかは従来のpair(v1 , v2 ) | f st v | snd v::= c | x | λx.e | e0 @e1 | h e i | Sk.e

call-by-value の TDPE で ↓(t1 ×(t2 →α))→β v と↑(t1 ×(t2 →α))→β e を実行してみて、結果を観察すれば良い。これらの式を実際に実行してみると、下pair(e1 , e2 ) | f st e | snd e
図 6. 構文: λ 計算と shift/resetのようになる。

↓t1 ×(t2 →α)→β v=として残され、正しく call-by-value で評価されてλp¦1 .init; wrap(↓β (v @ pair(↑t1 f st p¦1 ,λv1 . ↑α [(snd p¦1 @ ↓t2 v1 )])))↑t1 ×(t2 →α)→β e=

いることが分かる。

限定継続のための TDPE

5

λp1 . ↑β [(e @ pair(↓t1 f st p1 ,λx¦1 .init; wrap(↓α (snd p1 @ ↑t2 x¦1 ))))]

この節では shift/reset で拡張した TDPE について説明する。

5.1

上の２つの式において、最も外側の抽象 (λp¦1 ...)と (λp1 ...) は積の型を持つ引数を受け取る。その構文

積にパターンマッチを適用すると、上の式を次のように書き直すことが出来る。

対象とする言語とその型は図 6 に示した。

↓t1 ×(t2 →α)→β v=
λ(x¦1 , k1¦ ).init; wrap(↓β (v @ pair(↑t1 x¦1 ,shift/reset が存在すると、関数型は普通の関数型 t1 → t2 に加えて、４つ組の関数型 t1 /α → t2 /β

λv1 . ↑α [(k1¦ @ ↓t2 v1 )])))を持つ。それぞれの t1 は普通の関数型と同じ引数↑t1 ×(t2 →α)→β e=の型であり、t2 はその関数が返す式の型である。加λ(v1 , k1 ). ↑β [(e@ pair (↓t1 v1 ,λx¦1 .init; wrap( ↓α (k1 @ ↑t2 x¦1 ))))]

えて、α と β はそれぞれ関数が呼ばれる前と後のコンテキストの answer type である。
４つ組の関数型が pure な場合、つまり α と βこうして CPS の関数型を持つ項の TDPE にが polymorphic で同じであるような場合に普通のついて考えたところで、まず reify (↓) を直接形

関数型で表すことにする。shift/reset を含む式

式に戻すことについて考えてみる。CPS 形式ではの型は Danvy と Filinski [5] によって定義されてλ(x¦1 , k1¦ ) は引数と継続を受け取る。直接形式ではおり、今回使用する型システムはそれに pure な関x¦1 が引数を受け取ることに対応し、k1¦ が継続を切り取ることに対応する。よって、直接形式に書き直数型 [3] を加えたものとする。
対象とする言語の項は、ラムダ計算に加えてすと、ある M に対して λx¦1 .Sk1¦ .M となる。

shift/reset の 式 で あ る 。Sk. v と い う 項 は

M を求めようとしたところで、v は ↑t1 x¦1 に
λv1 . ↑α [(k1¦ @ ↓t2 v1 )] という継続のもとで適用(shift k v) を意味し、hvi という項は (resetv) を意味する。また、入力の項は完全に static であり、前述の型システムに基づいて型が付いている

されていることが分かる。直接形式では、これはλv1 . ↑α [(k1¦ @ ↓t2 v1 )] というコンテキストのもとと仮定している。

5.2

で、v@ ↑t1 x¦1 を実行することと一致する。
よって ↓(t1 ×(t2 →α))→β v はResidualization

λx¦1 .Sk1¦ .init;
wrap(↓β (λv1 . ↑α [(k1¦ @ ↓t2 v1 )])@(v @ ↑t1 x¦1 ))この節では、CPS の関数型を持つ項が call-by-となりそうである。

value の TDPE でどのように評価されるかを観察

しかし、これはコンテキストの範囲が定まっし、それを直接形式に戻すことで４つ組の関数型ていないため、うまく動かない。v は static な

5reify = λt.λv : t.↓t v: Type → Expr → TLT
↓

↓b v
v

t1 →t2↓t1 /α→t2 /β v
↓t1 ×t2 v
reﬂect= v= λx¦1 . ↓t2 (v @ ↑t1 x¦1 )= λx¦1 .Sk1¦ . init; wrap(↓β h let v1 = v @ ↑t1 x¦1 in (↑α [k1¦ @ ↓t2 v1 ])i)
= pair(↓t1 f st v, ↓t2 snd v)= λt.λe : t.↑t e: Type → Value → TLT↑b e = e↑t1 →t2 e = λv1 . ↑t2 (e @ ↓t1 v1 )↑t1 /α→t2 /β e = λv1 .Sk1 . ↑β [h let x¦1 = (e @ ↓t1 v1 ) in (init; wrap(↓α (k1 @ ↑t2 x¦1 )))]
↑t1 ×t2 e = pair(↑t1 f st e, ↑t2 snd e)
図 7. 限定継続のための TDPE

shift 式を含むかもしれない static な項である。

ものを使用した。その理由として、実際に計算をよって、もし ↓(t1 ×(t2 →α))→β v が上のように定義行う対象言語の shift/reset が let-insertion をされていたとすると、v の中の static な shift が行う shift/reset に影響を与えてしまうためであ全ての計算の残りを切り取ってしまう。代わりに、る。例えば、↓t1 /α→t2 /β v において k1¦ @ ↓t2 v1 と(λv1 . ↑α [(k1¦ @ ↓t2 v1 )]) というコンテキストのみいう dynamic な関数適用を外側の wrap の位置にを切り取る必要がある。v が切り取るコンテキス残す必要がある。しかし、k1¦ @ ↓t2 v1 はもうすでにトの範囲を定めるために、↓(t1 ×(t2 →α))→β v を次他の static な reset によって囲まれているので、のように定義する。

その wrap の位置に残すことは出来ない。

λx¦1 .Sk1¦ .init;
wrap(↓β h(λv1 . ↑α [k1¦ @ ↓t2 v1 ])@(v @ ↑t1 x¦1 )i)
同様にして reﬂect ↑t1 /α→t2 /β e は

よって、shift/reset-based let insertion を使うには、shift2 [6] が必要となる。

5.4

λv1 .Sk1 .
↑β [h(λx¦1 .init; wrap(↓α (k1 @ ↑t2 x¦1 )))例

いくつかの例を実行した結果を図 9 に示した。

@(e @ ↓t1 v1 )i]parse という関数は、型の parser である。
例えば、’((A * B) / C -> D / E) という型を(make-func-sr (make-prod (make-baseのように定義が出来る。
これらの式の static や dynamic な β-redex を、

static や dynamic な let 式で書き換える事で、図7 の限定継続のための TDPE を得る事ができる。

’A) (make-base ’B)) (make-base ’C)(make-base ’D) (make-base ’E))

(static な) shift/reset を使っているため、shift
や reset の命令 [7] をもつ言語で実行することを仮定している。

という Scheme 上で使える構造体に変換するような関数である。
一番最初の例としては pure な関数型を持つ式

5.3(λx.(λf.(f @x))) を考える。これは pure な関数型なので、call-by-value の TDPE と同じように部分

Scheme での実装

図 7 の TDPE を単純に Scheme で実装した例

評価され、(λx.x) となる。

を図 8 に示す。メインの関数 residualize は式と二 つ 目 の 例 は pure で な い 関 数 型 を 持 つ 式

その型を受け取り、TDPE の結果を返すような関(λf.(f @(Sk1 .(k1 @(Sk2 .(k2 @(+ 1 2))))))) であ数である。

る。この式中の Sk1 は、f @2 という継続と、外側の継続 h を受け取る。つまり、Sk1 が切り取

4 節での let-insertion については state-based の6

る継続をまとめると、hh@(f @2)i となる。また、正当性の証明6

Sk2 は k@2 という継続を受け取る。ここで実行
結果を簡略化してみると、

この節では、call-by-name の TDPE の証明を(lambda (f) (shift h (reset h (f 3))))

紹介した後、今後、他の TDPE の証明がどのようとなり、Sk1 と Sk2 の二つの static な shift 式

な形になるかについての展望を述べる。

が実行され、必要な dynamic な shift 式が作ら6.1

れたことが分かる。
三つ目の例もcall-by-name の TDPE の正当性

pure で な い 関 数 型 を 持 つく Sk は hh@(f @2)i という継続を受け取り、そcall-by-name の TDPE については、Filinski が意味論に基づく Kripke の論理関係を使った証明を行っている [8]。ここではそれを平易に噛み砕いてれを k@(k@(1 + 2)) と２回使っている。ここで実紹介する。

例 で 、受 け 取った 継 続 を ２ 回 使 う よ う な 例

λf.f @(Sk.k@(k@(1 + 2))) である。前の例と同じ

行結果を見てみると、継続は実際に２回に展開さ証明する上で必要となる call-by-name の TDPE

れていて、正しく実行されていることが分かる。

の定義はすでに図 1 に示している。また、TDPE

最後の二つの例は shift/reset で書かれた

前は static な項であるが、TDPE 後には dynamic(typed) printf 関数 [2] に関する実行例である。
まず、この関数 (lambda (f) (reset (f (cons(% str) (f (cons " is " (% str))))))) は、な項となるため、それら 2 つを比較するために dy-

関数 f をペアとして与えられた二つの string を・dynamic な項を static に変換する関数
I[[x]]ρ = ρ(x)namic な項を static に変換する関数が必要となる。

結合させて一つの string を返すような関数だとすI[[λx.M ]]ρ = λv.I[[M ]]ρ[x := v]

ると、C 言語での sprintf "%s is %s" と同じ働I[[M @N ]]ρ = I[[M ]]ρ@I[[N ]]ρ

きをする。(% str) は２回使われるので、この式
は引数を２つ受け取って string を返すような関数

これは、dynamic な term に対するインタプリである。よってこの式の型は string -> string

タととらえても良い。

-> string となる。この型は実際には pure な型

次に、型に関する帰納法で、次のような論理関であるが、四つ目の例では pure でない型を持つと係を定義する。

して、五つ目の例では pure な型としてそれぞれ実(論理関係の定義)
Rb (M, M 0 ) ⇔ I[[M ]]φ ∼ M 0
RA→B (M, M 0 ) ⇔ ∀RA (M1 , M10 ) について
RB (M @M1 , M 0 @M!0 )行した例となっている。

pure でない型として実行した四つ目の例は複雑な結果となっているが、let 式を η 簡約したり、
tail な位置の継続を全て実行してしまうと、(lambda (f) (lambda (x) (lambda (y)(reset (let ((g3 (f (cons " is " y))))ここで、φ は M の自由変数と M 0 の自由変数を関係づける環境である。また ∼ は call-by-nameのもとでの等価性を示す。ここでは、M と M 0 で(reset (f (cons x g3))))))))

同じ変数名を使うこととし、φ は恒等写像とする。

のようになる。この結果の式は、sprintf "%s is

上に示した論理関係は標準的なものだが、TDPE%s" で期待されたように、指定された数の引数を受け取って string を返す関数になっている。
最後に五つ目の例は、 前の例と同じように、指の証明には次のような補題が必要となる。

(1) RT (M ρ, M 0 ρ0 ) ならば I[[↓T M ]]ρ ∼ M 0 ρ0

定された数の引数を受け取って string を返す関数(2) I[[M ]] ∼ M 0 ならば RT (↑T M, M 0 )になっている。上の例で示した簡略化した式とほとんど同じになっているが、reset の有無が異なる

これらは、論理関係と、reify, reﬂect の間の関係のは、上の例では pure でない型として実行していを規定している。これらの補題は、型に関する帰納るので、pure でない場合に備えて継続を区切って法で示すことができる。

いるためである。

7

論理関係の基本定理は次のようになる。

7(定理)
Γ ` M : T かつΓで定義されている全ての変数 x

結論
この論文では限定継続 shift/reset の TDPE

0について RΓ(x) (ρ(x), ρ (x)) であればを改良し、その実装と実行例を示した。また、限定

RT (M ρ, M ρ0 )継続 shift/reset の TDPE の正当性を証明するために足掛かりとなる call-by-name の TDPE のここで M ρ は M に ρ を施した項である。こ

正当性を示し、今後の証明の方針を示した。

の定理は、項に関する帰納法で証明することがで

参考文献

きる。
論理関係の基本定理と上の補題 (1) を使うとTDPE の正当性を示す次の系を示すことができる。
` M : T ならば I[[↓T M ]] ∼ M

系

6.2[1] Asai, K. “Logical Relations for Call-by-value
Delimited Continuations,” Trends in Functional Programming (TFP 2005), Vol. 6,
pp. 63–78, Intellect (2007).

call-by-value の正当性に向けて[2] Asai, K. “On Typing Delimited Continuations: Three New Solutions to the Printf
Problem,” To appear in Higher-Order andFilinski [9] は、call-by-value の computational
λ-calculus に対する TDPE を示しており、そこで
let-insertion をモナドの形で導入している。その正Symbolic Computation, 17 pages (2010).

当性についても、call-by-name の手法を computa-[3] Asai, K., and Kameyama Y “Polymorphic

tional λ-calculus の値と計算のレベルで相互再帰的

Delimited Continuations”, In Z. Shao editor,
5th Asian Symposium on Programming Languages and Systems (APLAS 2007), pp. 239-に定義することで証明できると書いているが、詳細は記述されていない。現在、この方針で証明を試みているところである。

254 (November 2007).

さらに、この証明を shift/reset 付きの TDPEの正当性の証明に拡張するには、以下の点を考慮す[4] Danvy, O. “Type-Directed Partial Evalua-

る必要があると予想される。まず、第１に TDPE
定義もそれを考慮する必要があると思われる。論

tion,” Conference Record of the 23rd Annual ACM Symposium on Principles of Programming Languages, pp. 242–257 (January

理関係の RA→B の場合は、任意の関係づいている

1996).

中に静的な shift が実行されるため、論理関係の引数を受け取ったとき、実行結果も関係づいてい[5] Danvy, O., and A. Filinski “A Functional Ab-

ることを保証するが、shift/reset が使われる場

straction of Typed Contexts,” Technical Report 89/12, DIKU, University of Copenhagen(July 1989).

合にはその継続の振る舞いも保証する必要がある。
これには、shift/reset に対する通常の部分評価の正当性 [1] で使われた論理関係が参考になると思[6] Danvy, O., and A. Filinski “Abstracting Control,” Proceedings of the 1990 ACM Confer-

われる。
次に、shift/reset 付きの TDPE において

ence on Lisp and Functional Programming,
pp. 151–160 (June 1990).

は、入力プログラムの shift に加え、let-insertionを行うために shift2 /reset2 が使われる。したがって、論理関係を shift/reset だけでなく[7] Filinski, A. “Representing Monads,” Confer-

shift2 /reset2 も扱えるように拡張する必要があるかも知れない。現在、これらの考察をもとに、そence Record of the 21st Annual ACM Symposium on Principles of Programming Lan-の証明を試みているところである。

guages, pp. 446–457 (January 1994).

8

(define-struct base (base-type))(define-struct func-p (domain range))(define-struct func-sr (domain bef range aft))(define-struct prod (type1 type2)); domain -> range; domain / bef -> range / aft; type1 * type2(define wrap-stack ’())
(define (init)(set! wrap-stack (cons ’() wrap-stack)))(define (wrap e)(let ([lst (car wrap-stack)])(set! wrap-stack (cdr wrap-stack))(wrap-gen lst e)))(define (add e)(let ([g (gensym)])(set! wrap-stack (cons (cons (list g e) (car wrap-stack))(cdr wrap-stack)))g))(define (wrap-gen list body)(cond [(null? list) body][else (wrap-gen (cdr list)‘(reset (let ((,(car (car list)) ,(car (cdr (car list))))) ,body)))]))(define (residualize v t)
(letrec([reify (lambda (t v)(cond [(base? t) v][(func-p? t) (let ([t1 (func-p-domain t)][t2 (func-p-range t)][x1 (gensym)])‘(lambda (,x1) ,(reify t2 (v (reflect t1 x1)))))][(func-sr? t) (let ([t1 (func-sr-domain t)] [t2 (func-sr-range t)][bef (func-sr-bef t)] [aft (func-sr-aft t)][x1 (gensym)] [k1 (gensym)])‘(lambda (,x1)(shift ,k1 ,(begin (init) (wrap (reify aft (reset(let ([v1 (v (reflect t1 x1))])(reflect bef (add ‘(,k1 ,(reify t2 v1))))))))))))][(prod? t) (let ([t1 (prod-type1 t)] [t2 (prod-type2 t)])‘(cons ,(reify t1 (car v)) ,(reify t2 (cdr v))))]))][reflect (lambda (t e)(cond [(base? t) e][(func-p? t) (let ([t1 (func-p-domain t)][t2 (func-p-range t)])(lambda (v1) (reflect t2 ‘(,e ,(reify t1 v1)))))][(func-sr? t) (let ([t1 (func-sr-domain t)] [t2 (func-sr-range t)][bef (func-sr-bef t)] [aft (func-sr-aft t)] [x1 (gensym)])(lambda (v1)(shift k1 (reflect aft (add ‘(reset(let ([,x1 (,e ,(reify t1 v1))]),(begin (init)(wrap (reify bef (k1 (reflect t2 x1))))))))))))][(prod? t) (let ([t1 (prod-type1 t)] [t2 (prod-type2 t)])(cons (reflect t1 ‘(car ,e)) (reflect t2 ‘(cdr ,e))))]))])(reify t v)))

図 8. Scheme での限定継続のための TDPE の実装

9

> (residualize (lambda (x) ((lambda (f) f) x)) (parse ’(A -> A)))(lambda (x) x)> (residualize (lambda (f) (f (shift k (k (shift k2 (k2 (+ 1 2)))))))(parse ’((I / A -> C / B) / A -> C / B)))(lambda (f) (shift h(reset (let ((g3 (reset (let ((g1 (f 3))) (reset (let ((g2 (h g1))) g2)))))) g3))))> (residualize (lambda (f) (f (shift k (k (k (+ 1 2))))))(parse ’((I / A -> B / I) / A -> B / I)))
(lambda (f) (shift h(reset (let ((g3 (reset (let ((g1 (f 3))) (reset (let ((g2 (h g1))) g2))))))(reset (let ((g6 (reset (let ((g4 (f g3))) (reset (let ((g5 (h g4))) g5))))))g6)))))); (printf)> (define (str x) x)> (define (% to_str) (shift k (lambda (x) (k (to_str x)))))> (residualize (lambda (f) (reset (f (cons (% str) (f (cons " is " (% str)))))))(parse ’(((S * S) / A -> S / A) / A -> (S / A -> (S / A -> S / A) / A) / A)))(lambda (f) (shift k(reset (let ((g9 (k(lambda (x) (shift k1(reset (let ((g8 (k1(lambda (y) (shift k2(reset (let ((g6 (reset (let ((g3 (f (cons " is " y))))(reset (let ((g5(reset (let ((g4 (f (cons x g3)))) g4))))g5))))))(reset (let ((g7 (k2 g6)))g7)))))))))g8)))))))g9))))> (residualize (lambda (f) (reset (f (cons (% str) (f (cons " is " (% str)))))))(parse ’(((S * S) -> S) -> (S -> (S -> S)))))(lambda (f) (lambda (x) (lambda (y) (f (cons x (f (cons " is " y)))))))

図 9. 限定継続のための TDPE の Scheme での実行例[8] Filinski, A. “A Semantic Account of TypeDirected Partial Evaluation,” In G. Na-

pp. 378–395 (September 1999).
[9] Filinski, A. “Normalization by Evaluation

dathur, editor, Principles and Practiceof Declarative Programming (LNCS 1702),

for the Computational Lambda-Calculus,” In
S. Abramsky, editor, Typed Lambda Calculi
10and Applications (LNCS 2044), pp. 151–165(May 2001).
[10] Jones, N. D., C. K. Gomard, and P. Sestoft
Partial Evaluation and Automatic Program
Generation, New York: Prentice-Hall (1993).
[11] Sumii, E., and N. Kobayashi “A Hybrid Approach to Online and Oﬄine Partial Evaluation,” Higher-Order and Symbolic Computation, Vol. 14, Nos. 2/3, pp. 101–142, Kluwer
Academic Publishers (2001).
[12] Thiemann, P. J. “Cogen in Six Lines,” Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’96), pp. 180–189 (May 1996).
[13] Tsushima, K., and Asai, K. “Towards TypeDirected Partial Evaluation for Shift and Reset” Normalization of Evaluation 09, (August 2009).

11