shift/reset 付き TDPE の抽出
廣田 知子 1 , 浅井 健一 1
1 お茶の水女子大学

hirota.noriko@is.ocha.ac.jp, asai@is.ocha.ac.jp
概 要Danvy により提案された type-directed partial evaluator (TDPE) は，与えられた項を normal form に評価する関数であり，Filinski によって call-by-value 及び callby-name の単純型付き λ 計算における TDPE の正当性が示されている．一方，対馬らの論文によって，shift/reset 付きに拡張された TDPE が提案されているが，未だ正当性は保証されていない．
本研究では，対馬らによって提案された TDPE を参考に，CPS 変換を行った shift/reset付き TDPE を定義し，その正当性を示す試みを行った．証明は CPS 変換した論理述語を用いて行った．さらに，call-by-value の shift/reset を含んだ型付き λ 計算の正当性（本研究で定義した論理述語の定義を満たす）の証明を定理証明系システム Coq によって定式化することにより，OCaml 言語のプログラムを抽出した．抽出されたプログラムは，
複雑にはなっているものの，概ね対馬らによって提案された shift/reset 付 TDPE の形を成していることが見て取れるような構造になっている．

1

はじめに

type-directed partial evaluator（TDPE）は，Danvy により提案された [3] 部分評価器であり，termとその term の型が渡されたとき，その型によって場合分けを行いながら，term を normal form へと評価する関数である．TDPE の利点として，term の中身を見ないが故に，term の構造における場合
分け等を行わずに部分評価を行う為，高速であることが挙げられる．call-by-value 及び call-by-nameの単純型付き λ 計算における TDPE においては，その正当性が [4] にて Filinski により既に示されている．Filinski はその論文にて，論理関係を用いた Tait 流の証明を行っている．call-by-value だ
けでなく，任意の monadic eﬀect を持つ体系を対象としており，let-insertion を含めて証明が為されている．しかし，その証明は難解で，他の体系，特に shift/reset が入った場合にどうなるかを考えようとしても，そのまま拡張しようとするのは難しい．
一方，対馬らによって提案 [8] された shift/reset 付 TDPE においては，直感的な説明はされているものの，未だその正当性が示されていなかった．
[6] にて，Ilik が Coquand の研究 [2] を基に，性質の存在証明から shift/reset 付 TDPE を抽出す
る方法の足がかりを作っている．つまり，どのような性質の存在証明を行えば TDPE が抽出されるのかを明らかにした．定式化においては，（Ilik 自身の論文である）[5] を拡張した形となっている．
しかしその論文 [6] にて扱われている限定継続は論理から見たものであり，我々が考える通常の限定継続とは異なっているものと考えられる．
そこで本研究では，対馬らが提案した shift/reset 付 TDPE を CPS 変換し，そのプログラムとの対応を付けながら，通常の限定継続を扱える形で Ilik の手法 [6] を定式化し直した．その際，• 対馬らの TDPE のどの場所を CPS 変換すれば良いかは自明でなかった為，[6] が基になければ難しく，特に，TDPE に渡す static な term も CPS にしなければならないことが，Ilik の定式化を参考にすることにより分かった．
• その一方で、Ilik の定式化を通常の限定継続用に新たに定式化し直す際には，対馬らの TDPEと対応を付けつつ考えないと難しかった．
1

という意味において，対馬らと Ilik 双方の研究に融合させた形となっている．
本研究で行った定式化は，shift/reset なし λ 計算における TDPE における定式化手法を，shift/reset付きに拡張した形になっている為，本論文では，まず call-by-value の shift/reset なし λ 計算における TDPE の抽出から説明する．本論文の構成は，まず 2 節にて call-by-value の shift/reset なし λ計算における性質の存在証明から TDPE の抽出を行う方法と抽出された TDPE の説明を行い，そして 2 節での手法を拡張することによって call-by-vaule の shift/reset 付 λ 計算における性質の存在証明から shift/reset 付 TDPE が得られることを 3 節で述べる．そして 4 節にて本研究の今後の課
題を考察する．
以降，本論文で定義する call-by-value の shift/reset なし λ 計算を λcbv ，call-by-value の shift/reset
S/R
付 λ 計算を λcbv と表記する．

2

λcbv における TDPE の抽出

本節では，call-by-value の（shift/reset を含まない）λ 計算 λcbv において，どのように TDPE を抽出したかを説明する．対馬らが [8] にて記している call-by-value の λ 計算における TDPE の定義は，let-insertion を用いて行われている．その let-insertion に shift/reset を用いた定義が以下である．

t ∈ Type := b | t1 → t2v ∈ Value := x | λx.v | v0 @ v1e ∈ Expr := x | λx.e | e0 @ e1
Reify ” ↓ ”↓base v
↓A→B v:==

Type → Value → TLTv
λx .h↓B (v @ ↑A x1 )i

Reflect ” ↑ ”↑base e↑A→B e:==Type → Expr → TLTe
λv1 . ↑B Sk1 .let g  = e @ ↓A v1 in k1 @ g 

Expr は dynamic term，つまり TDPE が出力する部分評価後のプログラム（構文木）を表し，Value
は static term，つまり TDPE 時に（部分評価結果のプログラムを出力するために）実行されるプログラムを表す．また，TLT は Expr と Value が混ざった式を表していて，この中の static な部分を実行すると TDPE の結果が dynamic な式として得られることになる．アンダーラインの付いている式が dynamic な式を出力する命令，オーバーラインの付いている式が static な命令である．又， の付いている変数は，他の変数とぶつかることのないように選ばれた，fresh な変数である．Reflect の
A → B のケースは，call-by-name では λv1 . ↑B (e @ ↓A v1 ) となるところであるが，call-by-value
では dynamic な (e @ ↓A v1 ) を let-insertion を使って出力している．Sk で，その時点での継続を切り取り，fresh な変数 g  を使って (e @ ↓A v1 ) を let 文に残し，以降の計算には g  が渡されている．この let 文が出力されるのは，reify の A → B のケースで dynamic な束縛が作られる（staticな reset の）直下である。
この TDPE の定義は，static な shift/reset が使われている．Coq は shift/reset を提供していない
為，上の TDPE 定義を直接 Coq で定式化することは出来ない。そこで本研究では，その shift/reset
を CPS 変換して削除することとした．しかし TDPE のどの場所をどのようにして CPS 変換すれば良いのかは自明には分からなかった．そこで Ilik の研究 [6] を参考にし，どの箇所が CPS 変換に相当しているのかをみた．その論文において，抽出すると TDPE となると説明されている定理の定義を調べると，reify は型と CPS 変換された value を受け取り，CPS 変換されていないような termを返すこと，reflect は型と（CPS 変換されていない）term を受け取り，CPS 変換されている value
2

を返す関数となっていることが分かった．上の定義の static な term を CPS 変換したものが，以下に定義する関数である：

Reify ” ↓ ” : Type → Value → TLT↓base v = v↓A→B v = λx1 .v @ (↑A x1 ) @ (λv. ↓B v)
Reflect ” ↑ ” : Type → Expr → TLT↑base e = e↑A→B e = λv1 .λk1 .(λg  .k1 @ (↑B g  ))@(e@ ↓A v1 ).
この定義は，先の call-by-value の TDPE のうち，reify に渡される引数 v と reflect が返す static な
値を CPS 変換したものである．reify に渡される引数 v は CPS になったので，それを使う際には引
数 (↑A x1 ) に加えて，継続が渡されている．また、reflect が返す値は，λk1 のように継続を受け取る格好になっている．このように CPS 変換を施すと，shift/reset を使って行っていた let-insertionを shift/reset を使わずに行うことができる．上記の CPS の TDPE では，それを Coq での実装に合わせて let 文を展開した (λg  ....) @ (...) という形で表している．
このように CPS 変換をすると，その副作用として TDPE が受け取る static な term も CPS でな
くてはならなくなる．例えば [8] における CPS 変換前の TDPE では，λx.((λy.y)@x) : base → baseにおける TDPE の結果を得たければ，この項をそのまま reify に渡せば良かった．しかし CPS 変
換した TDPE にて λx.((λy.y)@x) : base → base を実行したい場合，この項を CPS 変換した式をreify に渡さねばならなくなっているのである．TDPE が受け取るものは CPS になるが，出力は直接形式のままである．上の例では，λx.((λy.y)x) を CPS 変換したものを TDPE に渡すと，その直接形式での正規形 λx.x が得られる．

2.1

λcbv の構文

まず，本研究で定義した λcbv の構文を以下に示す．

typeenvironment
variable term
term

:
typ 3
A :=
: world 3 w, Γ :=
:
`v 3
v :=
:
`t 3
p :=

base | A1 → A2
list of typ
hyp | wkn(v)v | lam(p) | app(p1 , p2 )本論文においては，束縛変数は de Bruijn index で表される．直感的には，hyp は一番内側の binder
で束縛されている変数を，wkn(v) は v の中の束縛変数の値を 1 繰り上げるような命令を意味している．例えば id 関数は，lam(hyp)，λx.λy.y@x は lam(lam(app(hyp, wkn(hyp)))) と書ける．
この構文では任意の term を書くことが出来るが，以下，型の付いている term だけを考える．次のような型規則を使い term を定義すると，型の付く term のみしか書けなくなる．
p : w `v A
hyp : A, w `v A wkn(p) : B, w `v A

v : w `v A
v : w `t A

p : A, w `t B
lam(p) : w `t A → B

p : w `t A → B q : w `t A
app(p, q) : w `t B

一見，一般的な型推論規則と差異がないようにも見えるが，この規則では e : w `t A の e が term，w `t A が e の型となっている．一般的に定義される term の型とは異なり環境 w も型情報に含まれており，加えて一般的な型推論規則の条件をも満たしていなければ term として成立しなくなっていることが上の定義の特徴である．上の定義をみれば分かる様に，wkn(p) の型規則は weakening を表すものとなっている．このように表現することにより，w `t A は論理式「w ⇒ A」と捉えることが出来る．よって Curry Howard 同型により，w `t A の成立と，この型の term が存在すること

3

が同値となる．又，型情報に環境を加えることと，de Bruijn index の使用により，α 同値問題を考える必要がなくなっている．Coq で term を定式化する際は，以下のように推論規則のみで定義した．尚，term の定式化に関しては [6] における定式化を参考にした．

set Implicit Arguments.
Inductive var : world -> typ -> Set :=| var_Hyp : forall w A, var (A :: w) A
| var_Wkn : forall w A B, var w A -> var (B :: w) A.
Inductive tm : world -> typ -> Set :=| tm_var : forall w A, var w A -> tm w A| tm_Lam : forall w A B,
tm (A :: w) B -> tm w (arrow A B)
| tm_App : forall w A B,
tm w (arrow A B) ->tm w A ->tm w B.
この定義を用いて，例えば id 関数は（world w において (base → base) 型を持つとすると，）(tm_Lam (tm_Hyp w base)) と記述できる．
（Set Implicit Arguments を使用しない場合は，全ての情報を記述しないといけない為，(tm_Lam w base base (tm_Hyp w base)) と記述する．
）
次に λcbv における normal form, neutral term を定義する．normal form は正規形であり，これ以上簡約出来ない term となっている．neutral term は変数を正規形で呼び出した形で、変数の値が具体化しない限り、これ以上、実行を進められない term を意味している．

normal form :neutral term :

`nf
`ne

3 nf := ne | lam(nf )3 ne := v | app(ne, nf ) | let(nf1 , app(ne, nf2 ))let(nf1 , app(ne, nf2 )) は，app(ne, nf2 ) を（nf1 の中の）0 番の変数に束縛して nf1 を実行するような let 文であり，app(lam(nf1 ), app(ne, nf2 )) と同じことである．この式は call-by-name ではさらに β 簡約出来てしまうが，call-by-value では lam(nf1 ) に渡される項が value でないと簡約は出来ない．しかし app(ne, nf2 ) は（これ以上簡約出来ないような）application であり，value ではない為，
app(lam(nf1 ), app(ne, nf2 )) はこれ以上簡約出来ない項であり，neutral term として定義する必要がある．この式は，これ以上実行を進められない項 app(ne, nf2 ) を，let 文に残していることに相当する．又，normal form，neutral term の推論規則は term の定義と同様にして以下の如く表現される：
p : A, w `nf B
p : w `ne A
p : w `nf A

lam(p) : w `nf A → B

p : w `ne A → B q : w `nf A
v : w `v A
v : w `ne A
app(p, q) : w `ne B
p : A, w `nf B q : w `ne C → A q 0 : w `nf C
let(p, app(q, q 0 )) : w `ne B

2.2

Soundness と Completeness の証明

本研究では Tait 流の論理述語を用いて，Kripke 意味論に対する soundness と completeness の定理を定義している．使用する論理述語は，call-by-value における一般的な定義（Pierce の著書 [7]S/Rに説明がある）と，[5]（λcbv においては [6]）における Ilik の定義，そして上述の CPS 変換した
TDPE を参考に定義している．λcbv にて使用する論理述語は以下の如く定義する．

4

1 (base)
Rw
1
Rw (A → B):= w ` base
1 (A) ⇒:= ∀w1 , ∀T, w ≤ w1 ⇒ Rw
1
1 (B) ⇒ w ` T ) ⇒(∀w2 , w1 ≤ w2 ⇒ Rw
22
w1 ` T

1 (A )) ∧ (R1 (A )) ∧ ... ∧ (R1 (A ))Rs1w ((A1 , A2 , ..., An )) := (Rw
1
2
n
w
w

ここで引数として渡されている ` は，world と型における述語であれば何でも良い．又， ≤ はworld の大小関係を表している．以下の様な ≤ の定義と公理を与えれば，R1 における soundnessを示すことが出来る．

(i) w ≤ w(ii) w ≤ w0 ⇒ w ≤ (A, w0 )公理 1 ∀w, ∀w0 , ∀A, w ≤ w0 ⇒ w ` A ⇒ w0 ` A
補題 1 ∀w, ∀w0 , ∀Γ, w ≤ w0 ⇒ Rs1w (Γ) ⇒ Rs1w0 (Γ)
定理 1 (Soundness, λcbv )1 (A) ⇒ w 0 ` T ) ⇒ w ` T∀A, ∀Γ, ∀w, ∀T, Γ `t A ⇒ Rs1w (Γ) ⇒ (∀w0 , w ≤ w0 ⇒ Rw
0

Proof. Γ `t A における帰納法．
（補題 1 を使用する．
）2
定理 1 の定義が意味するところは，「Γ のもとで A が成り立つなら，Γ を満たす任意の w の元で Aが成り立つ．
（言い換えると，Γ のもとで A 型になるような term があるなら，Γ を満たす値環境の中で A 型として振る舞う値が存在する）」である．ただし，その「A 型として振る舞う値」というのは，ここでは CPS になっているので，Γ を満たす環境の中で，A 型の値を受け取ったら Ans になるような継続を受け取ったら，Ans が成り立つ，ということになる．この定理の証明を抽出すると，CPS 変換に相当している．実際，証明は CPS 変換のプログラム通りに進んでゆく．
completeness の証明には，` を `nf に置換した論理述語を用いる．この述語の名前を R，Rs と置くこととする．定義は以下の如く．

Rw (base) := w `nf base
Rw (A → B) := ∀w1 , ∀T, w ≤ w1 ⇒ Rw1 (A) ⇒(∀w2 , w1 ≤ w2 ⇒ Rw2 (B) ⇒ w2 `nf T ) ⇒w1 `nf T
Rsw ((A1 , A2 , ..., An )) := (Rw (A1 )) ∧ (Rw (A2 )) ∧ ... ∧ (Rw (An ))先述したように，Curry Howard 同型により「w `nf A」は「w `nf A を型に持つ term が存在する」とみなすことが出来る．一般的に completeness，soundness の証明に使われる論理述語と比較して特に異なっているのは，論理述語が受け取る型が A → B のケースが複雑になっていることと，
world w を受け取っていることである．前者は CPS 変換を行っている為であり，特に，call-by-name
における論理述語の定義ならば Rw (A) ⇒ Rw (B) となるところを，Rw (B) ⇒ Ans という形の継続をとるようになっている．後者による利点は，world を持ち歩くことで，上手く α 変換の問題を回避していることにある．尚，R は TDPE の世界においては，実行済みの（中味を見ることが出来ない）値（或は関数）を意味している．
又， ≤ は，ここでは以下の様に定義する．

5∀A, w ≤ (A, w)
soundness の証明をしたときとは違って，ここでは ≤ について推移律が成り立つ必要がない．次の補題は，変数の weakening が 1 回だけ行えることを示している．
補題 2 ∀w, ∀w0 , ∀A, w ≤ w0 ⇒ w `v A ⇒ w0 `v A

Coq で定式化する際には， ≤ は Set 型として定義している為，抽出された関数にも登場することになるが，その関数内においては変数名のカウンタをひとつ増やす役割をすることになる．
以下の completeness の定理を証明し，その証明を抽出したものが，λcbv の TDPE となる．
定理 2 (Completeness, λcbv )∀A, (i) ∀w, Rw (A) ⇒ w `nf A(ii) ∀w, w `v A ⇒ Rw (A)Proof. A における帰納法．
（補題 2 を使用する．
）2(i) の定義は，A 型の static な値が存在するなら，A 型の正規形が存在する（つまり値を正規形に変換できる）ことを意味しており，(ii) は，A 型の変数は，いつでも A 型の static な値に変換することができることを意味する．(i) が，先に示した TDPE のモデルにおける Reify，(ii) が Reflect にそれぞれ対応しており，モデルの定義通りに証明していくことが可能である．

2.3

TDPE の抽出

soundness，completeness の証明は，それぞれ CPS 変換，CPS の TDPE のプログラムと一対一の関係にあり，実際，証明はプログラムを見ながら，その通りに証明した．completeness の証明から得られる Coq 上の関数定義（Print コマンドを用いれば見る事が出来る）に登場する，型に関する帰納法の原理を展開して, 自明な β 簡約を行うと，以下に示す関数が得られる．
Fixpoint reify (t : typ) : (forall w : world, R w t -> nf w t) :=match t as t0 return (forall w : world, R w t0 -> nf w t0) with| base => (fun (w : world) (X : R w base) => X)| arrow t0 t1 => (fun (w : world) (X : R w (arrow t0 t1)) =>nf_Lam(X (t0 :: w)t1(lew_cons t0 w)(reflect t0 (t0 :: w) (var_Hyp w t0))
(fun (w2 : world) (_ : t0 :: w <== w2) (X0 : R w2 t1) =>reify t1 w2 X0)))
end
with reflect (t : typ) : (forall w : world, var w t -> R w t) :=match t as t0 return (forall w : world, var w t0 -> R w t0) with| base => (fun (w : world) (H : var w base) => nf_ne (var_ne H))| arrow t0 t1 => (fun(w : world)(H : var w (arrow t0 t1))
(w1 : world)(T : typ)(H0 : w <== w1)(X : R w1 t0)(X0 : forall w2 : world, w1 <== w2 -> R w2 t1 -> nf w2 T) =>6

nf_ne(ne_Let(X0 (t1 :: w1) (lew_cons t1 w1) (reflect t1 (t1 :: w1) (var_Hyp w1 t1)))(var_ne (wkn_var H0 H)) (reify t0 w1 X)))end.

lew_cons は completeness の証明にて使用した ≤ であり，lew_cons t0 w は w ≤ (t, w) を表している．これは，変数名のカウンタをひとつ増やす役割を担っている．又，nf_ne と var_ne は，受け取った neutral term を nomal form，variable term を neutoral term としてそれぞれ認識する為の命令である．<==は，lew_cons の型を表している．wkn_var は補題 2 の証明により得られた関数である．例えば wkn_var (H1: w <== w’) (H2: var w A) といった式が与えられたとき，この式は var w’ A を型として持つ項を返す．
（H2 は variable term を表す）<==の定義により，w’ は w の先頭に要素を一つ加えたものである．故に，var w’ A は H2 の状態よりも，（一つ変数名が進んだ）
variable term を表す型となる．よって上の式は var_Wkn H2 となる．以上を踏まえて上の関数をみると，本節の冒頭にて示した，CPS 変換を施した TDPE に等しい定義になっているであろうことが分かる．さらにこの関数に Extraction コマンドを用いて OCaml のプログラムを抽出したものが以下である．
(** val reify : typ -> world -> r -> nf **)let rec reify t w x =match t with
| Base -> Obj.magic x| Arrow (t0, t1) ->Nf_Lam (w, t0, t1,
Obj.magic x (Cons (t0, w)) t1 (Lew_cons (t0, w))(reflect t0 (Cons (t0, w)) (Var_Hyp (w, t0)))(fun w2 x0 x1 -> reify t1 w2 x1))(** val reflect : typ -> world -> var -> r **)and reflect t w h =match t with
| Base -> Obj.magic (Nf_ne (w, Base, (var_ne w Base h)))| Arrow (t0, t1) ->Obj.magic (fun w1 t2 h0 x x0 ->Nf_ne (w1, t2,
Ne_Let (w1, t1, t2, t0,(x0 (Cons (t1, w1)) (Lew_cons (t1, w1))
(reflect t1 (Cons (t1, w1)) (Var_Hyp (w1, t1)))),(var_ne w1 (Arrow (t0, t1)) (wkn_var w w1 (Arrow (t0, t1)) h0 h)),(reify t0 w1 x))))

Obj.magic が現れているのは，論理述語の定義において，base と → ケースにおける式の型が異なる為である．Obj.magic が現れてはいるものの，CPS 変換された TDPE に等しいであろうことが見てとれる定義となっていることが分かる．

3

S/R

λcbv における TDPE の抽出
S/R

2 節を受けて，どのように λcbv における TDPE の抽出を行ったかを説明する．対馬らの call-byvalue の shift/reset 付き λ 計算における TDPE の定義は以下となっている．

7t ∈ Typev ∈ Valuee ∈ Expr:= b | t1 /α → t2 /β:= x | λx.v | v0 @ v1 | hvi | Sk.v:= x | λx.e | e0 @ e1 | hei | Sk.e

Reify ” ↓ ” : Type → Value → TLT↓base v:= v
A/a→B/b↓v := λx .Sk1 . h2 ↓b hlet v1 = (v @ ↑A x )in (↓a (S2 k.hlet x = (k1 @ ↓B v1 ) in k @ x i))i i2
Reify ” ↓ ” : Type → Expr → TLT↑base e:= e
↑A/r→B/r e := λv1 .Sk1 . ↑b S2 k.hlet x = (let x1 = (e @ ↓A v1 ) in h2 ↓a k1 @ ↑B x1 i2 ) in k @ x i
S と hi は 2 節でのケースと同様，let-insertion の定義の為の shift/reset である．又，S2 と h2 i2は，S と hi よりも一段階上の shift/reset となっている．よって，この TDPE から static な shift/reset
を外すには，まず S と hi を CPS 変換した後，さらに S2 と h2 i2 を CPS 変換する必要がある．そのようにして二回 CPS 変換をかけて，static な shift/reset をはずしたのが次の定義である：
Reify ” ↓ ” : Type → Value → TLT↓base v:= v
A/a→B/b↓v := λx1 .Sk1 .v @ (↓A x1 ) @ λv1 .λk2 .((λg  .k2 @ ↑a g  ) @ (k1 @ ↓B v1 ))@ λv2 . ↓b v2
Reify ” ↓ ” : Type → Expr → TLT↑base e:= e
↑A/r→B/r e := λv1 .λk1 .λk2 .((λg  .k2 @ ↑b g  ) @h(λx1 .k1 @ (↑B x1 ) @ (λv2 . ↓a v2 )) @ (e @ ↓A v1 )i)関数の型は 2 節にて示したモデルの型と同じである．k1 が continuation，k2 が meta continuationを表す変数となっている．このように CPS 変換を 2 回施して，2 階層の継続が出てくる形式を 2CPS
S/Rのプログラムと呼ぶ．このモデルを参考にして定式化を行っていく．λcbv のシステムや証明の定式化全てが λcbv のそれと全く同じ流れになっており，λcbv の定式化の拡張となっていることに注意さ
れたい．

3.1

S/R

λcbv の構文
S/R

まず λcbv の構文を定義する：

monomorphic type :polymorphic type :typm 3typp 3

A := base | A1 /A3 → A2 /A4
α := mono A | A1 →p A2

environment : world 3 w, Γ := list of typpvariable term :term :`v`t

33v := hyp | hyp’ | wkn(v)p := v | lam(p) | app(p1 , p2 ) | shift(p) | reset(p)monomorphic type の関数型 A1 /A3 → A2 /A4 においては，A1 型の式を受け取ると A2 型の式を返し，その実行に伴い継続の返す型 A3 を A4 へと変化させる様な関数の型である．polymorphic typeA1 →p A2 は ∀r, A1 /r → A2 /r を意味する関数型である．polymorphic type も定義している理由は，
completeness の証明において型の整合性をとる為に必要となるからである．又，hyp と hyp’ はそれ
ぞれ answer type が monomorophic と polymorphic であるような，（一番内側の binder で束縛されている）変数である．

8

term の推論規則は以下の如く定義する．e : w; a `t A; b とあるとき，term e の型が w; a `t A; bとなる．そしてこの型は，world w において A 型を持つ式 e を実行すると継続の返す型が a から bへと変化することを意味として持つ．
hyp : ∀r, (mono A, w; r `v A; r)hyp’ : ∀r, (A →p B, w; r `v A/a → B/a; r)v : w; a `v A; bv : w; a `v A; bwkn(v) : B, w; a `v A; bv : w; a `t A; b
p : w; r `t c/a → A/b; d q : w; b `t c; r
p : mono A, w; a `t B; blam(p) : ∀r, (w; r `t A/a → B/b; r)app(p, q) : w; a `t A; dp : A →p a, w; c `t c; b
p : w; a `t a; A
shift(p) : w; a `t A; b
reset(p) : ∀r, (w; r `t A; r)
そして本研究では，shift/reset 付 λ 計算における normal form と neutral term を以下の如く定めた：
normal form :neutral term :

`nf
`ne

3 nf := lam(shift(nf )) | ne
3 ne := v | app(ne, nf )| let(nf1 , app(ne, nf2 )) | let(nf , reset(ne))

normal form は neutral term 又は λ の直下に shift が入っている形の項であると定義した。lam(shift())
は，TDPE の結果の λ の直下に shift が入っている項を意味している．この λ と shift の関係に対する考え方は，shift/reset の通常の部分評価 [1] においても同様である．一方，neutral term は λcbvでの定義に加えて reset を let 文に残すものが入っている．これらの型規則を以下に示す．
p : w; a `nf A; bp : B →p a, mono A, w; c `nf c; b
p : w; a `ne A; bwkn(p) : B, w; a `nf A; b

p : w; a `ne A; bwkn(p) : B, w; a `ne A; blam(shift(p)) : ∀r, (w; r `nf A/a → B/b; r)

hyp : A, w; a `ne A; b

p : w; a `nf A; b

hyp : ∀r, (A →p B, w; r `ne A/a → B/a; r)

p : w; r `ne c/a → A/b; d q : w; b `nf c; rapp(p, q) : w; a `ne A; dp : mono c, w; a `nf A; b q : w; r0 `ne c0 /b → A/b0 ; rlet(p, app(q, q 0 )) : w; a `ne A; rp : mono c, w; a `nf A; rq 0 : w; b0 `nf c0 ; r0

q : w; a0 `nf a0 ; clet(p, reset(q)) : w; a `ne A; r

3.2

Soundness と Completeness の証明

2 節での soundness と completeness の証明と同様に，論理述語を用いて証明を行う．まずは，`を用いて monomorphic type と polymorphic type に関する論理述語をそれぞれ定義する．
2 (base):= ∀r, w; r ` base; r
Rw
2 (A) ⇒
2
Rw (A/a → B/b) := ∀w1 , ∀T1 , w ≤ w1 ⇒ Rw
1
2 (B) ⇒(∀w2 , ∀T, w1 ≤ w2 ⇒ Rw
2
2 (a) ⇒ ∀r, w ; r ` T ; r) ⇒(∀w3 , w2 ≤ w3 ⇒ Rw
3
3
∀r, w2 ; r ` T ; r) ⇒2 (b) ⇒ ∀r, w ; r ` T ; r) ⇒(∀w2 , w1 ≤ w2 ⇒ Rw
2
1
2
∀r, w1 ; r ` T1 ; r

2 (A)
Rw
3 (mono A)
Rw

2 (A/r → B/r)∀r, Rw
3 (A → B)Rwp

93 (α )) ∧ (R3 (α )) ∧ ... ∧ (R3 (α ))Rs2w ((α1 , α2 , ..., αn )) := (Rw
1
w 2
w n
2 (A/a → B/b) の二行目から四行目にかR2 の定義が 2CPS で書かれていることに注意されたい．Rw
けて括弧でくくられている式が continuation，五行目の式が meta continuation にそれぞれ対応している．この論理述語においても，2 節と同様にして，soundness を証明することが出来る．ここで≤ は，定理 1 の証明にて使用した定義と同じものを使うこととする．

公理 2 ∀w, ∀w0 , ∀A, ∀a, ∀b, w ≤ w0 ⇒ w; a ` A; b ⇒ w0 ; a ` A; b
補題 3 ∀w, ∀w0 , ∀Γ, ∀a, ∀b, w ≤ w0 ⇒ Rs2w (Γ) ⇒ Rs2w0 (Γ)

Proof. 公理 2 を用いる． 2
S/R

定理 3 (Soundness, λcbv )∀A, ∀a, ∀b, ∀Γ, ∀T, Γ; a `t A; b ⇒ ∀w,(Rs0w (Γ) ⇒2 (A) ⇒(∀w1 , ∀T1 , w ≤ w1 ⇒ Rw
1
2 (a) ⇒ ∀r, w ; r ` T ; r) ⇒(∀w2 , w1 ≤ w2 ⇒ Rw
2
1
2
∀r, w1 ; r ` T1 ; r) ⇒0 (b) ⇒ ∀r, w ; r ` T ; r) ⇒(∀w1 , w ≤ w1 ⇒ Rw
1
1
∀r, w; r ` T ; r)
Proof. Γ; a `t A; b における帰納法．
（補題 3 を使用する．
）2
これら補題・定理の証明は，ほとんどそのまま λcbv のそれを拡張しているだけである．
次に，TDPE を抽出する為の completeness を行う．まずは，上の論理述語の定義における ` を`nf に置き換える．
0 (base)Rw:= ∀r, w; r `nf base; r0
Rw (A/a → B/b) := ∀w1 , ∀T1 , w ≤ w1 ⇒ Rw1 (A) ⇒(∀w2 , ∀T, w1 ≤ w2 ⇒ Rw2 (B) ⇒(∀w3 , w2 ≤ w3 ⇒ Rw3 (a) ⇒ ∀r, w3 ; r `nf T ; r) ⇒∀r, w2 ; r `nf T ; r) ⇒(∀w2 , w1 ≤ w2 ⇒ Rw2 (b) ⇒ ∀r, w2 ; r `nf T1 ; r) ⇒∀r, w1 ; r `nf T1 ; r
0 (A)Rw
00 (mono A)
Rw

0 (A/r → B/r)∀r, Rw
00 (A → B)Rwp

00 (α )) ∧ (R00 (α )) ∧ ... ∧ (R00 (α ))Rs0w ((α1 , α2 , ..., αn )) := (Rw
1
w n
w 2

ここでの ≤ は以下の如く定義する．これは 2 節での completeness の証明に使用した ≤ を，
world の要素を二つまで増やしても 2 項関係が成立する様に拡張しただけである．この様に定義することによって，2 節ではカウンタをひとつ増やすだけであったのが，今回はカウンタを二つ増やす役割をも持たせている．

(i)∀A, w ≤ (A, w)(ii) ∀A, ∀B, w ≤ (A, B, w)
そして completeness の定義は以下の如くとなる．
10

S/R

定理 4 (Completeness, λcbv )0 (A) ⇒ ∀r, w; r `∀A, (i) ∀w, Rw
nf A; r0 (A)(ii) ∀w, ∀r, w; r `v A; r ⇒ Rw

Proof. A における帰納法．
（補題 2 を使用する．
）2
定理 4 の証明は，本節のはじめに示した TDPE のモデルを参考に，モデル定義にほぼ沿って証明を行うことが出来る．

3.3

TDPE の抽出

2 節と同様に，soundness と completeness の証明は，（shift/reset 付きにおける）CPS 変換と CPSの TDPE 一対一の関係にある．completeness の証明から得られた Coq 上の関数を 2 節と同様，型に関する帰納法の原理の展開と自明な β 簡約を行ったものが以下である．
Fixpoint reify (t : typ) : (forall w : world, R w t -> forall r : typ, nf w t r r) :=match t as t0 return (forall w : world, R w t0 -> forall r : typ, nf w t0 r r) with| base => (fun (w : world) (X : R w base) (r : typ) => X r)
| arrow t0 t1 t2 t3 => (fun (w : world) (X : R w (arrow t0 t1 t2 t3)) (r : typ) =>nf_LamShift w t0 t1 t2 t3 t3(X (arrowP t1 t2 :: mono t0 :: w) t3(lew_cons_2 (arrowP t1 t2) (mono t0) w)(reflect t0 (arrowP t1 t2 :: mono t0 :: w)(fun r0 : typ =>var_Wkn (mono t0 :: w) t0 (arrowP t1 t2) r0 r0(var_Hyp w t0 r0)))(fun (w2 : world) (T : typ)
(H : arrowP t1 t2 :: mono t0 :: w <== w2)(X0 : R w2 t1)(X1 : forall w3 : world,
w2 <== w3 -> R w3 t2 -> forall r0 : typ, nf w3 T r0 r0)(r0 : typ) =>nf_ne w2 T r0 r0(ne_LetApp w2 T r0 r0 r0 t2 r0 t1 r0 r0(X1 (mono t2 :: w2) (lew_cons_1 (mono t2) w2)(reflect t2 (mono t2 :: w2) (var_Hyp w2 t2)) r0)(ne_var w2 (arrow t1 t2 r0 r0) r0 r0(wkn_var H (var_Hyp2 (mono t0 :: w) t1 t2 r0 r0)))(reify t1 w2 X0 r0)))(fun (w2 : world) (_ : arrowP t1 t2 :: mono t0 :: w <== w2)(X0 : R w2 t3) (r0 : typ) => reify t3 w2 X0 r0)
t3)
r)
end
with reflect (t : typ) : (forall w : world, (forall r : typ, var w t r r) -> R w t) :=match t as t0 return (forall w : world, (forall r : typ, var w t0 r r) -> R w t0) with| base => (fun (w : world) (H : forall r : typ, var w base r r) (r : typ) =>nf_ne w base r r (var_ne (H r)))| arrow t0 t1 t2 t3 =>(fun(w : world)(H : forall r : typ, var w (arrow t0 t1 t2 t3) r r)
(w1 : world)(T1 : typ)(H0 : w <== w1)(X : R w1 t0)

11

(X0 : forall (w2 : world) (T : typ),w1 <== w2 ->R w2 t1 ->(forall w3 : world,
w2 <== w3 -> R w3 t2 -> forall r : typ, nf w3 T r r) ->forall r : typ, nf w2 T r r)
(X1 : forall w2 : world,
w1 <== w2 -> R w2 t3 -> forall r : typ, nf w2 T1 r r)
(r : typ) =>nf_ne w1 T1 r r(ne_LetReset w1 T1 r r t3 r t2
(X1 (mono t3 :: w1) (lew_cons_1 (mono t3) w1)(reflect t3 (mono t3 :: w1) (var_Hyp w1 t3)) r)(ne_LetApp w1 t2 t2 t2 t3 t1 t3 t0 t3 t3(X0 (mono t1 :: w1) t2 (lew_cons_1 (mono t1) w1)(reflect2 t1 (mono t1 :: w1) (var_Hyp w1 t1))
(fun (w3 : world) (_ : mono t1 :: w1 <== w3)(X2 : R w3 t2) (r0 : typ) => reify t2 w3 X2 r0) t2)(ne_var w1 (arrow t0 t1 t2 t3) t3 t3 (wkn_var H0 (H t3)))(reify t0 w1 X t3))))end.

nf_LamShift は normal form の定義における lam(shift( )) に，ne_LetApp と ne_LetReset は neutralterm の定義における let( , app( , )) と let( , reset( )) にそれぞれ対応している．又,var_Hyp2，mono，arrowP,arrow はそれぞれ hyp’，( →p )，( / → / ) を表している．lew_cons_1 と lew_cons_2
は，completeness の証明で使用した ≤ の (i) と (ii) にそれぞれ対応している．この関数定義においても，上述した CPS の shift/reset 付 TDPE と等しいであろうことが見てとれる．この関数をOCaml のプログラムとして抽出すると以下の如くとなる．
(** val reify : typ -> world -> r -> typ -> nf **)let rec reify t w x r0 =match t with
| Base -> Obj.magic x r0
| Arrow (t0, t1, t2, t3) ->Nf_LamShift (w, t0, t1, t2, t3, t3,(Obj.magic x (Cons ((ArrowP (t1, t2)), (Cons ((Mono t0), w)))) t3(Lew_cons_2 ((ArrowP (t1, t2)), (Mono t0), w))(reflect t0 (Cons ((ArrowP (t1, t2)), (Cons ((Mono t0), w))))(fun r1 -> Var_Wkn ((Cons ((Mono t0), w)), t0, (ArrowP (t1, t2)),
r1, r1, (Var_Hyp (w, t0, r1)))))(fun w2 t4 h x0 x1 r1 ->Nf_ne (w2, t4, r1, r1,
Ne_LetApp (w2, t4, r1, r1, r1, t2, r1, t1, r1, r1,
x1 (Cons ((Mono t2), w2)) (Lew_cons_1 ((Mono t2), w2))(reflect2 t2 (Cons ((Mono t2), w2))
(fun x2 -> Var_Hyp (w2, t2, x2)))
r1,
Ne_var (w2, (Arrow (t1, t2, r1, r1)), r1, r1,
wkn_var (Cons ((ArrowP (t1, t2)), (Cons ((Mono t0), w))))
w2 h (Arrow (t1, t2, r1, r1)) r1 r1(Var_Hyp2 ((Cons ((Mono t0), w)), t1, t2, r1, r1))),
reify t1 w2 x0 r1)))(fun w2 x0 x1 r1 -> reify t3 w2 x1 r1)
t3),
r0)

12

(** val reflect : typ -> world -> (typ -> var) -> r **)and reflect t w h =match t with
| Base ->Obj.magic (fun r0 ->Nf_ne (w, Base, r0, r0, (var_ne w Base r0 r0 (h r0))))| Arrow (t0, t1, t2, t3) ->Obj.magic (fun w1 t4 h0 x x0 x1 r0 ->Nf_ne (w1, t4, r0, r0,
Ne_LetReset (w1, t4, r0, r0, t3, r0, t2,
x1 (Cons ((Mono t3), w1)) (Lew_cons_1 ((Mono t3), w1))
(reflect t3 (Cons ((Mono t3), w1))
(fun x2 -> Var_Hyp (w1, t3, x2)))
r0,
Ne_LetApp (w1, t2, t2, t2, t3, t1, t3, t0, t3, t3,
x0 (Cons ((Mono t1), w1)) t2 (Lew_cons_1 ((Mono t1), w1))
(reflect t1 (Cons ((Mono t1), w1))
(fun x2 -> Var_Hyp (w1, t1, x2)))(fun w3 x2 x3 r1 -> reify t2 w3 x3 r1)
t2,
Ne_var (w1, (Arrow (t0, t1, t2, t3)), t3, t3,
wkn_var w w1 h0 (Arrow (t0, t1, t2, t3)) t3 t3 (h t3)),
reify t0 w1 x t3))))

ここでも Obj.magic が現れる理由は，2 節でのそれと同じである．しかしこの事を除けば CPS の
shift/reset 付 TDPE と同一の構造をしていること，そして [6] にて提示された shift/reset 付 TDPEとは全く異なる構造をしていることがみてとれる．

4

まとめと今後の課題

本研究では call-by-value の λ 計算における TDPE の抽出を定式化し，その方法を拡張する形で
call-by-value の shift/reset 付 λ 計算における TDPE を抽出した．定式化にあたっては，shift/reset付き λ 計算における normal form，neutral term の構造を提示した．抽出されたプログラムは複雑にはなっていたものの，[8] によって提示された shift/reset 付 TDPE を CPS 変換したプログラムと同一であろうことがみてとれた．
completeness の証明に対応する TDPE は CPS で書かれており，入力として CPS された termを受け取る．一方，soundness の証明からは CPS 変換を得られる．そうすると，soundness の証明の継続に completeness の証明の前半部分を入れる形で両者を合成すると，直接形式の入力を受け取り，その正規形を返す形の TDPE が得られる可能性がある．単純に関数合成したのでは CPS 変換
部分で入力の構文についての場合分けが入るので TDPE とは言いがたいが，両者を fusion などの手法を使って合成出来れば直接形式の TDPE を得られる可能性もある．この検討が今後の課題である．

謝辞
種々の有益なコメントを下さった査読者の方々に感謝いたします．

13

参考文献
[1] Asai, K. “Logical Relations for Call-by-value Delimited Continuations,” Trends in Functional Programming (TFP 2005), Vol. 6, pp. 63–78, Intellect (2007).
[2] Coquand, C. “A Formalised Proof of the Soundness and Completeness of a Simply Typed LambdaCalculus with Explicit Substitutions” Higher-Order and Symbolic Computation, Volume 15, Issue 1,
pp. 57-90 (March 2002).
[3] Danvy, O. “Type-Directed Partial Evaluation,” Conference Record of the 23rd Annual ACM Symposium on Principles of Programming Languages, pp. 242–257 (January 1996).
[4] Filinski, A. “Normalization by Evaluation for the Computational Lambda-Calculus,” In S. Abramsky,
editor, Typed Lambda Calculi and Applications (LNCS 2044), pp. 151–165 (May 2001).
[5] Ilik, D. “Continuation-passing style models complete for intuitionistic logic”, Annals of Pure andApplied Logic, Special issue: Classical logic and computation 2010.
[6] Ilik, D. “A formalized type-directed partial evaluator for shift and reset”, http://arxiv.org/abs/
1210.2094.
[7] Pierce, B. C. Types and Programming Languages, Cambridge: MIT Press (2002).
[8] Tsushima, K., and K. Asai “Towards Type-Directed Partial Evaluation for Shift and Reset,” Proceedings of the 2009 Workshop on Normalization by Evaluation, pp. 57–64 (August 2009).

14