Agda による CPS 変換の正当性の証明
石尾 千晶 (指導教員：浅井 健一)
1

はじめにプログラミングにおける「継続」とは、計算中のある時点における残りの計算のことである。プログラム内で継続を明示的に扱う方法の一つに、プログラム全体を継続渡し形式 (Continuation-Passing Style; CPS)に変換するというものがある。CPS 変換をするとプログラム中の継続を管理できるため、コンパイラの中間言語に使われるなどの応用がある。
本研究は、より効率的な CPS 変換である selectiveCPS 変換 [1] の Agda [5] による定式化を試みる研究の一環であり、単純型付き λ 計算に限定継続命令shift/reset を加えた体系における selective CPS 変換の正当性の証明の定式化を目指している。本稿では、
単純型付き λ 計算を対象として、selective CPS 変換の基礎となる CPS 変換を Agda を用いて定式化し、その正当性を証明する [4]。定式化するにあたっては、変数束縛のある言語の抽象構文木を表現するための方法の一つである PHOAS (Parameterized Higher-OrderAbstract Syntax) [2] を用いる。また、selective CPS変換の正当性の証明に対する見通しを示す。

2型

τ::=

Nat | τ → τ値

v::=c | x | λx. e

項e ::=v | e1 e2

図 1: 単純型付き λ 計算

(λy. y)[v] 7→ v

(λy. x)[v] 7→ x

(λy. c)[v] 7→ c′∀x((λy. (e y) x)[v] 7→ e x)
(λy. λx. e y)[v] 7→ λx. e′(λy. e2 y)[v] 7→ e′2(λy. e1 y)[v] 7→ e′1(λy. (e1 y) (e2 y))[v] 7→ e′1 e′2
図 2: 代入規則

3

CPS 変換の定式化

Var : {τ1 : typ} → var τ1 → value[ var ] τ1  変数

本稿では、Danvy/Filinski による one-pass の CPS
変換 [3] を扱う。型の変換を図 5 に、値と項の変換を
図 6 に示す。 CPS 変換は、値の変換 [[v]]v と項の変換[[e]], [[e]]′ の３種類からなる。変換の結果は、アンダーラインのついた式とオーバーラインのついた式を使った 2 レベルの λ 計算で書かれている。アンダーラインのついた式は dynamic な式と呼ばれ、出力の構文を表す。一方、オーバーラインのついた式は static な式と呼ばれ、CPS 変換時にこれらの命令が実行されることを示す。static な命令は CPS 変換時に実行されるため、いわゆる administrative β -redex を生じることなく、コンパクトな CPS 変換結果を生成できる [3]。
[[e]] @ κ は、項 e を受け取ると、それを static な初期継続 κ のもとで CPS 変換した結果を返すことを意味する。このとき κ はメタ言語で書かれる関数であり、変換時に実行される。一方、[[e]]′ @ k は、項 e を受け取ると、それを dynamic な初期継続 k のもとで CPS変換した結果を返すことを意味する。このように 2 種類の変換を用意しているのは、CPS 変換時に継続がわかっている場合とそうでない場合があるためである。

Fun : {τ1 τ2 : typ} →  λ 抽象

4

単純型付き λ 計算の定式化

本稿で対象とする言語は純粋な単純型付き λ 計算に自然数を加えたものである。その型と構文を図 1 に示す。型は自然数型か関数型のいずれかである。値は変数・自然数・λ 抽象の 3 つからなり、項は値か関数適用である。これを Agda で書くと次のようになる。値と項は相互再帰的に定義されており、図 1 の規則をそのまま埋め込めていることがわかる。
data typ : Set where

Nat : typ  自然数型_⇒_ : typ → typ → typ  関数型
mutualdata value[_]_ (var : typ → Set) : typ → Set where
Num : (n : N) → value[ var ] Nat  自然数(e1 : var τ2 → term[ var ] τ1 ) →CPS 変換の正当性の証明

この節では、3 節で示した CPS 変換が正しいこと、
つまり CPS 変換をしても変換前の項と同等の β 簡約を行うことを示す。

value[ var ] (τ2 ⇒ τ1 )data term[_]_ (var : typ → Set) : typ → Set where
Val : {τ1 : typ} →value[ var ] τ1 → term[ var ] τ1  値定理 1 (CPS 変換の正当性) 任意の項 e, e′ についてe → e′ が成り立つなら、任意の schematic な継続 κについて [[e]] @ κ →∗ [[e′ ]] @ κ が成り立つ。

App : {τ1 τ2 : typ} →  関数適用
(e1 : term[ var ] (τ2 ⇒ τ1 )) →(e2 : term[ var ] τ2 ) → term[ var ] τ1

Agda では、依存型を使って「型 τ を持つ項」を表

これを Agda で書くと次のようになる。

現できるため、このように定義された構文のうち型が付くもののみを扱うこととなる。
また、図 2 に示す代入規則を定義する。(λy. e)[v] 7→e′ と書くと、「項 e の中に出てくる y を値 v で置き換えると項 e′ となる」と読む。さらに図 3 で項の評価規則のためのフレームと評価文脈を、図 4 で β 簡約規則を定義する。代入や簡約が行われる値と項は、図 1 のように相互再帰的に定義されているので、各規則もそれにしたがって相互再帰的な構造となる。

correctEta :{var : typ → Set} → {τ : typ} →{e e : term[ var ◦ cpsT ] τ } →′(κ : value[ var ] cpsT τ → term[ var ] Nat) →Reduce e e′

→ schematic κ →Reduce* (cpsEta e κ) (cpsEta e′κ)定理 1 は任意の κ について成り立つわけではない。
static な継続 κ が「引数の変数の syntactic な構造を変更しない」という性質を持っている必要がある。この3フレームF
評価文脈 E[ ]e | v[ ]= [ ] | F [E]

=Nat∗

=Nat∗

=

τ1 ∗ ⇒ (τ2 ∗ ⇒ Nat) ⇒ Nat(τ1 ⇒ τ2 )

図 3: 評価文脈(λx. e)[v] 7→ e′(λx. e) v → e′

図 5: 型の CPS 変換′e→eF [e] → F [e′ ]図 4: 簡約規則= x=((λx. λk ′ . [[e x]]′ @ k ′ ) @ [[v2 ]]v ) @ (λv. κ @ v)→

(λk ′ . [[e′ ]]′ @ k ′ ) @ (λv. κ @ v)

補題 1→[[e′ ]]′ @ (λv. κ @ v)

補題 2= λx. λk. [[e]]′ @ k[[v]] =[[e1 @ e2 ]] =[[v]]′′[[e1 @ e2 ]]λκ. κ @ [[v]]v
λκ. [[e1 ]] @ (λm. [[e2 ]] @(λn. (m @ n) @ (λa. κ @ a)))= λk. k @ [[v]]v= λk. [[e1 ]] @(λm. [[e2 ]] @ (λn. (m @ n) @ k))

図 6: 単純型付き λ 計算の CPS 変換
れ以外の項と値は pure であるといい、answer type は変化しない。このように全ての項と値を pure またはimpure に分類し、注釈をつけて定式化する。3 節のCPS 変換では無条件に全ての値と項を変換の対象としたが、selective CPS 変換は impure な項のみを対象として変換を行うため、より効率的である [1]。
shift/reset を導入した体系で定式化を行うには、answer type についての各種の証明が必要となる。また、与えられた項が pure か impure かによっても場合分けが必要である。

′→ [[e ]] @ κ
補題 3
式中の β 簡約で以下の補題を利用することで、式をそのまま Agda のコードにすることができている。

6

まとめと今後の課題
単純型付き λ 計算における Danvy/Filinski の one-

補題 1 (CPS 変換と代入演算の可換性 1) 任意の項
e, e′ 、値 v 、dynamic な継続 k について (λy. e y)[v] 7→ e′が成り立つとき、(λy. [[e y]]′ @ k)[[[v]]v ] 7→ [[e′ ]]′ @ k が成り立つ。

pass の CPS 変換を定式化し、その正当性を Agda で示した。定式化の方法に PHOAS を採用することで変数束縛による証明の複雑化を避け、手で書いたものとほぼ対応した証明を書くことができた。また、shift/resetの入った体系での selective CPS 変換の定式化への見通しを示した。今後、selective CPS 変換を定式化し証明を完成させたい。

補題 2 (CPS 変換と代入演算の可換性 2) 任意の項
e、値 v 、dynamic な継続 k について
(λk. [[e y]]′ @ k)[v] 7→ [[e y]]′ @ v が成り立つ。

参考文献

base case の最後に現れる →∗ では、e′ の構造によっ[1] K. Asai and C. Uehara. Selective CPS Transformation for Shift and Reset. Proceedings of the ACM SIG-て簡約のステップ数が異なるため以下に示す補題 3 で別途証明をしている。e′ が値のときは 1 ステップの簡約が必要で、そうでないとき簡約は必要ない。以上より、定理 1 で [[e]] @ κ を 2 ステップもしくは 3 ステップ簡約することで [[e′ ]] @ κ に到達することがわかる。

PLAN Workshop on Partial Evaluation and ProgramManipulation (PEPM'18), pp. 4052, 2018.

[2] A. Chlipala. Parametric Higher-Order Abstract Syntax for Mechanized Semantics. Proceedings of theACM SIGPLAN International Conference on Functional Programming (ICFP'08), pp. 143156, 2008.

補題 3 (0 または 1 ステップの簡約) 任意の項 e、schematic な継続 κ について [[e]]′ @ (λv. κ @ v) →∗[[e]] @ κ が成り立つ。

5= c[[λx. e]]v

性質を schematic であるといい [3]、次のような式で示すことができる。
(λy. κ @ y)[v] 7→ κ @ vつまり、κ に y を渡した結果の項の y の部分に v を入れたものは、最初から κ に v を渡したものと等しくなるということである。
定理 1 の証明の概略を示す。定理 1 は、e → e′ の構造によって場合分けをして証明する。最初の場合分けは帰納法の base case に相当し、e が (λx. e1 ) @ v の形のとき β 簡約をする。残りのケースはフレームの中が簡約される場合で、フレームの形によってさらに場合分けし、どちらも再帰する形で証明する。base case の証明は以下のようになる。
[[(λx. e1 ) @ v]] @ κ∗[[c]]v[[x]]v[3] O. Danvy and A. Filinski. Representing Control:a Study of the CPS Transformation. MathematicalStructures in Computer Science, Vol. 2, No. 4, pp.
361391, 1992.

selective CPS 変換の定式化に向けて
selective CPS 変換では、限定継続命令 shift/reset[4] 石尾千晶, 山田麗, 浅井健一. Agda による PHOAS を用いた CPS 変換の正当性の証明. 第 20 回プログラミンを導入する。shift はその時点の継続を切り取ってくる命令で、reset は切り取られる継続の範囲を限定する命令である。shift を使った項を impure な項と呼び、現在のコンテキストの型をあらわす answer type が変化する可能性があることを意味する。部分項が impureである場合は、項全体が impure であるとみなす。そグおよびプログラミング言語ワークショップ論文集掲載
予定, 2018.

[5] A. Stump. Veried Functional Programming in Agda.
Morgan & Claypool, 2016.

4