定理証明系を用いた強正規化性の証明と評価器の抽出
廣田知子(指導教員：浅井健一)
one-step reduction rule:

概要1

信頼性の高いプログラムを得る一つの手法として、定理証明系を用いて実行結果の存在定理を証明し、そこからプログラムを抽出する方法がある。これによっ(λ.e) v
e1 e2; ev; e01 e2v e2; v e02て得られたプログラムはその正当性が保証されているが、一方でプログラムの抽出を行うのは簡単ではない。

if e1 ; e01
if e2 ; e02

ここで ev は e の中に含まれる束縛変数 0 に v を代入

そこで本研究では、プログラム抽出を容易に扱えるしたものを表している。

方法を探る一環として、評価器を抽出して知見を得る

big-step reduction rule:

ことを目指した。（評価器は、プログラムをそれ以上e ;∗e1 ;∗e1 ;∗評価出来なくなるまで β-簡約を行うプログラム変換器を指す。）まず単純型付き λ 計算を定理証明系 Coq を用いて定式化し（定式化方法は [1] を参考にした）、次に、論理述語を用いての Tait による強正規化性の証明[5] を Coq で定式化することにより、正当性が保証さ

4.3

型付け規則

ok Γ (x : T ) ∈ Γ(var)
Γ`x:T

強正規化性
強正規化性とは、プログラムを任意の順序で β-簡約

∀x ∈/ L. Γ, x : T1 ` ex : T2(f un)Γ ` λ.e : T1 → T2

していっても必ず簡約が停止する性質のことである。
ただし本研究では call-by-value left-to-right の簡約規Γ ` e1 : T1 → T2 Γ ` e2 : T1(app)Γ ` e1 e2 : T2則を採用したため、簡約順序は一意に決まる。

Locally Nameless 手法3if e1 ; e2if e1 ; e2 , e2 ;∗ e3

本稿では、型規則は Γ ` e : T のように表記する。

れた評価器を Ocaml のプログラムとして抽出した。

2ee2e3

本研究では Locally Nameless 手法を用いて λ 抽象を

例えば (var) の規則は「Γ ` x : T が成り立つため定義した。この手法は、α-equality の問題を解消するには環境 Γ が ok であり、かつ x が T 型を持つというための、変数の名前付けの方法であり、自由変数には情報が Γ に含まれていなくてはならない」という意味

x, y, ... 等の名前を付け、束縛変数には名前を付けずにを表す。Γ が ok であるとは、Γ 中に現れる変数名がde Bruijn index を用いて表現する。de Bruijn index
は変数を 0 以上の整数で表し、その式における一番内全て異なることを意味している。又、(f un) に現れる∀x ∈/ L. は L に含まれない x（自由変数）を表し、こ側の binder の変数名を 0 と考え、外にいくに従っての L には何も制限を付けていないので、自分で自由に0, 1, 2,... と大きくしていくという表現方法である。例
えば λ 計算式の λx.λy.λz.y x w z は Locally Nameless

変数とするのでなく、このように L に関してのみの制手法を用いて表すと、λ.λ.λ.1 2 w 0 となる。

限にとどめることにより、証明木を作成する場合等、L を定めることが出来る。x を他のどこにも現れない型付け規則に関わる証明を行う際の複雑さを軽減することが出来る。本研究では定理 3 の証明において使用

単純型付き λ 計算

4した。

本研究で使用したシステムは以下の通り。

4.1

項:
値:e := nv
型: T
4.25構文(束縛変数) | x (自由変数)| λ.e (λ抽象) | e1 e2 (関数適用):= x| λ.e:= A
| T1 → T2

簡約規則 (call-by-value left-to-right)

停止性 N と論理述語 R
簡約の停止性を述語 N を用いて定義し、論理述語 R

は N と型に関する帰納法を使って定義した。
定義 1 (停止性)N (e) ⇐⇒ e ;∗ v となるような値 v が存在する
定義 2 (論理述語 R)
・RA (e)∗one-step reduction ; と big-step reduction ; の定義を以下に示す。

⇐⇒ N (e)・RT1 →T2 (e) ⇐⇒ N (e) であり、かつ任意の項 e0 について RT1 (e0 ) ならば RT2 (e e0 ) が成り立つ

では、λ 抽象の body 部分をみるときに束縛変数を置きTait による本来の定義では「RT (e) において e の型は T である」の条件が付加されているが、本研究ではその制約をもうけていない。強正規化性を示す際に定項に関する帰納法をかけにくい。故に今回はやむなく理の条件部に型規則の成立を入れているため、そこで型付け規則に関する帰納法を用いた。

換えているため、単純な subterm にはなっておらず、そして停止性を示す強正規化性の定理は以下である。

e と T の関係性を示すことになり、論理述語にその定義を入れる必要がないからである。

6

Coq による定式化

λ 計算の構文や型、簡約規則、型付け規則等は全てInductive コマンドを用い、再帰を持つデータ型とし定理 4 (強正規化性) ` e : T ならば、N (e)[証明] 定理 3 により、e が RT (e) を満たすことが言え、故に、定理 1 によって N (e) が導ける。28プログラムの抽出て定義した。述語 N の定義には Deﬁnition コマンド定理 4 に関して Extraction コマンドを用いることにを用いたが、その際、N の返す型は、プログラム抽出より、Ocaml のプログラムの抽出を行った。その結果、を行うため、関数の型を表す Set 型とした。又、論理構文・型付け規則・N ・R はデータ型として、そして述語 R の定式化に関しては、通常ならば Inductive コ定理 2・3 がサブ関数として、定理 4 が評価器の関数とマンドを使い、データ型として定義するところだが、して抽出された。簡約規則・定理 1 は定義としてはプ

R の再帰が negative に現れてしまい（含意の前件部の前提に相当する部分に「任意の x に対して自身の定義が成り立つ」という条件が現れてしまう）、Coq ではログラムには書かれず、吸収された形になっている。

9

まとめと今後の課題

データ型として定義出来ないため、Type 型を返す関本研究では単純型付き λ 計算における強正規化性の数として R を定義した。
（[2] においても同様の手法が証明を Coq で定式化することによって評価器をプログ取られている。）なお、簡約規則の返す型は Prop 型でラムとして抽出した。今後は、本研究の発展として、定義したが、型付け規則の返す型は N と R の定義に部分評価器の抽出や、λ 計算に let 文と継続を扱う命合わせ、Set 型とした。

7

強正規化性の証明[5] で述べられている Tait の方法を参考に、Coq を用いて証明の定式化を行った。以下はその主となる定理である。
定理 1 RT (e) ならば、N (e)定理 2 e ;∗ e0 のとき、RT (e) と RT (e0 ) は同値
定理 3 x1 : T1 , ..., xn : Tn ` e : T かつ v1 , ..., vn について RT1 (v1 ), ..., RTn (vn ) が成り立つとき、RT ([x1 7→v1 ]...[xn 7→ vn ] e)定理 1 は R の定義により成立、定理 2 は型 T に関する帰納法で、そして定理 3 は途中で定理 2 を使いつつ、型付け規則の導出における帰納法を用いて証明を行った。

Coq での証明において、ある式に関する帰納法を使うと、抽出された関数ではその部分を、その式に関する場合分けを行うよう定義される。故に定理 3 の証明
方法だと、プログラムとして抽出したときに型付け規

令 shift/reset を導入した型システムにおける強正規化性の証明 [3] を用いた評価器の抽出を行う予定である。

参考文献[1] Aydemir, B., A. Charguéraud, B. C. Pierce,
R. Pollack, and S. Weirich “Engineering Formal Metatheory,” Conference Record of the 35th
Annual ACM Symposium on Princeples of Programming Languages, pp. 3–15 (January 2008).
[2] Berger, U., S. Berghofer, P. Letouzey, and H.
Schwichtenberg “Program extraction from normalization proofs,” Studia Logica 82, pp. 25–49(February 2006).
[3] Biernacka, M., and D. Biernacki “Contextbased proofs of termination for typed delimitedcontrol operators,” 11th International ACM
SIGPLAN Symposium on Principles and Practice of Declarative Programming (September2009).

則で場合分けを行うよう定義されてしまい、型付け規則が関数の引数としてどうしても必要になってしまう。

[4] Biernacka, M., O. Danvy, and K. Støvring

これにより、出来れば、項とその型を引数として渡せ“Program extraction from proofs of weak headnormalization,” Electronic Notes in TheoreticalComputer Science 155, pp. 169–189 (May 2006).

ば簡約を行ってくれるような評価器を抽出したいところだが、そうはならず、型付け規則を引数として必要とする評価器が抽出されることとなる。このような理由から、本当ならば定理 3 の証明は項に関する帰納法を用いて行うのが望ましいが、locally nameless 手法[5] Pierce, B. C. Types and Programming Languages, Cambridge: MIT Press (February 2002).