論理関係による shift/reset の部分評価器の正当性の証明
横関 茉衣, 浅井 健一
お茶の水女子大学{yokozeki.mai, asai}@is.ocha.ac.jp
概要
部分評価器は static な計算と dynamic な計算に分けられたプログラムを受け取り、static な計算のみを実行した結果のプログラムを返す。部分評価器の正当性を証明するためには、プログラムの意味が変換前と変換後で変わらないということを証明する。この証明を添えて shift/reset の部分評価器の定義を提案した研究がある。しかし、その正当性の証明は継続の引数の項を値でないのに値であるとして扱っている部分があった。この証明の誤りは、部分評価器が正しくないこと、つまりは変換前に存在していた dynamic な eﬀect が変換後には消えてしまうことに繋がっていた。そこで本研究は、let-insertion を用いて dynamic な eﬀect が消えることを防ぐように部分評価器を変更し、その新しい部分評価器に対して正当性の証明を行った。

1

はじめに

部分評価とは、プログラムと一部の入力データを受け取ったら、その入力データのみに依存する部分を先に計算してしまった残余プログラム (residual program) を出力するようなプログラム変換である。残りの入力データで残余プログラムを実行したとき得られる結果は、全ての入力デー
タで元のプログラムを実行した時に得られる結果と等しい [7]。部分評価は最適化手法のひとつであり、近年においてもドメイン固有言語の開発において部分評価を取り入れてより高速なプログ
ラムを生成する取り組みが行われている [10]。
部分評価の理論は活発に研究されていた歴史があり、研究の成果の一つとして Asai による
shift/reset の部分評価器 [2, 1] がある。Asai は shift/reset [5] で拡張した値呼びの λ 計算に対するオフライン部分評価器を定義した。オフライン部分評価器とは束縛時解析が済んだプログラ
ムを特化するものである。つまり、オフライン部分評価器は static な計算と dynamic な計算に分けられたプログラムを受け取り、static な計算のみを実行した結果のプログラムを返す。このようにオフライン部分評価器はコンパイラと同じようにプログラム変換器であるが、プログラム変換器はプログラムの意味が変換前と変換後で変わらないことに責任を持つべきである。そこで Asai
は部分評価器の定義とともに、論理関係という技法を使い、定義した部分評価器の正当性を証明した。構造的帰納法では高階関数が適用されるときの挙動を特徴づけることが難しいが、論理関係を使うと型の助けを借りて高階関数の性質を捉えることができる。しかし、部分評価器の正当性の証明を読み直したところ、証明には誤りがあることがわかり、そして部分評価器そのものも正しくないことがわかった。
本研究では、shift/reset の部分評価器の正当性の証明 [2, 1] に見つかった誤りを説明し、部分評価器が正しくないことを説明した上で、新たに部分評価器を定義する。さらに新たに定義した
部分評価器に対して正当性の証明を行う。正当性の誤りは継続の引数の項を値でないのに値であるとして扱っている部分にある。この証明の誤りは、部分評価器が正しくないこと、つまりは変換前に存在していた dynamic な eﬀect が変換後には消えてしまうことに繋がっていた。そこで本1

研究は、let-insertion を用いて dynamic な eﬀect が消えることを防ぐように部分評価器を変更し、その新しい部分評価器に対して正当性の証明を行った。
関連研究として、shift/reset の多段階計算 [9]、shift0/reset0 の多段階計算 [11] がある。多段階
計算は部分評価と同じように特化によりプログラムを最適化するが、多段階計算はコードを変数に束縛したり、コードをコードに埋め込むことなどができ、自由度が高い。また、生成されるコー
ドが型安全であることが保証されているという利点もある。一方で部分評価は、多段階計算と比較して自由度は低いが、元のプログラムと生成するプログラムで意味が変わらないため、そのま
まコンパイラの最適化に使用できるなどの利点がある。また、論理関係を使った証明についての関連研究として、Biernacka と Biernacki [3] による abortive な継続演算子で拡張した型付きラムダ計算に対する停止性の証明を値呼びと名前呼びの両方の体系に対して行った研究がある。本稿と同様に、項の論理関係と同時に継続の論理関係を定義している。
OCaml 5 に代数的エフェクトが導入されるなど限定継続を明示的に扱ったプログラムが増えてきている。そのようなプログラムの効率的な実行には、限定継続命令の最適化が欠かせない。しかし、限定継続命令の最適化は複雑で注意を要する。特に細かい議論をきちんとしないと間違った最適化を行うことになる。実際、最適化のひとつである先行研究の shift/reset の部分評価 [2, 1]
は間違っていることがわかった。本稿ではその原因を十分に究明して、その間違いを正す。そして、正しい最適化に貢献することを目指す。

1.1

本稿の構成

2 節では本稿全体で使用するメタ言語の説明などの準備を行う。3 節では 4 節の前段階として λ計算の部分評価器を概説する。4 節では先行研究 [2, 1] の shift/reset の部分評価器を概説し、さらにその型システムと正当性を証明する定理（本稿で誤りだったことが示されたもの）を述べる。5
節では 4 節の部分評価器の正当性の証明に見つかった誤りと、部分評価器そのものに見つかった
誤りを述べる。6 節では 5 節の部分評価器の誤りが修正された部分評価器を定義する。7 節では 6
節の新しい部分評価器の正当性の証明を行う。8 節ではまとめと今後の課題を述べる。

2

準備

2.1

メタ言語の定義

部分評価器は、直接形式でメタ言語の shift/reset を使って定義する。そのため、メタ言語は
left-to-right の値呼びの λ 計算を shift/reset とデータ型の構成子で拡張したものとする。メタ言語の構文は次のように表される。通常、メタ言語を表す際は M を用いるが、継続の body 部分を表す際は K を用いる。
M, K ::= x | λx. M | M M | ξk. M | ⟨M ⟩ | n | M + 1 |Var(n) | Lam(n, M ) | App(M, M ) | Shift(n, M ) | Reset(M ) |Lam(n, M ) | App(M, M ) | Shift(n, M ) | Reset(M ) |Lam(n, M ) | App(M, M ) | Shift(n, M )ξk. M は shift、⟨M ⟩ は reset を表す。データ型の構成子は、部分評価器への入出力項と、束縛時解析前の元のプログラムの項を表現する。上線が付いた構成子は入力項の static な項を、下線が付いた構成子は入力項の dynamic な項を表す。線が付いていない構成子は部分評価器の出力項と束縛時解析前の元のプログラムの項を表す。また、部分評価器の入出力となるプログラムの言語において、変数は自然数 n で表現する。そのため、このメタ言語には自然数と 1 を加算する演算子がある。
2

部分評価器が出力のプログラムを作成するとき、新しい変数を生成する。出力項において、deBruijn レベル [6] を使う。de Bruijn レベルは de Bruijn インデックスとは反対にラムダ束縛子に対して外から内へ番号を振る。そのため、例えば λx. (λy. xy) x は de Bruijn レベルでは λ. (λ. 01) 0となる。部分評価器の出力のプログラムを名前のついた変数を使って表すために、以下を定義する。

var(m)lam(f )
app(f1 , f2 )shift(f )reset(f )let(f1 , lam(f2 ))

=
=
=
=
=
=

λn. Var(m)λn. Lam(n, f (n + 1))
λn. App(f1 n, f2 n)
λn. Shift(n, f (n + 1))
λn. Reset(f n)app(lam(f2 ), f1 )let(f1 , lam(f2 )) は app(lam(f2 ), f1 ) の略記となっており、部分評価器の定義で利用される。この定義を使って表された項 M を具体的な項に変換するための操作として ↓n M を使う。↓n M = M nである。例えば、↓3 M は M の最も外側の束縛子に 3 を振り、その一つ内側の束縛子に 4 を振る
ため、↓3 (lam(λx. lam(λy. app(var(x), var(y)))))= Lam(3, Lam(4, App(Var(3), Var(4))))となる。
メタ言語の値は次のように表される。

V

2.2::= x | λx. M | n |Var(n) | Lam(n, V ) | App(V, V ) | Shift(n, V ) | Reset(V ) |Lam(n, V ) | App(V, V ) | Shift(n, V ) | Reset(V ) |Lam(n, V ) | App(V, V ) | Shift(n, V )メタ言語の項間の等価性を表す記号

メタ言語の項間の等価性を表す記号については、定義または α 同値を表す際は =、以下のKameyama と Hasegawa [8] の shift/reset の公理による項間の等価性を表す際は ∼ を用いる。

2.2.1

shift/reset の公理

Pure な評価文脈を下記の通り定義する。
F= []|FM |VF |Lam(x, F ) | App(F, M ) | App(V, F ) | Shift(k, F ) | Reset(F ) |Lam(x, F ) | App(F, M ) | App(V, F ) | Shift(k, F ) | Reset(F ) |Lam(x, F ) | App(F, M ) | App(V, F ) | Shift(k, F )これは、hole [ ] がメタ言語の reset では囲まれていないような評価文脈である。Kameyama とHasegawa [8] による、shift/reset で拡張された λ 計算における公理のうち本稿で使用するものは下記の通りである。

(λx. M ) V(λx. F [x]) M⟨V ⟩⟨F [ξk. M ]⟩

∼
∼
∼
∼

M [V /x]F [M ]
if x ̸∈ FV(F )V⟨(λk. M ) (λx. ⟨F [x]⟩)⟩ if x ̸∈ FV(F )

3

βv
βΩ
reset-value
reset-shift

継続とは
継続とは、プログラムを実行している最中における「残りの計算」である。例えば、1 + 2 ∗ 3という式の実行において、2 ∗ 3 を計算しようとしている際の継続は「2 ∗ 3 の結果を受け取り、それに １ を加える」となる。

shift/reset とは
shift/reset[5] とは限定継続、つまり限定された継続をプログラム中で扱うための演算子の一種である。reset で継続を区切り、shift で区切られた継続を取り除いて変数に束縛して利用する。本稿では reset を ⟨M ⟩ と書き、継続を ⟨⟩ の位置で区切る。shift を ξk. M と書き、その時点の継続を取り除いて変数 k に束縛して M を実行する。例えば、3 + ⟨2 + ξk. k (k 5)⟩ は以下のように実行される。shift/reset の正確な意味論は、通常 CPS インタプリタまたは CPS 変換によって与えられる。
3 + ⟨2 + ξk. k (k 5)⟩; 3 + ⟨(k (k 5))[λv. ⟨2 + v⟩/k]⟩; 3 + ⟨(k 7)[λv. ⟨2 + v⟩/k]⟩
; 3+9
; 12
ξk. k (k 5) を計算しようとするとき、reset によって区切られた継続は 2 + [·] である。そのため shiftの実行によりその継続が取って来られ、k に λv. ⟨2 + v⟩ が束縛される。

3

λ 計算の部分評価器

left-to-right の値呼びの λ 計算に対する部分評価器は以下のように定義される。ρ は部分評価時の環境である。基本的には、static な入力はインタプリタと同じように実行し、dynamic な入力
はコードに残している。
P 1 [[Var(n)]] ρP 1 [[Lam(n, W )]] ρP 1 [[Lam(n, W )]] ρP 1 [[App(W1 , W2 )]] ρP 1 [[App(W1 , W2 )]] ρ

=
=
=
=
=

ρ (n)
λx. P 1 [[W ]] ρ[x/n]lam(λx. ⟨P 1 [[W ]] ρ[var(x)/n]⟩)(P 1 [[W1 ]] ρ) (P 1 [[W2 ]] ρ)ξk. let(app(P 1 [[W1 ]] ρ, P 1 [[W2 ]] ρ), lam(λt. k (var(t))))dynamic な関数呼び出しの特化において、let-insertion [4] を行っている。let-insertion を行わなければ、部分評価器の正当性は言えない。dynamic な関数呼び出しの特化がP 1 [[App(W1 , W2 )]] ρ = app(P 1 [[W1 ]] ρ, P 1 [[W2 ]] ρ)と定義されていた場合を考える。このときに部分評価器が正しくない動作をする例として例 1 を見る。Wdiverge は Mdiverge を、W は M を束縛時解析したものとなっている。
例 1.

W
M
Wdiverge
Mdiverge= App(Lam(x, Lam(y, Var(y))), Wdiverge )= App(Lam(x, Lam(y, Var(y))), Mdiverge )λ 式の表記： (λx. λy. y) Mdiverge= App(Lam(x, App(Var(x), Var(x))), Lam(x, App(Var(x), Var(x))))= App(Lam(x, App(Var(x), Var(x))), Lam(x, App(Var(x), Var(x))))λ 式の表記： (λx. x x) (λx. x x)
4

P 1 [[W ]] ρ を計算すると、P 1 [[Wdiverge ]] ρ の周りの継続が P 1 [[Wdiverge ]] ρ の結果を捨てるため、
lam(λy. var(y)) となる。一方で、Mdiverge は発散する項のため、M はインタプリタで評価すると発散する。
Wdiverge に dynamic な入出力、副作用、例外などの他の eﬀect が入っていた場合も同様に、変換前に存在していた eﬀect が変換後には消えてしまう結果となる。部分評価器が正しいということは、プログラムの意味が変換前と変換後で変化しないことである。変換前に存在していた eﬀect
が変換後には消えてしまう場合は部分評価器が正しくない。
Wdiverge の dynamic な関数呼び出しのように、dynamic な関数呼び出しは停止しない dynamic
な計算を作っている可能性があり、let-insertion で出力項に残留されなければならない。
そこで dynamic な関数呼び出しの特化では、そのときの継続 k を shift で捉えた上で、関数呼び出しを残留させ、それを t という変数に束縛し、継続 k に t を渡している。
P 1 [[App(W1 , W2 )]] ρ = ξk. let(app(P 1 [[W1 ]] ρ, P 1 [[W2 ]] ρ), lam(λt. k (var(t))))
これにより、継続 k が引数を捨ててしまうような継続だったとしても、dynamic な関数呼び出しは出力されるプログラムに残る。例 1 の W 部分評価では、Wdiverge の 3 つの dynamic な関数呼び出しが let-insertion により残留し、以下のような出力項を得る。

reset(let(app(lam(λx2 . reset(let(app(var(x2 ), var(x2 )), λt2 . var(t2 )))),lam(λx3 . reset(let(app(var(x3 ), var(x3 )), λt3 . var(t3 ))))),
λt1 . lam(λy1 . var(y1 ))))
λ 式の表記： ⟨let t1 = ((λx2 . ⟨let t2 = x2 x2 in t2 ⟩) (λx3 . ⟨let t3 = x3 x3 in t3 ⟩)) in λy1 . y1 ⟩4Asai による shift/reset の部分評価器 [2, 1]

4.1

部分評価器

left-to-right の値呼びの shift/reset に対する部分評価器も、基本的には λ 計算に対する部分評
価器と同じ考え方で定義される。
P 2 [[Var(n)]] ρ = ρ (n)P 2 [[Lam(n, W )]] ρ = λx. P 2 [[W ]] ρ[x/n]P 2 [[Lam(n, W )]] ρ = lam(λx. shift(λk. ⟨reset(app(var(k), P 2 [[W ]] ρ[var(x)/n]))⟩))
P 2 [[App(W1 , W2 )]] ρ = (P 2 [[W1 ]] ρ) (P 2 [[W2 ]] ρ)
P 2 [[App(W1 , W2 )]] ρ = ξk. reset(let(app(P 2 [[W1 ]] ρ, P 2 [[W2 ]] ρ), lam(λt. k (var(t)))))
P 2 [[Shift(n, W )]] ρ = ξk. P 2 [[W ]] ρ[k/n]P 2 [[Shift(n, W )]] ρ = ξk. P 2 [[W ]] ρ[lam(λv. ⟨k (var(v))⟩)/n]
P 2 [[Reset(W )]] ρ = ⟨P 2 [[W ]] ρ⟩
ただし、特化している最中の継続と、束縛時解析前の元のプログラムを実行している最中の継続の間の整合性が保たれるように書かれている。特に dynamic な関数の特化にはそのための工夫が施されている。
dynamic な関数の特化がP 2 [[Lam(n, W )]] ρ = lam(λx. ⟨P 2 [[W ]] ρ[var(x)/n]⟩)と定義されていたときを考える。W に static な shift があった場合、その static な shift を特化しようとすると、shift で補足する継続は特化の最中に分からないという状態に陥る。そのため、dynamic な関数の body 部分の static な shift を特化できなくなってしまう。

5そこで、特に dynamic な関数 Lam(n, W ) を特化する際には、入力を Lam(n, Shift(k, App(k, W )))ととらえ、出力されるコードの継続 k を明示した上で、その継続の下で W を特化している。
（詳
しくは [2] を参照。）このようにすることで、入力の reset は常に static に処理できるようになるとともに、特化時に static に shift をすると、常に正しい継続を取ることができるようになって
いる。

4.2

型システム

型は以下のように定義される。

τ= d | τ /τ → τ /τd は dynamic であること表し、τ /τ → τ /τ は static な関数であることを表す。
型システムは以下のように定義される。これは束縛時解析を兼ねていて A, α ⊢ M : τ, β [W ] の前半部分は「型環境 A の下で（上線や下線のない入力の）項 M は τ 型を持ち、answer type を α か
ら β に変化させる」ことを意味する。さらに束縛時解析の結果 M は W のように static/dynamicに区分されることを示す。
A[n : τ ], α ⊢ Var(n) : τ, α [Var(n)]A[n : σ], α ⊢ M : τ, β [W ]A, δ ⊢ M1 : σ/α → τ /ϵ, β [W1 ]A, ϵ ⊢ M2 : σ, δ [W2 ]A, δ ⊢ Lam(n, M ) : σ/α → τ /β, δ [Lam(n, W )]A, α ⊢ App(M1 , M2 ) : τ, β [App(W1 , W2 )]A[n : τ /δ → α/δ], σ ⊢ M : σ, β [W ]A, σ ⊢ M : σ, τ [W ]A, α ⊢ Shift(n, M ) : τ, β [Shift(n, W )]A, α ⊢ Reset(M ) : τ, α [Reset(W )]A[n : d], d ⊢ M : d, d [W ]A, δ ⊢ Lam(n, M ) : d, δ [Lam(n, W )]A, δ ⊢ M1 : d, β [W1 ] A, d ⊢ M2 : d, δ [W2 ]A, d ⊢ App(M1 , M2 ) : d, β [App(W1 , W2 )]A[n : d], σ ⊢ M : σ, β [W ]A, d ⊢ Shift(n, M ) : d, β [Shift(n, W )]static な項の型付け規則に関しては、単純型付きの λ 計算と同じである。一方、dynamic な項の型付け規則では、dynamic な型は一括して d としている。すなわち、dynamic な項は untyped
であり、停止しない項も型がつく。

4.3

インタプリタ

正当性の証明で必要となるインタープリタは以下のように定義される。

I [[Var(n)]] ρI [[Lam(n, M )]] ρI [[App(M1 , M2 )]] ρI [[Shift(n, M )]] ρI [[Reset(M )]] ρ

=
=
=
=
=

6

ρ (n)
λx. I [[M ]] ρ[x/n](I [[M1 ]] ρ) (I [[M2 ]] ρ)
ξk. I [[M ]] ρ[k/n]⟨I [[M ]] ρ⟩

4.4

shift/reset の部分評価器の正当性の証明

値呼びのメタ言語の項間の論理関係 [12] を型の構造に対する帰納法により、以下のように定義する。
(M, M ′ ) ∈ Rd⇐⇒ I [[↓n M ]] ρid ∼ M ′ （n は十分に大きい）(M, M ′ ) ∈ Rσ/α→τ /β ⇐⇒ ∀(V, V ′ ) ∈ Rσ . ∀(λv. K, λv ′ . K ′ ) |= τ ; α.
(⟨(λv. K) (M V )⟩, ⟨(λv ′ . K ′ ) (M ′ V ′ )⟩) ∈ Rβ
ここで、ρid (n) は任意の n に対して ρid (n) = zn と定義する。これは部分評価器の出力項ある
いは束縛時解析前の元のプログラムの自由変数と、メタ言語の自由変数を関係付けるものである。
前者の自由変数が Var(n) のとき、後者の関係付けられる自由変数を zn と表す。この論理関係は
開いた項も対象に定義しているため、このような関係付けが必要となる。
また、M は自由変数を持つ可能性があるため、Rd の定義における n は M に現れる自由変数の整数より大きい必要がある。
そして、(λv. K, λv ′ . K ′ ) |= τ ; α は以下のように定義する。

(λv. K, λv ′ . K ′ ) |= τ ; α ⇐⇒ ∀(V, V ′ ) ∈ Rτ . (⟨(λv. K) V ⟩, ⟨(λv ′ . K ′ ) V ′ ⟩) ∈ Rα
論理関係は再帰的に定義されているが、型に関する再帰的な定義となっており、定義の右辺に現れる型は元の型より小さくなっている。
また、簡単のため対象言語とメタ言語では base type を省いているが、例えば int 型を追加する
場合は、型の定義に static な int 型を加え、以下のように static な int 型の論理関係の定義を追加する。
(M, M ′ ) ∈ Rint ⇐⇒ M ∼ M ′このようにして定義された論理関係を使い、先行研究 [2, 1] では以下の言明が定理として述べられていた。5 節で見る通り、部分評価器 P 2 は正しくないため、部分評価器 P 2 を使ったこの言明は成り立たない。
先行研究 [2, 1] では定理とされていた言明. A, α ⊢ M : τ, β [W ] かつ (ρ, ρ′ ) |= A かつ
(λv. K, λv ′ . K ′ ) |= τ ; α ならば (⟨(λv. K) (P 2 [[W ]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[M ]] ρ′ )⟩) ∈ Rβ .
ここで (ρ, ρ′ ) |= A は、(ρ, ρ′ ) |= A ⇐⇒ 任意の n ∈ dom(A) について (ρ (n), ρ′ (n)) ∈ RA(n) と定義する。ただし、dom(A) は A の定義域。
この言明の継続を初期継続にし、環境を空にすると、部分評価器の正当性を示す言明が得られる。しかしこの言明もまた、先行研究では系とされていたが、P 2 を使っているため成り立たない。
先行研究 [2, 1] では系とされていた言明.
⟨I [[M ]] ∅⟩.

d ⊢ M : d, d [W ] ならば I [[↓0 ⟨P 2 [[W ]] ∅⟩]] ρid ∼5

shift/reset の部分評価器 [2, 1] の正当性の誤り

5.1

正当性の証明の誤り

Asai による shift/reset の部分評価器の正当性の証明 [2] は、A ⊢ M : τ [W ] の証明の構造に沿った帰納法によるものである。A ⊢ M : τ [W ] に対して適用される型規則は 7 通りであるため、証明は 7 つの場合分けからなる。このうち、static な reset の場合と static な shift の場合において、証明に誤りがあった。この二つの誤りはどちらも、継続の引数の項を値でないのに値であるとして扱っているという誤りである。
7

5.1.1static な reset

static な reset の場合は以下のように証明されていた。補題 1、補題 2 は 7.1 節で定義されている。
(Static Reset)

A, σ ⊢ M : σ, τ [W ]A, α ⊢ Reset(M ) : τ, α [Reset(W )]が成り立っている。示したいのは、(ρ, ρ′ ) |= A かつ (λv. K, λv ′ . K ′ ) |= τ ; α ならば(⟨(λv. K) (P 2 [[Reset(W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Reset(M )]] ρ′ )⟩) ∈ Rαである。 P 2 と I の定義と補題 1 より、(⟨(λv. K) (P 2 [[Reset(W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Reset(M )]] ρ′ )⟩) ∈ Rα⇐⇒ (⟨(λv. K) ⟨P 2 [[W ]] ρ⟩⟩, ⟨(λv ′ . K ′ ) ⟨I [[M ]] ρ′ ⟩⟩) ∈ Rα⇐⇒ (⟨(λv. K) ⟨(λx. x) (P 2 [[W ]] ρ)⟩⟩, ⟨(λv ′ . K ′ ) ⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩⟩) ∈ Rα(λv. K, λv ′ . K ′ ) |= τ ; α より(⟨(λx. x) (P 2 [[W ]] ρ)⟩, ⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩) ∈ Rτを示せばよい。これは補題 2 から (λx. x, λx′ . x′ ) |= σ ; σ が成り立つため、帰納法の仮定より成り立つ。
この赤文字の部分が誤りであった。4.4 節でも定義した通り、(λv. K, λv ′ . K ′ ) |= τ ; α かつ
(V, V ′ ) ∈ Rτ ならば (⟨(λv. K) V ⟩, (λv ′ . K ′ ) V ′ ) ∈ Rα である。つまり、⟨(λx. x) (P 2 [[W ]] ρ)⟩ と⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩ が値ならば、赤文字の部分は正しい。
しかし、⟨(λx. x) (P 2 [[W ]] ρ)⟩ と ⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩ は値ではなく、さらには ⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩が正規化可能であるとは限らない。なぜならば全ての dynamic な項の型は d であるため、例えば
Wdiverge = App(Lam(x, App(Var(x), Var(x))), Lam(x, App(Var(x), Var(x))))λ 式の表記： (λx. x x) (λx. x x)といった発散する項も型がつく。そのため、⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩ の M は発散する項である可能性があり、⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩ が正規化可能であるとは限らない。

5.1.2

static な shiftstatic な shift の場合は以下のように証明されていた。補題 1、補題 2 は 7.1 節で定義されている。
(Static Shift)

A[n : τ /δ → α/δ], σ ⊢ M : σ, β [W ]A, α ⊢ Shift(n, M ) : τ, β [Shift(n, W )]が成り立っている。示したいのは、(ρ, ρ′ ) |= A かつ (λv. K, λv ′ . K ′ ) |= τ ; α ならば(⟨(λv. K) (P 2 [[Shift(n, W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Shift(n, M )]] ρ′ )⟩) ∈ Rβである。補題 1 と、⟨(λv. K) (P 2 [[Shift(n, W )]] ρ)⟩= {deﬁnition of P 2 }⟨(λv. K) (ξk. P 2 [[W ]] ρ[k/n])⟩∼ {reset-shift}⟨(λk. P 2 [[W ]] ρ[k/n]) (λa. ⟨(λv. K) a⟩)⟩∼ {βv }
⟨P 2 [[W ]] ρ[λa. ⟨(λv. K) a⟩/n]⟩∼ {βΩ }⟨(λx. x) (P 2 [[W ]] ρ[λa. ⟨(λv. K) a⟩/n])⟩

8

と

=
∼
∼
∼

⟨(λv ′ . K ′ ) (I [[Shift(n, M )]] ρ′ )⟩{deﬁnition of I}⟨(λv ′ . K ′ ) (ξk. I [[M ]] ρ′ [k/n])⟩{reset-shift}⟨(λk. I [[M ]] ρ′ [k/n]) (λa′ . ⟨(λv ′ . K ′ ) a′ ⟩)⟩{βv }⟨I [[M ]] ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n]⟩{βΩ }⟨(λx′ . x′ ) (I [[M ]] ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n])⟩から(⟨(λv. K) (P 2 [[Shift(n, W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Shift(n, M )]] ρ′ )⟩) ∈ Rβ⇐⇒ (⟨(λx. x) (P 2 [[W ]] ρ[λa. ⟨(λv. K) a⟩/n])⟩, ⟨(λx′ . x′ ) (I [[M ]] ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n])⟩) ∈ Rβを示せば良い。補題 2 から (λx. x, λx′ . x′ ) |= σ ; σ であるから、(ρ[λa. ⟨(λv. K) a⟩/n], ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n]) |= A[n : τ /δ → α/δ]すなわち(λa. ⟨(λv. K) a⟩, λa′ . ⟨(λv ′ . K ′ ) a′ ⟩) ∈ Rτ /δ→α/δ .
が成り立てば、帰納法の仮定より証明が終わる。
そのためには任意の (V, V ′ ) ∈ Rτ と (λu. L, λu′ . L′ ) |= α ; δ について(⟨(λu. L) ⟨(λv. K) V ⟩⟩, ⟨(λu′ . L′ ) ⟨(λv ′ . K ′ ) V ′ ⟩⟩) ∈ Rδを示せばよい。これは、(λv. K, λv ′ . K ′ ) |= τ ; α であるため成り立つ。
この赤文字の部分が誤りであった。4.4 節でも定義した通り、(λu. L, λu′ . L′ ) |= α ; δ かつ
(V, V ′ ) ∈ Rα ならば (⟨(λu. L) V ⟩, (λu. L′ ) V ′ ) ∈ Rδ である。つまり、⟨(λv. K) V ⟩ と ⟨(λv ′ . K ′ ) V ′ ⟩が値ならば、赤文字の部分は正しい。しかし、⟨(λv. K) V ⟩ と ⟨(λv ′ . K ′ ) V ′ ⟩ は値ではなく、さらには ⟨(λv ′ . K ′ ) V ′ ⟩ が正規化可能であるとは限らない。そのため、例えば λv ′ . K ′ が λv ′ . I [[M ]] ρ′と表せて M が発散する項だった場合、⟨(λv ′ . K ′ ) V ′ ⟩ は発散する。つまり ⟨(λv ′ . K ′ ) V ′ ⟩ が正規化可能であるとは限らない。

5.2

部分評価器の正当性の誤り

5.1 節の通り部分評価器の正当性の証明に誤りがあったが、実は証明しようとしていたもの、つまり部分評価器そのものが正当ではなかった。部分評価器の入力項に dynamic な eﬀect が含まれていた場合、その eﬀect が出力項では消滅しているケースがあり、その場合は部分評価器が正しくない。eﬀect が部分評価により消滅するケースは、5.1 節の正当性の証明が破綻するケースと対応しており、static な reset に由来するものと static な shift に由来するものがある。
5.2.1

static な reset

5.1.1 節で説明した通り、(⟨(λv. K) (P 2 [[Reset(W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Reset(M )]] ρ′ )⟩) ∈ Rαの証明が破綻するのは、⟨I [[M ]] ρ′ ⟩ が発散するときである。そのような場合の例として例 2 を考える。I [[M2 ]] ρ′ の計算において、⟨I [[Mdiverge ]] ρ′ ⟩ は発散する。W2 は M2 を束縛時解析したものである。また、Wdiverge と Mdiverge は例 1 と同じである。

9

例 2.

W2 = App(Lam(x, Lam(y, Var(y))), Reset(Wdiverge ))M2 = App(Lam(x, Lam(y, Var(y))), Reset(Mdiverge ))λ 式の表記： (λx. λy. y) ⟨Mdiverge ⟩P 2 [[W2 ]] ρ を計算すると、P 2 [[Wdiverge ]] ρ の周りの継続が P 2 [[Wdiverge ]] ρ の結果を捨てるため、
lam(λy. var(y)) となる。一方で I [[M2 ]] ρ′ を計算すると発散する。変換前に存在していた停止しない計算が変換後には消えているため、部分評価器は正しくない。
3 節で見た通り、dynamic な関数呼び出しの部分評価の定義において、停止しない計算が消滅してしまうのを防ぐために、let-insertion を使って dynamic な関数呼び出しを let 文に残している。なぜ Wdiverge に含まれていた dynamic な関数呼び出しは消滅してしまったのだろうか。W2
を部分評価すると次のような経過をたどる。
P 2 [[W2 ]] ρ = (λx′ . P 2 [[Lam(y, Var(y))]] ρ[x′ /x]) ⟨P 2 [[Wdiverge ]] ρ⟩
Wdiverge の dynamic な関数呼び出しを部分評価する際、let-insertion が行われるが、let 文はP 2 [[Wdiverge ]] ρ を囲う reset の下に置かれる。そのため、のちのステップで let 文ごと消滅してし
まう。
5.2.2

static な shift

5.1.2 節で説明した通り、(⟨(λv. K) (P 2 [[Shift(n, W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Shift(n, M )]] ρ′ )⟩) ∈ Rβの証明が破綻するのは、捕捉した継続に渡される値を V ′ として、⟨(λv ′ . K ′ ) V ′ ⟩ が発散するときである。そのような場合の例として例 3 を考える。I [[M3′ ]] ρ′ の計算において、Shift(k, M3 ) により捕捉される継続に渡す値を V ′ として、⟨(λy ′ . I [[Mdiverge ]] ρ′ [y ′ /y]) V ′ ⟩ は発散する。W3 は M3を、W3′ は M3′ を束縛時解析したものである。また、Wdiverge と Mdiverge は例 1 と同じである。
例 3.

W3′ = Reset(App(Lam(y, Wdiverge ), Shift(k, W3 )))M3′ = Reset(App(Lam(y, Mdiverge ), Shift(k, M3 )))λ 式の表記： ⟨(λy. Mdiverge ) (ξk. M3 )⟩W3 = App(Lam(x, Lam(y, Var(y))), App(Var(k), Lam(z, Var(z))))M3 = App(Lam(x, Lam(y, Var(y))), App(Var(k), Lam(z, Var(z))))λ 式の表記： (λx. λy. y) (k (λz. z))

P 2 [[W3′ ]] ρ を計算すると、lam(λy. var(y)) となる。一方で I [[M3′ ]] ρ′ を計算すると発散する。変
換前に存在していた停止しない計算が変換後には消えているため、部分評価器は正しくない。
なぜ W3 に含まれていた dynamic な関数呼び出しは、let-insertion を使って let 文に残したはずであるのに消滅してしまったのだろうか。W3′ を部分評価すると次のような経過をたどる。
P 2 [[W3′ ]] ρ
= ⟨(λy ′ . P 2 [[Wdiverge ]] ρ[y ′ /y]) (ξk ′ . P 2 [[W3 ]] ρ[k ′ /k])⟩= ⟨(λy ′ . P 2 [[Wdiverge ]] ρ[y ′ /y]) (ξk ′ . (λx′ . P 2 [[Lam(y, Var(y))]] ρ[x′ /x, k ′ /k]) (k ′ (λz ′ . z ′ )))⟩∼ (λx′ . P 2 [[Lam(y, Var(y))]] ρ[x′ /x, λv. ⟨(λy ′ . P 2 [[Wdiverge ]] ρ[y ′ /y]) v⟩/k]) (⟨P 2 [[Wdiverge ]] ρ[y ′ /y]⟩)Wdiverge の dynamic な関数呼び出しを部分評価する際、let-insertion が行われるが、let 文はP 2 [[Wdiverge ]] ρ[y ′ /y] を囲う reset の下に置かれる。そのため、のちのステップで let 文ごと消滅し
てしまう。
10

本稿の shift/reset の部分評価器

6

本稿が提案する部分評価器は以下の通りである。部分評価器・型システム共に、static な resetと static な shift 以外は先行研究 [2, 1] と変わらない。先行研究と異なる部分を赤文字で示す。
部分評価器：

P 3 [[Var(n)]] ρ = ρ (n)P 3 [[Lam(n, W )]] ρ = λx. P 3 [[W ]] ρ[x/n]P 3 [[Lam(n, W )]] ρ = lam(λx. shift(λk. ⟨reset(app(var(k), P 3 [[W ]] ρ[var(x)/n]))⟩))
P 3 [[App(W1 , W2 )]] ρ = (P 3 [[W1 ]] ρ) (P 3 [[W2 ]] ρ)
P 3 [[App(W1 , W2 )]] ρ = ξk. reset(let(app(P 3 [[W1 ]] ρ, P 3 [[W2 ]] ρ), lam(λt. k (var(t)))))
P 3 [[Shift(n, W )]] ρ = ξk. P 3 [[W ]] ρ[λv. ξk ′ . let(k v, lam(λt. k ′ (var(t))))/n]
P 3 [[Shift(n, W )]] ρ = ξk. P 3 [[W ]] ρ[lam(λv. ⟨k (var(v))⟩)/n]
P 3 [[Reset(W )]] ρ = ξk. let(⟨P 3 [[W ]] ρ⟩, lam(λt. k (var(t))))型：

τ= d | τ /τ → τ /τ型システム：

A[n : τ ], α ⊢ Var(n) : τ, α [Var(n)]A[n : σ], α ⊢ M : τ, β [W ]A, δ ⊢ M1 : σ/α → τ /ϵ, β [W1 ]A, ϵ ⊢ M2 : σ, δ [W2 ]A, δ ⊢ Lam(n, M ) : σ/α → τ /β, δ [Lam(n, W )]A, α ⊢ App(M1 , M2 ) : τ, β [App(W1 , W2 )]A[n : τ /d → d/d], σ ⊢ M : σ, β [W ]A, σ ⊢ M : σ, d [W ]A, d ⊢ Shift(n, M ) : τ, β [Shift(n, W )]A, d ⊢ Reset(M ) : d, d [Reset(W )]A[n : d], d ⊢ M : d, d [W ]A, δ ⊢ Lam(n, M ) : d, δ [Lam(n, W )]A, δ ⊢ M1 : d, β [W1 ] A, d ⊢ M2 : d, δ [W2 ]A, d ⊢ App(M1 , M2 ) : d, β [App(W1 , W2 )]A[n : d], σ ⊢ M : σ, β [W ]A, d ⊢ Shift(n, M ) : d, β [Shift(n, W )]6.1

static な reset

5.2.1 節で見た dynamic な eﬀect の消滅が行われないように、定義を変更する。3 節の dynamic
な関数呼び出しの部分評価で見た通り、eﬀect を捨ててしまうことを防ぐためによく用いられる手法は、let-insertion を行うことである。そこで、reset の部分評価の定義を以下のように定義することを考える。
P 3 [[Reset(W )]] ρ = ξk. let(⟨P 3 [[W ]] ρ⟩, lam(λt. k (var(t))))
こうすると、継続 k に渡されるものは値 var(t) となる。そのため 7.2.1 節で見る通り、正当性の証明を行うことができる。また、W が eﬀect を持つ項だったとしても、let-insertion により eﬀectが消えないようになる。

11

6.2

static な shift

5.2.2 節で見た dynamic な eﬀect の消滅が行われないように、定義を変更する。static な resetと同様に、eﬀect を捨ててしまうことを防ぐために let-insertion を行う。static な shift の部分評
価の定義を以下のように定義することを考える。
P 3 [[Shift(n, W )]] ρ = ξk. P 3 [[W ]] ρ[λv. ξk ′ . let(k v, lam(λt. k ′ (var(t))))/n]
こうすると、継続 k ′ に渡されるものは値 var(t) となる。そのため 7.2.2 節で見る通り、正当性の証明を行うことができる。また、W が eﬀect を持つ項だったとしても、let-insertion により eﬀectが消えないようになる。

6.3
6.3.1

型付け規則における変更
static な reset

先行研究の static な reset の型付け規則はA, σ ⊢ M : σ, τ [W ]A, α ⊢ Reset(M ) : τ, α [Reset(W )]であったが、本稿の static な reset の型付け規則は次のようになっている。
A, σ ⊢ M : σ, d [W ]A, d ⊢ Reset(M ) : d, d [Reset(W )]これは static な reset の特化の定義

P 3 [[Reset(W )]] ρ = ξk. let(⟨P 3 [[W ]] ρ⟩, lam(λt. k (var(t))))に由来している。τ が d となった理由は、特化の定義において ⟨P 3 [[W ]] ρ⟩ が let の引数になっているためである。また、α が d となった理由は、特化の定義において λt. k (var(t)) が lam の引数になっているためである。

6.3.2

static な shift

先行研究の static な reset の型付け規則はA[n : τ /δ → α/δ], σ ⊢ M : σ, β [W ]A, α ⊢ Shift(n, M ) : τ, β [Shift(n, W )]であったが、本稿の static な shift の型付け規則は次のようになっている。
A[n : τ /d → d/d], σ ⊢ M : σ, β [W ]A, d ⊢ Shift(n, M ) : τ, β [Shift(n, W )]これは static な shift の特化の定義

P 3 [[Shift(n, W )]] ρ = ξk. P 3 [[W ]] ρ[λv. ξk ′ . let(k v, lam(λt. k ′ (var(t))))/n]に由来している。α が d となった理由は、特化の定義において k v が let の引数になったいるためである。また、δ が d となった理由は、特化の定義において λt. k ′ (var(t)) が lam の引数になっているためである。

12

型の制約が厳しくなったことによる影響

6.4

let-insertion により正しい部分評価器を得ることができたが、その代わりに let-insertion は 6.3
節の通り、型の制約を厳しくした。先行研究の型システムでは型が付くが、本研究の型システム
では厳しくなった制約により型が付かない例として例 4 が考えられる。
例 4.

W4 = Reset(App(Lam(x, Var(x)), Shift(k, Var(k))))λ 式の表記： ⟨(λx. x) (ξk. k)⟩
6.3.1 節で見た通り、先行研究の static な reset の型付け規則の τ は d となった。そのため、staticな reset に囲われた項の部分評価結果が static な関数となる例 4 は型が付かない。また、6.3.2 節
で見た通り、先行研究の static な shift の型付け規則の α と δ は d となった。この点でも例 4 は型が付かない。
例 4 のように、dynamic な関数呼び出しが存在せず、let-insertion が必要ない項にも型の制約がかかってしまう。

7

正当性の証明7.1

いくつかの性質補題 1 (Admissibility, Wand [12]). もし M1 ∼ M1′ かつ M2 ∼ M2′ ならば (M1 , M2 ) ∈ Rτ ⇐⇒(M1′ , M2′ ) ∈ Rτ
証明 τ の長さ |τ | の帰納法による。|τ | は |d| = 0 と |σ/α → τ /β| = |β| + 1 によって定義される。型が d の場合、十分に大きい n に対し、

(M1 , M2 ) ∈ Rd ⇐⇒ I [[↓n M1 ]] ρid ∼ M2⇐⇒ I [[↓n M1′ ]] ρid ∼ M2′⇐⇒ (M1′ , M2′ ) ∈ Rd
型が σ/α → τ /β の場合、|β| < |σ/α → τ /β| であるから(M1 , M2 ) ∈ Rσ/α→τ /β⇐⇒ ∀(V1 , V2 ) ∈ Rσ . ∀(λv1 . K1 , λv2 . K2 ) |= τ ; α. (⟨(λv1 . K1 ) (M1 V1 )⟩, ⟨(λv2 . K2 ) (M2 V2 )⟩) ∈ Rβ⇐⇒ ∀(V1 , V2 ) ∈ Rσ . ∀(λv1 . K1 , λv2 . K2 ) |= τ ; α. (⟨(λv1 . K1 ) (M1′ V1 )⟩, ⟨(λv2 . K2 ) (M2′ V2 )⟩) ∈ Rβ⇐⇒ (M1′ , M2′ ) ∈ Rσ/α→τ /β
補題 2. 任意の τ に対し、(λx. x, λx′ . x′ ) |= τ ; τ .
証明(V, V ′ ) ∈ Rτ とする。(⟨(λx. x) V ⟩, ⟨(λx′ . x′ ) V ′ ⟩) ∈ Rτ であることを示す。これは⟨(λx. x) V ⟩ ∼ ⟨V ⟩ ∼ V

であり、V ′ についても同じことが言えるため、補題 1 によって証明される。

13

7.2

正当性の証明定理 1. A, α ⊢ M : τ, β [W ] かつ (ρ, ρ′ ) |= A かつ (λv. K, λv ′ . K ′ ) |= τ ; α, ならば(⟨(λv. K) (P 3 [[W ]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[M ]] ρ′ )⟩) ∈ Rβ .
この定理が成り立てば、継続を初期継続にし、環境を空にすることによって、欲しかった部分
評価器の正当性を証明できる。
系 1. d ⊢ M : d, d [W ] ならば I [[↓0 ⟨P 3 [[W ]] ∅⟩]] ρid ∼ ⟨I [[M ]] ∅⟩.
定理 1 と系 1 の文言は、以前の成り立っていなかった文言の P 2 を P 3 に変えただけである。つ
まり以前の文言は P 3 に対しては成り立つことを意味している。
定理 1 の証明は、A ⊢ M : τ [W ] の証明の構造に沿った帰納法によるものである。A ⊢ M : τ [W ]に対して適用される型規則は 7 通りであるため、証明は 7 つの場合分けからなる。static な resetと static な shift の場合以外、証明は先行研究 [2] と変わらない。よって、この２つの場合のみ部
分評価の正当性を証明する。

7.2.1

static な reset(A, d ⊢ Reset(M ) : d, d [Reset(W )] の場合)
A, σ ⊢ M : σ, d [W ]A, d ⊢ Reset(M ) : d, d [Reset(W )]が成り立っている。示したいのは、(ρ, ρ′ ) |= A かつ (λv. K, λv ′ . K ′ ) |= d ; d ならば(⟨(λv. K) (P 3 [[Reset(W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Reset(M )]] ρ′ )⟩) ∈ Rdである。 補題 1 と、

=
∼
∼
∼
∼

⟨(λv. K) (P 3 [[Reset(W )]] ρ)⟩{P 3 の定義 }⟨(λv. K) (ξk. let(⟨P 3 [[W ]] ρ⟩, lam(λt. k (var(t)))))⟩{reset-shift}⟨(λk. let(⟨P 3 [[W ]] ρ⟩, lam(λt. k (var(t))))) (λx. ⟨(λv. K) x⟩)⟩{βv }⟨let(⟨P 3 [[W ]] ρ⟩, lam(λt. (λx. ⟨(λv. K) x⟩) (var(t))))⟩{βv }⟨let(⟨P 3 [[W ]] ρ⟩, lam(λt. ⟨(λv. K) (var(t))⟩))⟩{reset-value}let(⟨P 3 [[W ]] ρ⟩, lam(λt. ⟨(λv. K) (var(t))⟩))と⟨(λv ′ . K ′ ) (I [[Reset(M )]] ρ′ )⟩= {I の定義 }⟨(λv ′ . K ′ ) ⟨I [[M ]] ρ′ ⟩⟩より、(let(⟨P 3 [[W ]] ρ⟩, lam(λt. ⟨(λv. K) (var(t))⟩)),⟨(λv ′ . K ′ ) ⟨I [[M ]] ρ′ ⟩⟩) ∈ Rd
を示せば良い。

14ここで、補題 2 から (λx. x, λx′ . x′ ) |= σ ; σ であり、これと帰納法の仮定から(⟨(λx. x) (P 3 [[W ]] ρ)⟩, ⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩) ∈ Rd が成り立つ。これを使うと上の欲しかった論理
関係は、十分に大きい n に対して以下のように導出できる。

=
=
=
=
∼
∼
∼
∼
∼

I [[↓n (let(⟨P 3 [[W ]] ρ⟩, lam(λt. ⟨(λv. K) (var(t))⟩)))]] ρid{let の定義 }I [[↓n (app(lam(λt. ⟨(λv. K) (var(t))⟩), ⟨P 3 [[W ]] ρ⟩))]] ρid{↓n の定義 }I [[App(Lam(n, ↓n+1 ⟨(λv. K) (var(n))⟩), ↓n ⟨P 3 [[W ]] ρ⟩)]] ρid{I の定義 }(λzn . I [[↓n+1 ⟨(λv. K) (var(n))⟩]] ρid [zn /n]) (I [[↓n ⟨P 3 [[W ]] ρ⟩]] ρid ){ρid の定義 }(λzn . I [[↓n+1 ⟨(λv. K) (var(n))⟩]] ρid ) (I [[↓n ⟨P 3 [[W ]] ρ⟩]] ρid ){(λv. K, λv ′ . K ′ ) |= d ; d かつ (var(n), zn ) ∈ Rd }(λzn . ⟨(λv ′ . K ′ ) zn ⟩) (I [[↓n ⟨P 3 [[W ]] ρ⟩]] ρid ){βΩ }(λzn . ⟨(λv ′ . K ′ ) zn ⟩) (I [[↓n ⟨(λx. x) (P 3 [[W ]] ρ)⟩]] ρid ){(⟨(λx. x) (P 3 [[W ]] ρ)⟩, ⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩) ∈ Rd }(λzn . ⟨(λv ′ . K ′ ) zn ⟩) (⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩){βΩ }(λzn . ⟨(λv ′ . K ′ ) zn ⟩) (⟨I [[M ]] ρ′ ⟩){βΩ }⟨(λv ′ . K ′ ) ⟨I [[M ]] ρ′ ⟩⟩· · · (∗)

最後の ⟨(λx. x) (P 3 [[W ]] ρ)⟩ と ⟨(λx′ . x′ ) (I [[M ]] ρ′ )⟩ が関係付いていることの証明の途中にある(λzn . I [[↓n+1 ⟨(λv. K) (var(n))⟩]] ρid ) (I [[↓n ⟨P 3 [[W ]] ρ⟩]] ρid )∼ {(λv. K, λv ′ . K ′ ) |= d ; d かつ (var(n), zn ) ∈ Rd }(λzn . ⟨(λv ′ . K ′ ) zn ⟩) (I [[↓n ⟨P 3 [[W ]] ρ⟩]] ρid )· · · (∗)という変形は、定義を変更したために行えたことである。let-insertion により、継続の引数が値、つまり変数 var(n) もしくは zn となり、継続が関係付いていることを利用することができた。

7.2.2

static な shift
A[n : τ /d → d/d], σ ⊢ M : σ, β [W ]A, d ⊢ Shift(n, M ) : τ, β [Shift(n, W )]が成り立っている。示したいのは、(ρ, ρ′ ) |= A かつ (λv. K, λv ′ . K ′ ) |= τ ; d ならば(⟨(λv. K) (P 3 [[Shift(n, W )]] ρ)⟩, ⟨(λv ′ . K ′ ) (I [[Shift(n, M )]] ρ′ )⟩) ∈ Rβ15である。補題 1 と、

=
∼
∼
∼
∼

⟨(λv. K) (P 3 [[Shift(n, W )]] ρ)⟩{P 3 の定義 }⟨(λv. K) (ξk. P 3 [[W ]] ρ[λw. ξk ′ . let(k w, lam(λt. k ′ (var(t))))/n])⟩{reset-shift}⟨(λk. P 3 [[W ]] ρ[λw. ξk ′ . let(k w, lam(λt. k ′ (var(t))))/n]) (λa. ⟨(λv. K) a⟩)⟩{βv }⟨P 3 [[W ]] ρ[λw. ξk ′ . let((λa. ⟨(λv. K) a⟩) w, lam(λt. k ′ (var(t))))/n]⟩{βv }⟨P 3 [[W ]] ρ[λw. ξk ′ . let(⟨(λv. K) w⟩, lam(λt. k ′ (var(t))))/n]⟩{βΩ }⟨(λx. x) (P 3 [[W ]] ρ[λw. ξk ′ . let(⟨(λv. K) w⟩, lam(λt. k ′ (var(t))))/n])⟩

と

=
∼
∼
∼

⟨(λv ′ . K ′ ) (I [[Shift(n, M )]] ρ′ )⟩{I の定義 }⟨(λv ′ . K ′ ) (ξk. I [[M ]] ρ′ [k/n])⟩{reset-shift}⟨(λk. I [[M ]] ρ′ [k/n]) (λa′ . ⟨(λv ′ . K ′ ) a′ ⟩)⟩{βv }⟨I [[M ]] ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n]⟩{βΩ }⟨(λx′ . x′ ) (I [[M ]] ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n])⟩より、(⟨(λx. x) (P 3 [[W ]] ρ[λw. ξk ′ . let(⟨(λv. K) w⟩, lam(λt. k ′ (var(t))))/n])⟩,⟨(λx′ . x′ ) (I [[M ]] ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n])⟩) ∈ Rβを示せば良い。
補題 2 から (λx. x, λx′ . x′ ) |= σ ; σ であるから、(ρ[λw. ξk ′ . let(⟨(λv. K) w⟩, lam(λt. k ′ (var(t))))/n], ρ′ [λa′ . ⟨(λv ′ . K ′ ) a′ ⟩/n]) |= A[n : τ /d → d/d]つまり(λw. ξk ′ . let(⟨(λv. K) w⟩, lam(λt. k ′ (var(t)))), λa′ . ⟨(λv ′ . K ′ ) a′ ⟩) ∈ Rτ /d→d/dが成り立てば、帰納法の仮定より証明が終わる。
そこで、これを示す。そのためには、任意の (V, V ′ ) ∈ Rτ と (λu. L, λu′ . L′ ) |= d ; d について、(⟨(λu. L) ((λw. ξk ′ . let(⟨(λv. K) w⟩, lam(λt. k ′ (var(t))))) V )⟩, ⟨(λu′ . L′ ) ((λa′ . ⟨(λv ′ . K ′ ) a′ ⟩) V ′ )⟩) ∈ Rd

16

を示せば良い。補題 1 と、

∼
∼
∼
∼
∼

⟨(λu. L) ((λw. ξk ′ . let(⟨(λv. K) w⟩, lam(λt. k ′ (var(t))))) V )⟩{βv }⟨(λu. L) (ξk ′ . let(⟨(λv. K) V ⟩, lam(λt. k ′ (var(t)))))⟩{reset-shift}⟨(λk ′ . let(⟨(λv. K) V ⟩, lam(λt. k ′ (var(t))))) (λa. ⟨(λu. L) a⟩)⟩{βv }⟨let(⟨(λv. K) V ⟩, lam(λt. (λa. ⟨(λu. L) a⟩) (var(t))))⟩{βv }⟨let(⟨(λv. K) V ⟩, lam(λt. ⟨(λu. L) (var(t))⟩))⟩{reset-value}let(⟨(λv. K) V ⟩, lam(λt. ⟨(λu. L) (var(t))⟩))と⟨(λu′ . L′ ) ((λa′ . ⟨(λv ′ . K ′ ) a′ ⟩) V ′ )⟩∼ {βv }⟨(λu′ . L′ ) ⟨(λv ′ . K ′ ) V ′ ⟩⟩より、(let(⟨(λv. K) V ⟩, lam(λt. ⟨(λu. L) (var(t))⟩)), ⟨(λu′ . L′ ) ⟨(λv ′ . K ′ ) V ⟩⟩) ∈ Rd
を示せば良い。これは、十分に大きい n に対して以下のように導出できる。

=
=
=
=
∼
∼
∼

let(⟨(λv. K) V ⟩, lam(λt. ⟨(λu. L) (var(t))⟩)){let の定義 }I [[↓n (app(lam(λt. ⟨(λu. L) (var(t))⟩), ⟨(λv. K) V ⟩))]] ρid{↓n の定義 }I [[App(Lam(n, ↓n+1 ⟨(λu. L) (var(n))⟩), ↓n ⟨(λv. K) V ⟩)]] ρid{I の定義 }(λzn . I [[↓n+1 ⟨(λu. L) (var(n))⟩]] ρid [zn /n]) (I [[↓n ⟨(λv. K) V ⟩]] ρid ){ρid の定義 }(λzn . I [[↓n+1 ⟨(λu. L) (var(n))⟩]] ρid ) (I [[↓n ⟨(λv. K) V ⟩]] ρid ){(λu. L, λu′ . L′ ) |= d ; d かつ (var(n), zn ) ∈ Rd }(λzn . ⟨(λu′ . L′ ) zn ⟩) (I [[↓n ⟨(λv. K) V ⟩]] ρid ){(λv. K, λv ′ . K ′ ) |= τ ; d かつ (V, V ′ ) ∈ Rτ }(λzn . ⟨(λu′ . L′ ) zn ⟩) ⟨(λv ′ . K ′ ) V ′ ⟩{βΩ }⟨(λu′ . L′ ) ⟨(λv ′ . K ′ ) V ′ ⟩⟩· · · (∗)

最後の let(⟨(λv. K) V ⟩, lam(λt. ⟨(λu. L) (var(t))⟩)) と ⟨(λu′ . L′ ) ⟨(λv ′ . K ′ ) V ⟩⟩ が関係付いていることの証明の途中にある(λzn . I [[↓n+1 ⟨(λu. L) (var(n))⟩]] ρid ) (I [[↓n ⟨(λv. K) V ⟩]] ρid )∼ {(λu. L, λu′ . L′ ) |= d ; d かつ (var(n), zn ) ∈ Rd }(λzn . ⟨(λu′ . L′ ) zn ⟩) (I [[↓n ⟨(λv. K) V ⟩]] ρid )· · · (∗)という変形は、定義を変更したために行えたことである。let-insertion により、継続の引数が値、つまり変数 var(n) もしくは zn となり、継続が関係付いていることを利用することができた。

17

8

まとめと今後の課題

本研究では先行研究 [2, 1] の shift/reset の部分評価器の正当性の証明において、継続の引数の項を値でないのに値であるとして扱っている部分を発見した。これは、部分評価器が正しくない
こと、つまりは変換前に存在していた dynamic な eﬀect が変換後には消えてしまうことに繋がっていた。そこで、let-insertion を用いて定義を修正し、eﬀect が消えることを防いだ新しい部分評
価器を定義し、それに対して正当性の証明を行った。
今後の課題としては、厳しくなりすぎている型の制約を緩和することが挙げられる。6.3 節で説明した通り、先行研究の static な reset の型付け規則はA, σ ⊢ M : σ, τ [W ]A, α ⊢ Reset(M ) : τ, α [Reset(W )]であったが、本稿の型付け規則は次のようになっている。
A, σ ⊢ M : σ, d [W ]A, d ⊢ Reset(M ) : d, d [Reset(W )]これは static な reset の特化の定義

P 3 [[Reset(W )]] ρ = ξk. let(⟨P 3 [[W ]] ρ⟩, lam(λt. k (var(t))))に由来している。しかし、static な reset の項 Reset(W ) に対して、⟨P 3 [[W ]] ρ⟩ の型が dynamic な型となるように制限してしまうことは本来なら避けたい。型が dynamic になってしまっているのは、入力言語の shift/reset の実行と let-insertion の実現に、どちらもメタ言語の同じ shift/resetを使っているためである。そうではなく入力言語の shift/reset を超えた位置に let-insertion を行
えればこの問題は解消できる可能性がある。これを目指して、現在は CPS を２度行った 2CPSの体系を検討中である。
また今後の展望として、代数的エフェクトを含む他の限定継続演算子と部分評価器の組み合わせが考えられる。shift/reset はいろいろな限定継続演算子の中では扱いやすい演算子であり、他の限定継続演算子の部分評価を考える上での土台となると考えられる。

謝辞
有益なコメントをくださった査読者の皆様に感謝申し上げます。また、本研究は一部 JSPS 科
研費 22H03563 の助成を受けたものです。

参考文献[1] K. Asai. Logical relations for call-by-value delimited continuations. In Symposium on Trends inFunctional Programming, 2005.
[2] K. Asai. Logical relations for call-by-value delimited continuations. In Technical Report of Department of Information Science, Ochanomizu University, OCHA-IS 06-1, April 2006.
[3] M. Biernacka and D. Biernacki. A context-based approach to proving termination of evaluation.
Electronic Notes in Theoretical Computer Science, 249:169–192, 2009. Proceedings of the 25th
Conference on Mathematical Foundations of Programming Semantics (MFPS 2009).
[4] A. Bondorf and O. Danvy. Automatic autoprojection of recursive equations with global variables
and abstract data types. Science of Computer Programming, 16(2):151–195, 1991.

18

[5] O. Danvy and A. Filinski. Abstracting control. In Proceedings of the 1990 ACM Conference on
LISP and Functional Programming, LFP ’90, page 151–160, New York, NY, USA, 1990. Association
for Computing Machinery.
[6] N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula
manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381–392, 1972.
[7] N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation.
Englewood Cliﬀs, NJ: Prentice Hall, 1993.
[8] Y. Kameyama and M. Hasegawa. A sound and complete axiomatization of delimited continuations.
In Proceedings of the eighth ACM SIGPLAN International Conference on Functional Programming(ICFP’03), August 2003.
[9] Y. Kameyama, O. Kiselyov, and C. chieh Shan. Shifting the stage: Staging with delimited control.
Journal of Functional Programming, 21(6):617–662, 2011.
[10] R. Leißa, K. Boesche, S. Hack, A. Pérard-Gayot, R. Membarth, P. Slusallek, A. Müller, and
B. Schmidt. Anydsl: a partial evaluation framework for programming high-performance libraries.
Proceedings of the ACM on Programming Languages, 2:1 – 30, 2018.
[11] J. Oishi and Y. Kameyama. Staging with control: Type-safe multi-stage programming with control
operators. In Proceedings of the 16th ACM SIGPLAN International Conference on Generative
Programming: Concepts and Experiences, GPCE 2017, page 29–40, New York, NY, USA, 2017.
Association for Computing Machinery.
[12] M. Wand. Specifying the correctness of binding-time analysis. In Journal of Functional Programming, Vol. 3, No. 3, pages 365–387. Cambridge University Press, July 1993.

19