型付きの shift/reset を含む言語における Reﬂection にむけて理学専攻 情報科学コース 2040659 山本 充子 (指導教員：浅井 健一)

1

はじめにCPS とは、継続 (ある時点における残りの計算) を明示的に表すようにした表現形式のことである。また、CPS 変換前の表現形式を DS と呼ぶ。CPS のプログ
ラムでは、全て tail-call(末尾呼び出し) になっているのに対して、DS のプログラムでは、関数呼び出しが末尾に限定されない。
CPS のプログラムに変換する CPS 変換は、コンパイラなどで使われおり [1]、コンパイラの正しさを保証するためには CPS 変換の正当性を言う必要がある。正当性として健全性と完全性を示す方法の一つが Galois Connection を示すことである。本研究は、shift/reset を含む言語に対して Galois Connectionを示すとともに、Galois Connection の特別なケースである Reﬂection に関する証明を行なったものである。
プログラミング言語において型を導入することは、プログラムの安全性を保証できる。本研究では、型を導入することで、DS と CPS の世界で型がどのように対応していくのかをみていき、型がついた世界でもReﬂection の証明ができるのかをみた。
型が付いた体系で証明を行おうとすると、複雑になり手で証明すると誤りが発生することがある。そこで、定理証明系の Agda を用いて型のついた形で定式化をして証明を行なった。本研究で示す証明は、DS のプログラムを let で正規化した体系の DSkernel 項と CPS項の間の Reﬂection である。DSkernel の体系と CPSの体系の型システムと証明が完成しており、これらはDS と CPS の間における Reﬂection を示す第一歩となる。

2

Galois Connection と Reﬂection

これまで、CPS 変換の正当性の証明は様々に行われてきた。Sabry と Wadler は、Galois Connection を用
いて call-by-value の λ 計算に対する CPS 変換の健全性と完全性を示すことで、CPS 変換の正当性を証明した [4]。彼らは、CPS 変換が Reﬂection であることも示した。Biernacki、Pyzik と Sieczkowski は、Sabry とWadler の λ 式に shift/reset[3] を加えて拡張し、その λ 式においても Reﬂection を証明ができることを示した [2]。
Galois Connection の定義を Sabry と Wadler の論文より引用する [4]。以下の式における、→ は、one step簡約を意味し、↠ は、one step 以上の簡約を表す。また、λSc は、DS 項を表し、 λcps は、CPS 項を表す。
↠λSc は DS における簡約、↠λcps は CPS 項におけるS簡約を表す。写像 ∗ : λSc → λcps と # : λcps → λc はそれぞれ CPS 変換と DS 変換を表す。

命題 2 以下の 4 つの条件が成り立つとき、写像 ∗ と# は λSc から λcps への Galois Connection であるとい′う。(M, M ′ ∈ λSc , N, N ∈ λcps )定義 1 は以下のように書き換えることができる。

M ↠ M ∗#(2)N #∗ ↠ N(3)

M ↠ M ′ ならば M ∗ ↠ M ′(4)′#N ↠ N ′ ならば N # ↠ N∗

定義 3 写像 ∗ と # が Galois Connection であり、N ≡N #∗ のとき、∗ と # は λSc と λcps において、Reﬂectionであるという。(N ∈ λcps )DS 変換 # をした結果は、すべての DS 項 λSc に戻るとは限らない。よって、DS 変換して得られた項をDSkernel λSc∗∗ と定義する。DSkernel の項は let で正規化された式になっている。Reﬂection が示されたと
き、CPS 項 λcps と DSkernel 項 λSc∗∗ は全てそれぞれ１対１対応しており、DSkernel 項 λSc∗∗ から CPS 項 λcpsへの同型写像が存在する。本研究は、DSkernel と CPSの間で Reﬂection を証明したものである。

CPS 項

3項∆

τ
M, N::=::=Nat | Bool | τ2 → [τ1 → τ3 ] → τ4
K ∆ V | V W K ∆ | K ∆ M•

値V, W::=

n | x | λxk. Mk | S

shift

S::=λwj. w(λyk. k(jy))(λx. x)

継続∆K::=(∆=k) k | (∆=•) λx. x | λx. M∆

型

図 1: CPS 項
本研究は、DSkernel 項と CPS 項の間に Reﬂectionを示すので、DS 項と CPS 変換の定義は省略する。図1 を見ると、項と継続には ∆ がついている。左辺に現れる ∆ と右辺に現れる ∆ には同じものが入り、∆ には変数 k または • のどちらかが入る。∆ をつけること
で、継続が tail-recursive か returning call かを区別することができる。

DS 変換

4x♮

(λxk. Mk )♮(λwj. w(λyk. k(jy))(λx. x))k♭(λx. x)定義 1 以下が成り立つとき、写像 ∗ と # は λSc からλcps への Galois Connection であるという。(M, M ′ ∈λcS , N, N ′ ∈ λcps )M ↠λSc N # if and only if M ∗ ↠λcps N(1)♭(λx. N∆ )(K∆ V )♭♯(V W K∆ )(K∆ M• )♯♯♮=x=λx. S(λk. ⟨Mk♯ ⟩)=S=k[ ]=[ ]=♯let x = [ ] in N∆=♭K∆[V ♮ ]=♭K∆[V ♮ W ♮ ]=♭K∆[⟨M• ♯ ⟩]図 2: DS 変換

V ♮ は値の変換、K ♭ は継続の変換、M ♯ は項の変換を表す。Biernacki らの定義では、関数抽象の変換にお♮いて (λxk. Mk ) = λx. Mk♯ とし、継続 k を削除した。
彼らの定義では、この k が後の計算でいずれ消えることが暗黙のうちにあるため、このような定義にした。
しかし、これを Agda で表現しようとすると Mk♯ 内の自由変数 k を削除するのは難しい。よって、k を明示するために図 2 のように定義する必要があった。

DSkernel 項

5型

τ::=

Nat | Bool | τ1 → τ2 @cps[τ3 , τ4 ]項∆

M, N::=

K∆ [V ] | K∆ [P ]

値

V, W

::=

n | x | λx. S(λk. ⟨Mk ⟩) | S

値でない

P, Q::=

V W | ⟨M• ⟩コンテキスト∆

K::=(∆=k) k[定理 6 (DS 変換の 1step 簡約の保存証明) 次のことが成り立つ：

1. Mk → Mk′ ならば Mk♯ → M ′ k♯
2. M• → M•′ ならば ⟨M•♯ ⟩ → ⟨M ′ • ⟩′♮′♮
3. V → V ならば V → V♭♭
4. K → K ′ ならば K∆→ K ′∆♯

定理 5 と同様、1 は (β.v)、2 は、(β.S)、3 は (η.v)
を、4 は (η.let) の簡約の保存証明をそれぞれ行なった。
定理 5 では、次の代入補題を必要とする。
補題 7 (CPS 変換における代入補題) 次のことが成り立つ：†

1. V1 † [x := V † ] = (V1 [x := V ])‡2. K1 ‡ [x := V † ] = (K1 [x := V ])◦3. M ◦ [x := V † ] = (M [x := V ])‡†′‡4. K1 [x := V ][k := K ] = (K1 [x := V ][k′ := K])‡
5. M ◦ [x := V † ][k′ := K ‡ ] = (M [x := V ][k′ := K])◦] | (∆=•) [ ] | let x = [ ] in M∆

図 3: DSkernel 項
図 3 で示されているのは、DS 変換後の項、すなわち DSkernel 項の定義を表す。ここでは、shift を値として扱っている。通常、shift は、Sk. e のように項として表すが、Sk. e は S(λk. e) と同義である。また、値の関数抽象で λx. S(λk. ⟨Mk ⟩) となっているのは、4節の DS 変換で扱った通りである。

6

1 は値、2, 4 は継続、3, 5 は項に関する帰納法でそれぞれ解く。
同様に、定理 6 でも以下のような代入補題を必要とする。

CPS 同型写像

CPS 項と DS 項は１対１対応しているため、CPS 同型写像は DS 変換をひっくり返した定義となる。値の変換は V † 、コンテキストの変換は K ‡ 、項の変換は M ◦と表す。

補題 8 (DS 変換における代入補題) 次のことが成り立つ：♮Reﬂection を示すため、以下の定理を証明する必要がある。

1. V1 ♮ [x := V ♮ ] = (V1 [x := V ])♭2. K1 ♭ [x := V ♮ ] = (K1 [x := V ])♯♯♮3. M [x := V ] = (M [x := V ])4. K1 ♭ [x := V ♮ ][k′ := K ♭ ] = (K1 [x := V ][k′ := K])♭♯
5. M ♯ [x := V ♮ ][k ′ := K ♭ ] = (M [x := V ][k ′ := K])

定理 4 († と ‡ 、 ◦ の左逆元・右逆元) 次 の こ と が成り立つ:

補題 7 と同様、値、コンテキスト、項に関する帰納法でそれぞれ解く。

7正当性の証明

1. M ≡ M ◦♯2. V ≡ V †♮3. K ≡ K ‡♭♯◦
1. M∆≡ M∆

2. V
3.

♮†≡V♭‡K∆≡ K∆

左側にある３つの式は、左逆元の定理、右側の３つの式は右逆元の定理である。左逆元について、≡ になっているのは、DSkernel λSc∗∗ と CPS λcps は全ての項に対して 1 対 1 対応しているためである。それぞれの定理の証明ではまず、1 において項に関する帰納法で解く。さらに、1 では 2, 3 の定理を必要とする。2 は値に関する帰納法、3 は継続 または コンテキストに関する帰納法で解き、1, 2, 3 を相互再帰して証明を行う。
定理 5 (CPS 変換の 1step 簡約の保存証明) 次のことが成り立つ：◦1. M → M ′ ならば M ◦ → M ′◦2. ⟨M ⟩ → ⟨M ′ ⟩ ならば M ◦ → M ′′†′†
3. V → V ならば V → V‡
4. K → K ′ ならば K ‡ → K ′1 は (β.v)、2 は、(β.S)、3 は (η.v) を、4 は (η.let)の簡約の保存証明をそれぞれ行なった。

8まとめ

本研究では、Biernacki らの shift/reset 入りのラムダ計算に型をつけ、DSkernel と CPS の間の Reﬂection を証明した。また、それを Agda にのせた。DSkernel 項の定義を一般の DS 項に拡張し、DS 項と CPS 項の間における Reﬂection を証明しようとしているが、定義においてまだ課題が残っている。

参考文献[1] Andrew W Appel. Compiling with continuations. Cambridge university press, 2007.
[2] Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski.
A Reﬂection on Continuation-Composing Style.
InZena M. Ariola, editor, 5th International Conference onFormal Structures for Computation and Deduction (FSCD2020), Vol. 167 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 18:1–18:17, Dagstuhl, Germany,
2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.
[3] Olivier Danvy and Andrzej Filinski. Abstracting control.
In Proceedings of the 1990 ACM Conference on LISP andFunctional Programming, pp. 151–160, 1990.
[4] Amr Sabry and Philip Wadler. A reﬂection on call-byvalue. ACM transactions on programming languages andsystems (TOPLAS), Vol. 19, No. 6, pp. 916–941, 1997.