control/prompt 入り CPS 変換の正当性の証明
本田 華歩(指導教員：浅井 健一)

はじめに

1

つ目の引数の型、idk の返す値の型、idk の二つ目の引数の型に対応している。同様に Cons (::) と Append (@p ) はそれぞれ継続と trail、trail と trail を繋ぐものである。idk と同様に型を合わせるために compatible という名前で制約をかける関数を作っており、compatible の各行が Cons, Append の 4 行と対応している。

プログラムにおける「継続」とは、計算中のある時点における残りの計算のことを指す。継続をプログラム中で扱うには control/prompt [4] や shift/reset [2] など継続を切り取って扱う限定継続演算子が使われる。その意味論は継続渡し形式 (continuation-passing style; CPS) に変換することで与えられるが、これまで CPS 変換の正当性は shift/reset 入りの体系において議論されてきた。 [5, 6]
また、型システムにおいては、control/prompt が含まれる体系は、shift/reset が含まれる体系と違い、継続が連なっている trail という新しい概念を取り入れなければならない。そのため CPS 変換においても扱う型が増え、正当性の証明は複雑になる。本研究では、定理証明支援系言語である Agdaにおいて control/prompt が含まれた体系での CPS インタプ
リタ並びに CPS 変換を定式化し、CPS 変換の正当性を証明することを目指す。

= v

idk v k= k v idt

k :: idt=k′=λv. λt′ . k v (k ′ :: t′ )k :: kDS 項と CPS インタプリタ

2idk v idt

idk @p t =t

k @p tk :: t=

本節では CPS インタプリタを Agda で定式化する。

2.1

DS 項の定義

CPS 変換前の項を DS 項という。以下に DS 項の定義を示す。
型

τ:= Nat | Bool | τ2 → τ1 (µα ) α (µβ ) βtrailµ:= • | τ → τ ′ µ2.3値

v:= n | x | λx. e

項e:= v | e1 @ e2 | e1 + e2 | Fc. e | heiΓ ` e : τ (µα ) α (µβ ) β という型判定は、型環境 Γ のもとで、e が τ → µα → α の型の継続と µβ 型の trail を受け取り、β型の値を返すことを意味している。control/prompt の型規則
[1] を以下に示す。control のインタプリタは、Cons, Append,idk を全て含むため、前提に三つの制約が入る。prompt は idkのための is-id-trail が前提に入っている。control/prompt 以外の型規則は先行研究と同様である。

型は自然数型、真偽値型、関数型の三つからなる。関数型は、τ2 型の値を受け取ったら τ1 型の値を返す関数だが、継続(τ1 → µα → α) と trail (µβ ) の型の情報も持っている。trailは control/prompt に特有なもので、継続が連なった形をしている。τ → τ ′ µ は、τ から τ ′ への継続で、その際に µ 型のtrail を受け取ることを意味する。(•) は空の trail を表している。値は自然数、変数、λ 抽象の三つからなる。項は値、関数適用、足し算、control、prompt からなる。型と trail、値と項はそれぞれ相互再帰の形で Agda に載せることができた。

2.2

型規則

is-id-trail(γ, γ ′ , µid )compatible(t1 → t2 µ1 , µ2 , µ0 ) compatible(µβ , µ0 , µα )Γ, k : τ → t1 (µ1 ) t2 (µ2 ) α ` e : γ (µid ) γ ′ (•) β(TControl)Γ ` F c. e : τ (µα ) α (µβ ) βCPS インタプリタ
is-id-trail(β, β ′ , µid ) Γ ` e : β (µid ) β ′ (•) τ(TPrompt)Γ ` hei : τ (µα ) α (µα ) α

CPS 変換を定式化する前に、CPS インタプリタを Agda に載せた。CPS インタプリタの定義を以下に示す。
ε[[x]] ρ k t = k(ρ(x)) t′′ε[[λx. e]] ρ k t = k(λv. λk . ε[[e]] ρ[v/x] k ) tε[[e1 @ e2 ]] ρ k t = ε[[e1 ]] ρ (λv1 . ε[[e2 ]] ρ (λv2 . v1 v2 k) ) tε[[e1 + e2 ]] ρ k t = ε[[e1 ]] ρ (λv1 . ε[[e2 ]] ρ (λv2 . k(v1 + v2 )) ) tε[[Fc. e]] ρ k t = ε[[e]] ρ[λv. λk ′ . λt′ . k v (t @p k ′ :: t′ )/c] idk idt

型のついたプログラムを実行すると、定義された通りに型がついた値を返し、型エラーになることはない。つまり、インタプリタにおける型の対応を以下のように定義した時、定理 1 がいえる。
[[•]]µ = •[[τ → τ ′ µ]]µ = [[τ ]]τ → [[µ]]µ → [[τ ′ ]]τ

ε[[hei]] ρ k t = k(ε[[e]] ρ idk idt )t[[Nat]]τ = N

ここで、idk とは初期継続を表しており、渡す trail が空かそうでないかによって挙動が変わってくる。型付きの idk において型の辻褄を合わせるために is-id-trail という名前で制約をかける関数を作っている。下に idk の定義と is-id-trail の実際のコードを示す。is-id-trail の 3 つの引数は順に、idk の一[[Bool]]τ = B[[τ2 → τ1 (µα ) α (µβ ) β]]τ =[[τ2 ]]τ → ([[τ1 ]]τ → [[µα ]]µ → [[α]]τ ) → [[µβ ]]µ → [[β]]τ
75

定理 2 の証明では、e → e′ の簡約の形によって場合分けして取り組み、現段階では control 以外の場合において証明が済んでいる。証明の際は、必要な補題を都度立てる必要がある。例えば e → e′ が (λx. e1 ) @ v → e1 [x/v] の場合の証明には以下の補題を使用した。

定理 1 Γ ` e : τ (µα ) α (µβ ) β ならば Γ∗ ` ε[[e]] : ([[τ ]]τ →[[µα ]]µ → [[α]]τ ) → [[µβ ]]µ → [[β]]τ

Agda に CPS インタプリタを載せられたことにより、定理1 が証明できた。

3

CPS 変換の定式化

補題 3 (CPS 変換と代入の可換性) 任意の項 e1 、値 v 、継続 k 、trail t について (λx. e1 x)[v] 7→ e2 が成り立つとき、(λx. [[e1 x]] @ k @ t)[[[v]]] 7→ [[e2 ]] @ k @ t が成り立つ。

本稿では one-pass の CPS 変換 [3] を行う。2 節での CPS インタプリタを元にしてアンダーラインのついた式とオーバーラインのついた式に出力を区別して定義し、Agda に載せた。
アンダーラインのついた式は dynamic な式と呼び、自分で定義した出力時の構文を表す。オーバーラインのついた式はstatic な式と呼び、今回では Agda の本当の式であり CPS 変換時に実行されることを表す。

4CPS 変換の正当性の証明

4.1

代入規則と簡約規則

これは e1 の中にある x を v に置き換えると e2 になる時、e1の CPS 変化後の項にある x を v の CPS 変換後の値で置き換えると e2 の CPS 変換結果になる、つまり代入と CPS 変換の可換性を示している。
補題 4 (継続に関する代入演算) 任意の項 e、値 v 、trail t、
schematic な継続 k について (λx. [[e]] @ (k1 x) @ t)[v] 7→[[e]] @ (k1 v) @ t が成り立つ。

正当性を証明するために、DS 項、CPS 項それぞれにおいて代入規則と簡約規則を Agda に載せた。これまでの β 簡約と足し算の簡約規則に、下に示す control/prompt の簡約規則を加えた。

hE[Fc. e1 ]i →hv1 i

継続 k の変数の構造が変わらない場合、k の中の x を v で置き換えられることを示している。
補題 5 (継続の簡約に関する補題) 任 意 の 項 e1 、値 v 、trail t、schematic な継続 k1 について (k1 @ [[v]] @ t) →(k2 @ [[v]] @ t) が成り立つとき、[[e]] @ k1 @ t2 → [[e]] @ k2 @ t2が成り立つ。

h(λc. e1 ) @ (λx. E[x])i (RControl)→ v1(RPrompt)

RPrompt は、簡約する段階で prompt の中身が値になっており、prompt を外すことで簡約を進める。RControl の E はpure な評価文脈であり、Hole の中には、次に評価される項が入っている。RControl は control の c に control によって切り取られた継続を渡して e1 を実行する。RControl を使う例を示すと以下のようになる。
h1 + (Fc. c @ 1)i → h(λc. c @ 1) @ (λx. 1 + x)i

継続の部分を同じ意味を持つものに置き換えたい時に使う。
e → e′ が (λx. e1 ) @ v → e1 [x/v] の場合の証明では最後の簡約で使用した。
[[(λx. e1 ) @ v]] k t..
.

RControl は prompt の中身が、評価文脈の Hole に control が入ったコンテキスト、つまり「次に control を実行するという状態の項」である時に適用できる。例の簡約結果において、(λc. c @ 1) は control の中身である。(λx. 1 + x) はコンテキス
トの Hole を x に置き換えたものであり、control によって切り取られた継続になっている。(λc. c @ 1) に (λx. 1 + x) を適用することで c に切り取られた継続を渡して control の項を実行している。また、E[x] の周りに prompt をつけて hE[x]iとすると shift の簡約規則になる。
4.25→[[e′ ]] (λv. (λt′′′ . (λv. (λt′′ . k @ v @ t′′ ))) @ v @ t′′′ ) t→[[e′ ]] k t

まとめAgda を使って CPS インタプリタと CPS 変換を定式化することができた。CPS インタプリタと型規則を Agda に載せたことで CPS インタプリタ前後での型の整合性を証明することができた。また、今後は control の場合において正当性の証明に取り組む。

参考文献

正当性の証明[1] Kenichi Asai, Youyou Cong, and Chiaki Ishio. A functional abstractionof typed trails. In PEPM, 2021.

CPS 変換前の項を簡約した後に CPS 変換した項と、CPS変換後の項が β 同値であること、つまり以下の定理を示す。

[2] O. Danvy and A. Filinski. Abstracting Control. In Proc. 1990 ACM
Conference on Lisp and Functional Programming, pp. 151–160, 1990.
[3] O. Danvy and A. Filinski. Representing Control: a Study of theCPS Transformation. Mathematical Structures in Computer Science,Vol. 2, No. 4, pp. 361–391, 1992.

定理 2 任意の項 e, e′ について e → e′ が成り立つならば任意の schematic な継続 κ に対して [[e]] @ k @ t =β [[e′ ]] @ k @ t が成り立つ。

[4] Mattias Felleisan. The theory and practice of ﬁrst-class prompts. In
POPL ’88: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 180–190, 1988.

ここで =β は β 同値である。schematic というのは、「引数の変数の構造を変更しない」性質のことである。本稿で扱う
継続 k は値と trail の二つを受け取るため、次の二式がこの性質を表す。

(k @ x @ t)[v/x] =k@v@t(k @ v @ x)[t/x] =k@v@t[5] Chiaki Ishio and Kenichi Asai. Verifying selective cps transformation
for shift and reset. In William J. Bowman and Ronald Garcia, editors,Trends in Functional Programming, pp. 38–57, Cham, 2020. Springer
International Publishing.
[6] Urara Yamada and Kenichi Asai. Certifying cps transformation of letpolymorphic calculus using phoas. In Sukyoung Ryu, editor, Programming Languages and Systems, pp. 375–393, Cham, 2018. Springer International Publishing.

76