論理関係によるスタック導入の正当性の証明
新井祐美

1(指導教員：浅井健一)

はじめにすべての関数を末尾呼出しにすることを言う。eval1 とeval2 はともに CPS で書かれている。

本研究では、先行研究 [1] で提案されているプログ
ラム変換の一手法であるスタック導入について、論理関係を用いてその前後の等価性を証明する。
スタック導入とは、より現実の機械に近い形式の抽象機械を導出するためのプログラム変換であり、これによってプログラム中の関数呼出しは、値の受け渡しをスタックの先頭で行うように書き換えられる。証明の方針は、まずスタック導入前後の値についての対応を論理関係 [2] として定義し、入力データの構造についての帰納法によって、両者の出力結果が（論理関係の意味で）等しいことを示していく。
これにより、CPS の λ 計算のインタプリタにスタック導入することの正当性が保証される。

24.2

λ 計算は、関数の計算に関する理論である。
本研究では、整数型を基本型とし、以下のように定義される型付きの λ 式を入力言語としている。
項 : t := n（整数）| x（変数）| λx.M（λ抽象）| M N（関数適用）
型 : T := int | T1 → T2
また、型付け規則は以下の通りである。
Γ ` n : int

Γ, x : T1 ` M : T2

スタック導入Γ ` λx.M : T1 → T2
Γ ` M : T1 → T 25（λ 抽象）Γ ` N : T1（関数適用）定理

図１に示した eval1 と eval2 の等価性を示すために、まず、次の定理を証明する。
定理：Γ ` t : T と型付けされた λ 式 t について、

RA ((eval1 t env1 cont1 ), f st(eval2 t env2 stack cont2 ))ただし、
1. ∀x ∈ dom(Γ) について、RΓ(x)∗ (env1 (x), env2 (x))
2. stack は任意のリスト
3. RT ∗ →A (cont1 , cont2 )4. T ∗ は継続の型であり、以下の定義に従う。
- (int)∗ = int- (T1 → T2 )∗ = T1∗ → (T2∗ → A) → A
A : Answer T ype
5. f st() はリストを受け取ったらその先頭の要素を返す関数とする。

論理関係

また、論理関係 RT は、次のように定める。

1. R(int)∗ (t1 , t2 ) ⇔ ∀n : int について、
t1 = V Int1 (n) かつ t2 = V Int2 (n)2. RT1∗ →A (k1 , k2 ) ⇔ ∀(v1 , v2 ) ∈ RT1∗ 、∀s について、RA (k1 v1 , f st(k2 (v2 :: s)))CPS の λ 計算のインタプリタ

3. R(T1 →T2 )∗ (V F un1 (f1 ), V F un2 (f2 ))⇔ ∀(v1 , v2 ) ∈ RT1∗ 、∀(k1 , k2 ) ∈ RT2∗ →A 、∀s について、RA ((f1 v1 k1 ), f st(f2 (v2 :: s) k2 ))本論で扱った CPS の λ 計算のインタプリタ eval1 お
よび eval1 にスタック導入を施した eval2 の振る舞いを図１に示した。

4.1

（変数）

Γ ` M N : T2

本研究では、論理関係を用いた証明の手法を採用した。この手法は、型付きの言語を対象としている。
まず型に関する帰納法によって、等価性を保証するための関係を定義する。そして、関係性を示したい２つの項がともに定義した関係を満たしていれば、それらは等価であるということが証明できる、というもの
である。

4（整数）

Γ, x : T1 ` x : T1

先行研究は、限定継続処理のオペレータ shift / resetに関して、正当性の保証された処理系を与えることを目的としている。その手法として、CPS の λ 計算のインタプリタにスタック導入を含む各種プログラム変換を用いて、より抽象機械の動作に近いインタプリタを導出し、機械語での限定継続処理実装のための正当性の保証のあるモデルを提案しようとしている。
スタック導入前のインタプリタでは、値はそれを取る継続ごとに保持されているが、一般的な機械語ではスタックに中間結果を保存するようになっている。このため先行研究では、新たに評価器に引数としてスタックを持たせ、値をスタックに積んで受け渡すように変更し、このプログラム変換をスタック導入と呼んでいる。
スタック導入前後のインタプリタについて、型無しの言語を入力した場合、両者で同じように実行が進むことが先行研究において証明されているが、本研究では、型付きの言語を入力した場合、結果が等しいということを証明する。

3

λ 計算

RT は型 T に関して帰納的に定義されている。これは前節の T の構造に従っているので、すべての入力言語について論理関係が定義できていることがわかる。

CPS（継続渡し形式）

継続とは、計算が終わったあとにする処理のことである。継続渡し形式は、継続を引数として渡すことで、

61eval1 n env1 cont1 Ã cont1 (V Int1 (n))
eval1 x env1 cont1 Ã cont1 (env1 (x))

eval2 n env2 stack cont2 Ã cont2 (V Int2 (n) :: stack)eval2 x env2 stack cont2 Ã cont2 (env2 (x) :: stack)eval1 (λx.M ) env1 cont1
Ã cont1 (V F un1 (f un v1 k1 →eval1 M (x, v1 ) :: env1 k1 )eval2 (λx.M ) env2 stack cont2
Ã cont2 (V F un2 (f un (v2 :: s) k2 →eval2 M (x, v2 ) :: env2 s k2 )eval1 M N env1 cont1
Ã eval1 N env1 (f un v2 →eval2 M N env2 cont2
Ã eval2 N env2 stack (f un s1 →eval1 M env1 (f un v1 →match v1 withV F un1 (f1 ) → f1 v2 cont1

eval2 M env2 s1 (f un s2 →match s2 withV F un2 (f2 ) :: v20 :: s → f2 (v20 :: s) cont2| → raise Error| → raise Error
図 1: eval1 , eval2 の振る舞い

eval1 と eval2 では継続の型が違うので、等価性を考えることが難しくなる。しかし、両者の関係性を定義する論理関係を用いることにより、入力言語の性質そのものについて議論できるようになるため、この問題は解消される。

67

スタック導入の正当性の証明

５節の定理を証明できたことにより、次の系を得る。
系：` t : int と型付けされたプログラムについて、

eval1 t φ id = f st(eval2 t φ [] id)
ただし、id は恒等関数である。

証明

t の構造についての帰納法により、各入力に対する出力が定義した論理関係を満たしていることを示す。

証明
命題は、前定理に関して、型環境 Γ、環境 env1 、env2および stack が空、初期継続が id の場合であると言える。
今、Γ が空であるから、x ∈ dom(Γ) を満たす x が存在しないため、前定理の環境についての前提を満たす。
また、∀(v1 , v2 ) ∈ R(int)∗ 、∀s について、Rint ((id v1 ), f st(id (v2 :: s))) が成り立つので、R(int)∗ →int (id, id) となり、これは前定理の継続についての前提を満たす。
よって、前定理よりこれは成り立ち、スタック導入の正当性が証明された。

(1) t = n, T = int（整数）のとき
論理関係１および env1 , env2 についての前提より、論理関係２が適用できて、RA (cont1 (V Int1 (n)), f st(cont2 (V Int2 (n) :: stack)))(2) t = x, T = Γ(x)（変数）のとき
env1 , env2 および cont1 , cont2 についての前提より、論理関係２が適用できて、RA (cont1 (env1 (x)), f st(cont2 (env2 (x) :: stack))))(3) t = λx.M, T = T1 → T2 （λ 抽象）のとき
実行結果を cont1 (V F un1 (f1 ))、cont2 (V F un2 (f2 ) ::stack) とおく。
f1 , f2 に ∀(v1 , v2 ) ∈ RT1∗ 、∀(k1 , k2 ) ∈ RT ∗ →A 、∀sを渡すことを考えれば、型に関する帰納法の仮定が使える。
論理関係３より、R(T1 →T2 )∗ (V F un1 (f1 ), V F un2 (f2 ))である。
また、cont1 , cont2 についての前提より、論理関係２が適用できて、RA (cont1 (V F un1 (f1 )), f st(cont2 (V F un2 (f2 )::stack)))(4) t = M N, T = T2 （関数適用）のとき
型に関する帰納法の仮定より、Γ ` M : T1 → T2 、
Γ ` N : T1 が得られる。各継続に ∀(x1 , x2 ) ∈ RT1∗ 、∀s を渡すことを考えれば、帰納法の仮定を使うための前提条件が満たされるので、RA ((f1 v2 cont1 ), f st(f2 (v20 :: s) cont2 ))8

まとめと今後の課題

CPS の λ 計算のインタプリタにスタック導入を用いるとき、入力される λ 式が型付けされており、値が整数であれば結果は等しいということを証明した。今後
は、先行研究の本題である限定継続命令を含めたインタプリタへのスタック導入の正当性を確かめたい。今回見てきたインタプリタで限定継続命令を扱えるようにするためには、対象言語に shift と reset を付け足すことになるため、本論で定義した論理関係ではすべての入力を網羅することができない。しかし、限定継続を表す項の性質をよく観察し、スタック導入前後の対応を記述する論理関係を定義することができれば、本論と同様に証明できると予想される。

参考文献

以上より、Γ ` t : T と型付けされた入力に対して、RA ((eval1 t env1 cont1 ), f st(eval2 t env2 stack cont2 ))が成り立つ。

62[1] 木谷有沙, 浅井健一. 「仮想機械導出のためのプロ
グラム変換」. 第 12 回プログラミングおよびプロ
グラミング言語ワークショップ (PPL2010) 掲載予定, January 2010.
[2] 萩谷昌己, 西崎真也. 論理と計算のしくみ. 岩波書店, 2007.