全文 - 東京工業大学電子図書館

定理証明支援系によるプログラム検証の
対話的修正に関する研究
東京工業大学
大学院情報理工学研究科
計算工学専攻
渡部研究室 09D38059
森口 草介
平成 24 年度 博士論文
i
概要
本研究の目的は、定理証明支援系を用いて検証したプログラムを、漏れなく確
実に拡張する手法の考案である。より具体的には、Coq によって検証したプログ
ラム（以下検証付きプログラム）に対し、宣言した型に対するコンストラクタの
拡張のみを許すことで、その影響を網羅的に検出する手法である。検出した箇所
を対話的に修正することにより、拡張時の見落としをなくし、拡張後のプログラ
ムに対する信頼性を維持することができる。
定理証明支援系によるプログラムの検証は非常に強力だが、その反面全体のサ
イズが大きくなる傾向がある。この検証は記述した仕様を厳密に満たすことを証
明することで行われる。一方で、厳密な仕様記述は難しく、仕様のサイズは大き
くなりがちである。そのため、プログラマがプログラムと仕様の全体を把握する
ことが難しくなる。
しかし、検証付きプログラムでは、簡単な変更であっても全体を把握していな
ければならない場合がある。これは、プログラムと仕様、証明の記述が相互に強
く依存しているため、一部の変更が全体に波及していくためである。この波及は、
データ型の種類の追加といった単純なものであっても発生しうる。全体に横断し
た変更は見落としなどのヒューマンエラーを誘発する原因となる。
この問題に対し、既存研究では大きく二種の研究によって解決を試みている。一
つはこれら波及箇所に対する修正を可能にする研究である。これには例えばアス
ペクト指向やメタプログラミングなどが挙げられる。しかしこれらの研究では、修
正を可能にするものの、波及箇所について言及する手法は提案されていない。
もう一つは変更可能な箇所を事前に決めることで波及箇所をより限定する手法
である。これはデータ型の宣言や関数などの処理の宣言を特殊な形式で行うこと
で、修正の記述を可能にする。この記述は、事前に想定していた変更に対する影
響を比較的容易に限定することができる。一方で、変更可能な箇所は事前に想定
した範囲にとどまるため、想定されない箇所の変更はたとえ単純な変更であって
も許されない。この問題を解決するには全ての変更可能な箇所を特殊な宣言にす
る必要がある。その結果、波及箇所の限定には用いることができなくなり、また
記述が煩雑になるというデメリットが生まれる。さらに、宣言は単純に変更可能
な箇所を示すため、ある変更に対する波及箇所を限定することはできない。
ii
これらに共通することは、ある特定の変更の影響を分析する研究は十分でない
という点である。影響に関する見積もりは change impact analysis などの研究で行
われているが、波及箇所を限定できるほど正確な分析は存在しない。
本研究ではこの問題に対して、可能な変更を限定し対話の形で行うことで、変
更の種類の限定を行う。変更の種類を限定することで、より文法上の影響を考慮
しやすくなり、影響箇所をより限定することができる。また、検証も同様に拡張
することで、その拡張が元の検証した性質を保っていることを保障する。この機
構を、本研究では対話的修正機構と呼ぶ。
本論文では、定理証明支援系 Coq に対し、既存の帰納型に新たなコンストラク
タを追加する命令を追加し、それにより受けた影響を検出する手法を提案する。帰
納型へのコンストラクタの追加では、関数におけるパターンマッチや帰納法を用
いた記述に対し、網羅性が満たされなくなるという形で影響を与え、またそのほ
かにその帰納型に関する性質を記述する述語も影響を受けうる。これらの影響の
うち、パターンマッチの網羅性は多くの関数型言語における検査の対象であり、比
較的容易に検出することが可能だが、述語の検出は本質的に難しい。本論文で提
案する手法では、述語についてプログラマへ提示することで、プログラマが変更
すべき箇所を認識することを可能にしている。
この手法をそのまま用いた場合、実用的でない数の検出が行われる場合がある
ため、その解決として拡張前の記述を用い、検出箇所を最適化する手法も提案す
る。対話的修正機構による検出は影響を受けた箇所の網羅を目的としているため、
プログラムを直接変更する場合は変更の必要のない箇所であっても変更を要求す
る。特に証明は記述と内部表現が異なり、内部表現では難読な検出箇所を多数持
つ。ここでは、拡張前の証明の記述を再実行することで検出箇所を最適化する。こ
の最適化によりプログラムを直接変更する場合と遜色ない検出数となり、本手法
を実用的なツールとして実現できることが確かめられる。
また、本論文では、対話的修正機構で作成した複数の独立した拡張を一つのプ
ログラムに対して適用するための手法を提案している。対話的修正では、修正箇
所を順序によって表現しているため、合成を機械的に行うことは難しい。提案手
法では、修正を表した項を定義することにより、修正箇所を明示する仕組みを提
供し、これらの項を集めたモジュールを定義する。対話的修正機構を用いてこの
モジュールを作成することで、プログラムに対して複数の拡張を適用することが
可能になる。
iii
目次
第1章
1.1
1.2
1.3
序論
背景 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
目的と貢献 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
本論文の構成 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
第2章
2.1
本研究の背景
Coq . . . . . . . . . . . . .
2.1.1 Coq の概要 . . . . .
2.1.2 pCIC . . . . . . . .
2.1.3 Ltac . . . . . . . . .
問題：拡張に対する指摘 .
2.2.1 初期プログラム . .
2.2.2 拡張 . . . . . . . . .
既存研究の問題 . . . . . .
2.3.1 Expression problem
2.3.2 既存手法 . . . . . .
2.2
2.3
第3章
3.1
3.2
3.3
3.4
3.5
3.6
対話的修正機構
対話的修正機構の挙動 . . .
形式的定義 . . . . . . . . .
3.2.1 帰納型の提案 . . .
3.2.2 拡張の適用 . . . . .
型拡張の制限 . . . . . . . .
3.3.1 パターンマッチの型
3.3.2 ソート多相 . . . . .
拡張の健全性 . . . . . . . .
帰納原理関数 . . . . . . . .
使用例と問題点 . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1
1
3
5
.
.
.
.
.
.
.
.
.
.
7
7
8
12
17
18
18
20
25
25
27
.
.
.
.
.
.
.
.
.
.
33
33
36
36
37
38
39
41
42
45
48
iv
第4章
4.1
4.2
4.3
記述の再利用
問題点 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
関数の補完 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
証明の補完 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
51
51
52
54
第5章
5.1
5.2
5.3
5.4
拡張のモジュール化
拡張の衝突 . . . . . . . . . . . . .
拡張モジュール . . . . . . . . . .
対話による拡張モジュールの作成
複数のモジュールの合成 . . . . .
.
.
.
.
63
63
64
65
69
第6章
6.1
6.2
6.3
6.4
関連研究
関数型言語 . . . . . . . .
機能指向プログラミング
アスペクト指向 . . . . .
Coq の検証手法 . . . . . .
.
.
.
.
71
71
72
73
74
第7章
7.1
7.2
結論
まとめ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
残された課題 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
77
77
78
.
.
.
.
付 録 A While 言語とその最適化器
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
87
1
第 1 章 序論
1.1 背景
定理証明支援系は命題の証明を補助するためのシステムである。定理証明支援
系には大きくわけて対話的証明支援系と自動証明器が存在する。自動証明器では
機械的な命題の証明を試みるが、一方で対話的証明支援系では証明の流れを全て
人間が記述する。これらにはそれぞれに利点と欠点が存在する。証明が容易な命
題に対しては自動証明器により即座に証明が行われるものの、ある程度以上複雑
な命題になると補題を適宜示す必要がある。対話的証明支援系では、複雑な命題
も人間が指示を出すため、結果としてはそれほど自動証明器との差がない。
定理証明支援系は、命題にプログラムへの言及を行うことでプログラムの検証
に利用できる。このときプログラムは証明支援系において記述可能なプログラム
である必要がある。また、証明の複雑さは命題として記述したプログラムの性質
やプログラム自体の内容によって大きく異なる。
定理証明支援系をプログラムの検証に用いるという試みは長く続けられている
が、近年までは現実的なプログラムに対する検証は行われていなかった。これは、
実用的プログラムが満たすべき性質の記述の規模が非常に大きかったためである。
そのため、検証されたプログラムは小さなサンプルにおける検証にとどまり、実用
に耐えうるプログラムに対しては行われなかった。しかし、近年いくつかのプロ
ジェクトにおいて実用的プログラムに対しての適用が試みられている [7, 9, 12, 37]。
プログラムとその検証を行うためのコード（以下検証コード）をまとめて検証
済みプログラムと呼ぶ。定理証明支援系を用いた検証済みプログラムでは、検証
を行うためのコードは性質の記述およびその証明に当たる。 このとき、検証コー
ドとプログラムの間には非常に強い依存関係が存在する。一般に、プログラムで
はデータ構造とそれに対する処理が互いに依存する傾向があるが、これらの依存
性は一方の変更が他方に影響を与える。これは検証コードとプログラムの間にお
ける依存関係も同様であり、結果として、プログラムの変更はプログラム内部で
の依存性の他に検証コードへの依存性も考慮しなければならない。
また、検証済みプログラムでは、検証を段階的に行うためにプログラムをいく
つかの処理に分けることがある。例えば CompCert プロジェクトは C のサブセット
第1章
2
序論
をサポートするコンパイラを作成するプロジェクトだが、このコンパイラには複
数の中間言語が含まれている。これは、段階を追ってコンパイルを進めるためで
あり、例えば変数のスタック割り当てや、有限のレジスタに対する割り当てを行
うなどをそれぞれの中間言語で変換する。この手法により、検証において変換し
ていない箇所を言及する必要がなくなり、変換箇所への言及に注力することがで
きる。
しかし、複数の段階に分けたために、機能拡張時に全ての段階に横断して変
更しなければならない場合がある。例えば CompCert プロジェクトから派生した
CompCertTSO[32] では、スレッドによる並列を導入しているが、そのためにメモ
リモデルへスレッドイベントを追加し、また命令としてスレッド生成を追加して
いる1 。これらを追加する対象は C 言語から一定の形式の記述へ変更した Clight と
いう中間言語だが、イベントや命令の追加はそれ以降の中間言語全てにも行われ
ている。これは、元の CompCert プロジェクトにおいて検証した際に、意味論の記
述にこれらの概念が存在しなかったためである。
このように、変更による影響が横断する場合がある一方で、変更の影響がそれ
ほど広がらない場合もある。例えば同様に CompCert プロジェクトから派生したも
のとして、意味論の記述を実行可能なプログラムにすることでテストなどを通じ
た検査を可能にしたもの [5] では、主に C の意味論の記述の変更のみが必要であ
り、Clight への変換手法とその証明は変更されているが、それ以降の中間言語には
影響を及ぼさない。このように、ある検証済みプログラムを変更した結果影響を
受ける箇所は、元の検証済みプログラムで性質が表現可能か、などに非常に強く
依存し、拡張そのものだけでは判断出来ない。
このように、機能の拡張による変更は広く波及する場合もあるが、必ずしも全
体に波及するわけではない。波及の範囲は検証済みプログラムと拡張の二つに依
存するため、範囲を把握するには検証済みプログラムの理解が必要となる。しか
し、検証済みプログラムの規模は通常のプログラムに比べ検証コードによって可
読性、保守性が低下する。特に対話的証明支援系による検証コードは通常のプロ
グラムの 10 倍を超える規模となることもある [22]。このことから、範囲の認識は
容易ではないといえる。
範囲の認識を行う代わりに、範囲を狭める方法を考えることもできる。一般に関
心事の分離を行うと、プログラムに施した機能拡張の影響が分離した関心事にと
どまることが多く、保守性の向上が見込まれる。一方で、上記で説明したモジュー
ルに横断する変更は、単一のモジュール単位では関心事の分離が行いにくい。
このような変更は横断的関心事の一種であり、アスペクト指向などが対象とし
1
そのほかにも意味論を変更するなどしている。論文が発表された当時は CompCert は big-step
semantics を使用していたが、現在は small-step semantics になっているため、現在は論文で主張さ
れるほどには変更されないと考えられる。
1.2. 目的と貢献
3
てきた問題である [21, 17]。特にジョインポイントモデル [20] では、通常の関数や
メソッドとは別にアドバイスを記述することでこれらの挙動を変更する。アドバ
イスは外部に存在する関数やメソッドに対して変更を行うため、複数のモジュー
ルの変更に関するアドバイスを行うことができる。
また、データ構造や関数を常時拡張可能にすることで横断的な変更を行うこと
もできる [36, 15, 24]。この手法では、既存のモジュールを超えてプログラムに必
要な箇所を拡張できるため、横断的な変更にも対応することができる。これはモ
ジュール化とは異なるが、本質的にアスペクト指向における拡張と同種と見るこ
とができる。
これらの手法は、可能な拡張の記述の柔軟性に重点を置いている。このように、
拡張に関する記述可能性は広く研究されている問題であるといえる。一方で、こ
れらによる拡張箇所は全てプログラマが記述する必要がある。したがって、漏れ
なく拡張を行うためには拡張の必要な箇所全てをプログラマが理解していなけれ
ばならない。
しかしながら、プログラムの大きさの問題から、一般にプログラマはプログラ
ム全体を把握できるわけではない。多くの場合、修正を行うプログラマは、一部の
修正箇所のみを知っているだけであり、把握できていない箇所も多い。この場合、
何らかの方法によりプログラマが残りの修正箇所を知る方法が必要となる。依存
性解析を用いることで、影響を受ける箇所を分析する手法も提案されている [30, 2]
が、これらは基本的に値間の依存性を見ているため、型の変更に対して過剰に影
響を見積もるか過小に見積もってしまい、正確に影響箇所を判定することは難し
い。その結果、型や論理に基づいて記述される検証付きプログラムには適用が難
しい。
対話的証明支援系における検証では、プログラムと検証する仕様が同じ言語で
記述されるため、仕様における修正漏れはプログラムの修正漏れと同様の原因で
発生しうる。プログラムの中に修正漏れが存在し、かつ検証を通過した場合、こ
の修正漏れがバグとなる。多くの場合、修正漏れは検証時に発見されるが、検証
の記述が同時に修正漏れを起こした場合、通過してしまう可能性がある。このこ
とから、検証付きプログラム全体に対して、確実に修正すべき箇所を検出する手
法が必要である。
1.2 目的と貢献
本研究では、以上の問題に対して以下の二点を目的として手法を提案する。
• 修正が記述可能であるだけでなく、修正箇所を提示する。多くの場合プログ
4
第1章
序論
ラマが知る修正箇所は全体のごく一部であり、他は正確にはわかっていない。
しかし、多くの場合、修正すべき箇所さえわかれば修正できる。
• 修正の種類を限定する。ただし、修正の影響を受ける箇所を網羅できること、
そしてその修正が理論的に問題を起こさないことを証明できるようにする。
網羅性は規模の増大に対して問題となるが、その対処は理論的基礎の上で応
用として行う。
本論文では、この目的に対して、定理証明支援系 Coq に修正を行う命令と、そ
の修正によって影響を受けた箇所を対話的に修正する機能によって実現した。これ
らを総称して、対話的修正機構と呼ぶ。本論文における対話的修正機構の可能な
修正はコンストラクタを既存の帰納型に追加するというものである。しかし、こ
れだけであってもいくつかの条件によって修正漏れが発生してしまう場合がある。
本論文の貢献は、次の通りである。
• 型にコンストラクタを追加した際に、変数を用いたパターンによって、意図
しない挙動が行われる可能性がある点について分析する。代数的データ構造
におけるパターンマッチでは比較的容易に回避可能な問題だが、より拡張性
の高い型システムを利用すると、パターンマッチの網羅性を優先し、追加し
たコンストラクタに対する挙動についての記述漏れが起こりうる。
• Coq において上の問題を解決する手法である対話的修正を提案する。データ
型を拡張する仕組みを提供し、変数を用いたパターンなどに対しても対話的
にプログラマに修正を求めることで、記述漏れのない拡張を可能にする。
• Coq において網羅性のない述語について、網羅性を利用する代わりに拡張し
た型を元にプログラマに修正箇所として提示する手法を提案する。これは本
質的に網羅的である必要のない述語への提案を可能にする。
• プログラマに修正を求める際に、関数については変数によるパターンで生成
される項を提示する。これによりプログラマに判断する機会を与え、記述漏
れを防ぐことを可能にしている。また、既存の証明によって可能な限り変更
後の証明を進行させることを可能にした。これは直接証明を利用した場合に
エラーが出る場合についても対応できる。
• 変更をモジュール化し、複数のモジュールを同時に利用可能にする仕組みを
提案する。これにより、独立に行った複数の変更を一つのプログラムに対し
て適用することができる。このとき、それぞれの拡張によって修正が必要な
箇所が生じる場合もあるが、これを再び対話的に修正することで全体を構築
できる。
1.3. 本論文の構成
5
1.3 本論文の構成
本論文の構成は以下の通りである。
• 第 2 章では、本研究において使用する Coq、そして対象とする問題について
述べる。また、その問題が一般のプログラミング言語においてどのような解
決を試みられているか、という点について分析する。
• 第 3 章では、Coq においてプログラムの拡張をサポートする対話的修正機構
について、修正の流れ、挙動の形式的定義、拡張の健全性について議論する。
また、Coq が自動生成する関数についての制約についても述べる。最後に、
証明に対する修正箇所の問題について説明する。
• 第 4 章では、前章で問題として挙げた修正箇所を減らすために、検証に用い
ていた証明を利用する手法について提案する。
• 第 5 章では、対話的修正機構によって作成した拡張部分について、プログラ
ムの拡張モジュールとして取り扱う方法について述べる。
• 第 6 章では、プログラムの拡張に関する既存研究との比較を行う。
• 第 7 章では全体をまとめ、残された課題について述べる。
• Appendix A に、例題として使用したプログラムの全体を載せる。
7
第 2 章 本研究の背景
本章では、この論文において用いられる Coq と本研究が対象とする問題につい
て説明する。まず Coq で用いられる表層言語と内部表現、型システム、および戦
略記述言語について説明する。次に、対話的修正機構が対象とする典型的な問題
について述べ、その問題に対する既存手法について考察する。
2.1 Coq
Coq はフランスの国立研究機関 INRIA で開発されている対話的定理証明支援系
であり、特に本論文において扱う特徴として以下の特徴を持つ。
• 計算体系として predicative Calculus of (Co)Inductive Constructions（以下 pCIC）
を利用
• Ltac による対話的証明と証明の半自動化
本節では、導入として Coq の概要について説明し、その後 pCIC の定義と Ltac の
定義を行う。
この他の定理証明支援系の代表的なものとしては Isabelle[28, 19] や Agda[27] が
ある。本研究において Coq を用いる理由は、主に以下の二点を満たしている点に
ある。
• 対象とする論理体系が定まっている。
• 証明の記述が柔軟である。
Isabelle はメタ論理を提供する基盤である。そのため一つ目の点に対し、Isabelle/HOL
が広く用いられているとはいえ、対象の限定が難しい。Agda では Ltac のような
証明記述言語が存在せず、その点で規模の大きなプログラムの検証が難しいと考
えられる。また、CompCert のように大きなプログラムの検証が行われている点も
Coq を用いる理由として挙げられる。
第2章
8
本研究の背景
2.1.1 Coq の概要
Coq では、宣言などに用いるコマンドを Vernacular、項記述を Gallina、証明に
用いる言語を Ltac と呼ぶ。これらの言語を用い、プログラムの記述と検証を行っ
ている。以降では、コマンドと書いた場合は Vernacular で記述したものを指し、項
と書いた場合には Gallina で記述したものを指す。また、Ltac で記述した証明のた
めの命令を戦略（tactic）と呼ぶ。
Coq におけるプログラムの記述は、帰納型の宣言、定数の宣言、証明、記法の
宣言などで構成される。なお、本研究では記法の宣言についての議論はしないた
め、これらに関する説明は省略する。
帰納型の宣言
帰納型の宣言には Inductive コマンドを用いる。例えばペアノの公理に従った
自然数の宣言は以下の通りである。
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
ここで、nat は自然数の型を表す識別子であり、Set に属していることが宣言され
ている。Set はソートと呼ばれる帰納型の型であり、特に一般的な集合の型であ
る。O や S は nat のコンストラクタであり、それぞれ 0 とサクセサを表す。例えば、
2 に相当する nat の項は S (S O) である。これらのコンストラクタによってのみ
nat は構成される。なお、帰納型では必ず各要素は有限長であることが決まってお
り、例えば無限にサクセサが続く値は nat に属する要素ではない。
帰納型は型パラメータを持つことが出来る。例えば、リストの宣言は以下の通
りである。
Inductive list (A : Set) : Set :=
| nil : list A
| cons : A -> list A -> list A.
この宣言の中で、A はリストの要素を表す型としてパラメータ化されている。使
用時には A に対して実際の型を入れることができる。例えば、自然数のリストは
list nat であり、そのソートは Set である。この結果自然数のリストのリストと
して list (list nat) が記述でき、このソートもまた Set である。
パラメータは型だけではなくデータも取り得る。長さをパラメータとして持つ
リストの宣言は次の通りである。
2.1. Coq
9
Inductive vec (A : Set) : nat -> Set :=
| vnil : vec A O
| vcons : A -> forall n : nat , vec A n -> vec A (S n).
vcons の型は list のコンストラクタである cons と非常に似ているが、残りのリ
ストを取る前に自然数に対する全称限量が使用されている。この自然数は残りの
リストの型や結果の型の記述に用いられている。このように、与えられたデータ
に依存する型（依存型）を記述可能であることが Coq の特徴の一つである。なお、
この全称限量は関数と同様に振る舞い、関数適用によって値が決定される。例え
ば、要素 2 を持つ自然数のリストは vcons nat (S (S O)) O (vnil nat) と表現
され、その型は vec nat (S O) で表される。ここで、vcons の引数はそれぞれ、
リストに入る型、リストに入れる値、リストの長さ、残りのリストを表している。
定数の宣言
定数の宣言は、Definition コマンドや Variable コマンドを用いて行う。Variable
コマンドは定義をしない要素を作り出す。例えば、プログラミング言語を定式化
する際に、その中の変数の表現を明示したくない場合がある。このような場合に、
以下のように記述することで変数を表す型 Var を宣言できる。
Variable Var : Set.
一方で、Definition コマンドは項や関数を定義するために使われる。
Definition Env : Set := Var ->nat.
Definition eval_Var (v : Var) (e : Env) := e v.
ここで、Env は変数から自然数への関数であり、eval Var は変数と変数から自然
数への関数を取り、対応する自然数を返す関数である。このように、Coq では一般
の関数型言語におけるプログラミングに近い記述が可能である。この他にも、帰
納型に関するパターンマッチも行える。
Definition pred (n : nat) :=
match n with
| O => O
| S n’ => n’
end.
これは一つ前の自然数を返す関数である。便宜上 0 の一つ前を 0 としたが、これは
Coq の関数が常に全域関数でなければならないためである。これはパターンマッ
チの網羅性検査によって保証される。
第2章
10
本研究の背景
Coq では再帰関数の記述も可能である。再帰関数の記述には Fixpoint コマンド
を用いる。
Fixpoint length (A : Set) (l : list A) :=
match l with
| nil => O
| cons a l’ => S ( length A l ’)
end.
Coq における再帰関数には停止性を保証しなければならないという制約がある。
Fixpoint コマンドにより定義する関数は、この制約のために帰納型の値に対して
一度以上コンストラクタの展開を行った状態で再帰呼び出しをしなければならな
い。ここでは length の呼び出しの度に l のコンストラクタが展開されているた
め、受理される。より複雑な条件による停止性の保証は Function コマンドによっ
て可能であるが、本論文の範囲を超えるためここでは説明しない。
証明
証明は Theorem コマンドや Lemma コマンドによって定理を宣言することで始ま
る1 。ここでは、簡単な命題を証明することで証明について説明する。
Theorem example : forall P Q R : Prop ,
(P -> Q -> R) -> (P -> Q) -> P -> R.
ここで、Prop は Set 同様ソートである。Set は集合を表すソートだったが、Prop
は命題を表すソートであり、論理式や述語を定義するために用いられる。
証明時には、Coq は証明モードと呼ばれる状態になる。証明モードでは、現在
証明している命題と、その時点で使用可能な変数（とその型）の一覧が与えられ
る。例えば、上の入力の直後では以下のように表示される。
1 subgoal
============================
forall P Q R : Prop ,
(P -> Q -> R) -> (P -> Q) -> P -> R
この表示の後に入力待ちとなる。この表示では、残っている命題の数（1 subgoal）
や証明しようとしている命題が表示されている。証明モードでは戦略を用いて証明
を進行させる。例えば以下は intros 戦略を用いた場合に表示される状態である。
1
本体を記述しない Definition も同様の挙動を示す。これらは構文上同一だが、通常は意図を
区別するために使い分ける。
2.1. Coq
11
1 subgoal
P : Prop
Q : Prop
R : Prop
H : P -> Q -> R
H0 : P -> Q
H1 : P
============================
R
戦略によって、証明しようとしている命題が変化し、使用可能な変数（P、Q、R、
H、H0 および H1）が現れている。この変数と戦略を用いることで命題を証明する
ことができる。以降では、証明している命題をゴール、使用可能な変数を仮定と
呼ぶ。また、複数のゴールについて考える場合、それぞれのゴールをサブゴール
と呼ぶ。
定理の証明が完了すると、定理の名前で宣言した定数として扱われる。 この定
数は実体を持ち、その実体の型が定理に相当する。このときの実体を以後証明項と
呼ぶ。例えば、上の命題の証明項の一つとして、以下のものが構築される。
example =
fun (P Q R : Prop) (H : P -> Q -> R)
(H0 : P -> Q) (H1 : P) => H H1 (H0 H1)
: forall P Q R : Prop , (P -> Q -> R) -> (P -> Q) -> P -> R
このことから証明項は Prop ソートを用いている点を除くと完全に通常の定数の宣
言と同じであることがわかる。このような、命題と型、証明と項の間にある対応
関係をカリー・ハワード同型と呼ぶ。Coq はカリー・ハワード同型を用いること
で関数型言語のようなプログラミングと証明の記述を可能にしている。
述語
帰納型の宣言として Prop を用いたものを以下では述語と呼ぶ。例えばパラメータ
として与えられる自然数が偶数であることを表す述語は以下のように定義される。
Inductive even : nat ->Prop :=
| even_O : even O
| even_SS : forall n : nat , even n -> even (S (S n)).
また、複数のパラメータについての関係を記述することもできる。次の例は第一
引数が第二引数の二倍であることを表す述語である。
第2章
12
本研究の背景
Inductive double : nat ->nat ->Prop :=
| double _O : double O O
| double _S : forall n m : nat ,
double n m -> double (S (S n)) (S m).
述語を用いると、関数としては記述が難しい性質を記述することもできる。
2.1.2 pCIC
pCIC は Calculus of Constructions に帰納型を加えたものである2 。Calculus of
Coonstructions[10] は型付きラムダ計算の一種であり、依存型を持つ。一方、単純
型付きラムダ計算や System F と異なり、構文上に項と型の明確な区別がない体系
である。
オリジナルの pCIC の定義はリファレンスマニュアル [8] に記載されているが、
ここでは Coq で使用されている体系について Gallina に近い文法で記述する。
項と環境の定義
まず、pCIC の項の定義を行う3 。項の定義は図 2.1 の通りである。最初の三つは
ソートと呼ばれるものであり、帰納型の型である。Set に属する帰納型は通常の集
合に相当するデータ型であり、ブール値や自然数、整数、リストなど多くの代数
的データ構造が含まれる。Prop に属する帰納型は命題に相当する型である。この
中には論理積や論理和、矛盾、値の等価性（通常は Leibniz equality）などが含ま
れる。Type0 は上記二つのソートの型であり、また通常の集合より大きな型が所属
するソートである。したがって、全ての集合の要素を集めた型は Type0 に属する
必要がある。Set と Type0 との関係と同様に、Type0 の型は Type1 、Type1 の型は
Type2 、のように自然数の範囲で増加する。 なお、これら Typei は Gallina では添
え字を付けない。また、Coq の内部では具体的な自然数でなく、他の Type の出現
との添え字の不等号で表現されている。
pCIC には変数だけでなく定数が存在する。定数は Coq のトップレベルにおいて
定義された値であり、Definition コマンドによって宣言された関数などに束縛さ
れていたり、Variable コマンドによって宣言されたパラメータであったりする。
一方、変数は関数抽象や let 式が束縛する要素である。
2
Calculus of Inductive Constructions が先に提案され、Coq7.4 まで使用されていた。
本論文では再帰関数や余帰納型などに関する議論は行わないが、再帰関数や余帰納関数（cofix）
に関する guard condition を除くと一般的な関数や帰納型と同様の型システムとなっており、基本的
に議論をそのまま利用することができる。
3
2.1. Coq
T ::=
|
|
|
|
|
|
|
|
|
|
|
13
Set
Prop
Typei
x
c
(T T )
fun x : T => T
∀x : T, T
let x := T in T
I
C
match T return T with ( | C x∗ => T )∗ end
(Set ソート)
(Prop ソート)
(レベル i の Type ソート)
(変数)
(定数)
(関数適用)
(関数抽象)
(全称限量)
(let 式)
(帰納型)
(コンストラクタ)
(パターンマッチ)
図 2.1: pCIC の項の定義。
関数適用や関数抽象は ML や Haskell などの一般的な関数型言語のそれと同様で
ある。しかし、関数を表す型は全称限量が対応し、全称化されている要素が引数
の型、本体が関数本体の型に当たる。例えば A → B は B に x が自由に出現しない
とすると、∀x : A, B という記述が A → B に相当する4 。一方、B に x が自由に出現
している場合、 B は x に依存した型である。
帰納型とコンストラクタは帰納型の宣言によって定義される値である。帰納型
の宣言の形式的定義は以下の通りである。
Ind ::= I (x : T )∗ : T := ( | C (x : T )∗ : T )∗
なお、I の型は必ずソートで終わらなければならない。また、そのほかにもコンス
トラクタが満たさなければならない positivity condition などが存在するが、本論文
ではこれらが成立している前提とする。
パターンマッチは、代数的データ構造の代わりに帰納型の展開を行うという点
を除くと、ほぼ ML におけるパターンマッチと同じである。ただし、大きな差とし
てパターンマッチの結果を表す return から始まる節が追加されている。これは、
パターンマッチによって展開する値によって型が変わる（依存型を返す）場合に
推論が難しい（場合によっては決定不能）ためである。関数型言語として用いる
場合、この return 部分は省略可能であり Coq が推論によって補う。
4
概要で利用していることからわかるように、Coq では束縛変数が出現しないという条件を満た
す全称型は関数型や含意として記述される。
第2章
14
本研究の背景
最後に、定義環境を定義する。定義環境は、直感的には定数の宣言と帰納型の
宣言のリストであり、形式的に定義した場合以下の通りである。
Def ::= c : T
E
::= ·
| c : T := T
| Def ; E
| Ind
以上の pCIC の定義は Gallina のほとんどの要素と一対一に対応するが、一部異
なる部分がある。顕著なのはパターンマッチであり、pCIC では帰納型を一つ展開
することしかできないが、Coq では例えば以下の記述が可能である。
Definition is_fst_zero (nl : list nat) : bool :=
match nl with
| cons O _ => true
| _ => false
end.
pCIC では一つ目のパターンで cons 以外のコンストラクタを記述することができ
ないため、cons の第一引数を変数として受け取り、そのパターンマッチを行う必
要がある。しかし、Gallina では同時にその箇所に O が出現するというパターンを
記述することができる。
また、この例では二つ目のパターンとしてワイルドカードパターン（アンダー
スコアのみのパターン）を使用している。ワイルドカードパターンはコンストラ
クタを展開せずに、それまでに記述されたパターンにマッチしない項全てとマッ
チするパターンである。同様に、アンダースコアの代わりに変数を用いることで、
残りの全ての項を変数に束縛して利用することができる。なお、ワイルドカード
パターンはパターンの本体に出現しない変数を用いたパターンと等価である5 。
このような pCIC で表現できないパターンマッチはパターンの展開により pCIC
に変換される [3]。また、出力時には可読性向上のためにこの変換の逆に相当する
操作が行われる。しかし、それぞれの変換は一対一ではないため、結果として一
部の項が出力時に異なる形で出力される。例えば上の例は以下のとおりに出力さ
れる。
is_fst_zero =
fun nl : list nat =>
match nl with
| nil => false
| cons O _ => true
| cons (S _) _ => false
end
5
Gallina では変数を使用する箇所全てでアンダースコアを用いることができる。意味はパター
ンの場合と同様に、束縛が有効な範囲で出現しない変数を用いた場合と等価である。
2.1. Coq
15
このように、複数のコンストラクタの展開は表示されるが、ワイルドカードパター
ンが展開され、nil の場合と、cons の最初の要素が何かに S を適用した場合を表
すパターンが出現している。一方、内部ではリストと自然数のパターンマッチは
別に展開されているが、出力時にまとめられている。このことは、上の例の pCIC
での表現と同一である次の記述を出力すると全く同様の出力があることからも確
かめられる。
Definition is_fst_zero (nl : list nat) : bool :=
match nl with
| nil => false
| n :: _ =>
match n with
| O => true
| S _ => false
end
end.
規則
本節では、本研究で提案する手法の健全性についての証明に用いる情報を記述
する。ただし、型付け規則はリファレンスマニュアルに記述されたものを使用し、
ここには記載しない。なお、リファレンスマニュアルにおける記法との違いは以
下の通りである。
• 表面的な記述。本論文では関数抽象を fun を用いているが、リファレンス
マニュアルでは λ を使っている。そのほか、パターンマッチがコンストラク
タ毎の関数（コンストラクタのパラメータを引数に取る）として表現されて
いる。
• 帰納型の宣言。本論文では一つの宣言のみを取り扱っているが、リファレン
スマニュアルでは相互帰納型の記述のために複数の帰納型をまとめた記述を
している。一般化は複数の連続した宣言を使用することで容易に可能である
ため、ここでは一つの宣言しか取り扱わない。
型付け規則は、定義環境と項に対して相互に依存する形で記述される。また、項
に対する型付け規則の定義は、いくつかの簡約に基づく順序関係を用いて定義さ
れる。簡約や規則は環境と局所文脈を用いて定義されるため、まず局所文脈につ
いて記述する。局所文脈は変数に関する型または実体を含むものであり、直感的に
第2章
16
本研究の背景
は局所変数の情報を集めた物である。局所文脈の形式的定義は以下の通りである。
Var ::= x : T
Γ
::= ·
| x : T := T
| Var; Γ
プログラムのある地点で定義環境が E であり、局所文脈が Γ である場合、その地
点での文脈を E[Γ] と表す。直感的には文脈はその地点で可視な定数や変数の一覧
である。この文脈下で項 t に型 T 型がつくことを E[Γ] ⊢ t : T と記述する。
次に簡約とそれに基づく順序関係の定義を行う。ここで定義する簡約は β 簡約、
ι 簡約、δ 簡約、ζ 簡約であり、また η 変換について述べる。なお、項 T の変数 x
に対する t の代入を T {x/t} と記述する。これは新たに束縛関係を作らないものと
する。
簡約はそれぞれ、E[Γ] ⊢ T ▷ x T ′ のように記述され、 x には β, ι, δ, ζ が入る。そ
れぞれの定義は以下の通り。
E[Γ] ⊢ ((fun x : T 1 ) T 2 ) ▷β T 1 {x/T 2 }
E[Γ] ⊢ match Ci T 1 . . . T n with . . . | Ci x1 . . . xn => T ′ | . . . end ▷ι T ′ {x j /T j } j=1..n
E[Γ] ⊢ x ▷δ T 1
if x : T 2 := T 1 ∈ Γ
E[Γ] ⊢ c ▷δ T 1
if c : T 2 := T 1 ∈ E
E[Γ] ⊢ let x := T 1 in T 2 ▷ζ T 2 {x/T 1 }
ι は表記の関係上パターンマッチの return 節を消去した。このように、それぞれ
関数適用、パターンマッチ、変数や定数の本体への置き換え、let 式の展開を表し
ている。また、η 簡約として (fun x : T 1 => (T 2 x)) ▷ T 2 が存在する（ただし x は T 2
に自由に出現しない）が、これは無条件に利用すると型の健全性が失われる。一
般にはこの逆である η 拡大を利用する。これらの簡約と逆方向の変換を総称して η
変換と呼ぶ。
二つの項 T , U は、複数回の β, ι, δ, ζ 簡約の後、高々一回の η 変換したものが一
致する場合に E[Γ] ⊢ T =βιδζη U である。また、これを用いたサブタイプ関係は次
のように定義される。
1. E[Γ] ⊢ T =βιδζη U であるとき E[Γ] ⊢ T ≤βιδζη U
2. i ≤ j ならば E[Γ] ⊢ Typei ≤βιδζη Type j
3. 自然数 i に対して、E[Γ] ⊢ Set ≤βιδζη Typei
4. E[Γ] ⊢ Prop ≤βιδζη Set
5. E[Γ] ⊢ T =βιδζη U かつ E[Γ; x : S ] ⊢ T ′ ≤βιδζη U ′ であるとき
E[Γ] ⊢ ∀x : T ′ , T ≤βιδζη ∀x : U ′ , U である。
2.1. Coq
17
2.1.3 Ltac
Ltac は Coq において証明に使用する戦略を記述する言語である。戦略には基礎的
な（Ltac でこれ以上細分化されない）戦略と、Ltac によって組み立てられた戦略が
ある。基礎的な戦略には intro や apply などの Coq 組み込みの戦略の他、OCaml
で記述された6 （Ltac では記述できない、または難しい）戦略がある。以下では、
このような基礎的な戦略を原子戦略と呼ぶ。
本研究で扱う Ltac の構文は以下の通りである。
t ::=
|
|
|
|
atomic tac
t;t
t ; [ t | t | ... | t ]
try t
repeat t
(原子戦略)
(連結)
(サブゴール数固定の連結)
(try コマンド)
(repeat コマンド)
それぞれの振る舞いについて説明する。ただし原子戦略については省略する。
• 戦略の連結 t1 ; t2 は、まず与えられたゴールに対して t1 を適用し、証明を試
みる。その結果、残ったサブゴール全てに対して t2 を適用する。ただし、t1
の適用時点で証明が終了した場合、t2 は適用されない。t1 の適用時か、t2 が
適用されたサブゴールのうち一つ以上においてエラーが発生した場合、この
戦略はエラーとなる。
• サブゴール数固定の連結 t ; [ t1 | . . . | tn ] は、t の適用結果残ったサブゴール
が連結した戦略の数である n に一致しなければならず、一致した場合は i 番
目のサブゴールに対して ti を適用する。数が一致しない場合や ti のうちの一
つがエラーとなった場合、全体もエラーとなる。数の不一致によるエラーは
t によって証明が終了した場合でも発生する。
• try コマンドは、続く戦略がゴールに対してエラーを起こした場合に、try コ
マンドが実行される前の状態に戻す。成功した場合はそのまま終了する。
• repeat コマンドは、続く戦略を成功する限りゴールに繰り返し適用する。エ
ラーとなった場合は、最後に成功した時点の状態へ戻す。
なお、この他にも Ltac には多くの構文が存在する。例えば、選択実行、ゴール
や仮定に対するパターンマッチなどが挙げられる。本研究における議論では、定
義していない構文は原則として原子戦略であるとして扱う。これらの構文は自動
化のために頻繁に用いられるものの、本質的な難しさはほとんど変わらず、同様
の処理が可能である。
6
Coq は OCaml で実装されており、モジュールを読み込むことで戦略を具現化する。
第2章
18
本研究の背景
2.2 問題：拡張に対する指摘
本節では、本研究の対象とする問題を例題を用いて説明する。ここで取り上げ
る例題は While 言語という非常にシンプルな手続き型言語をターゲットとしたプ
ログラムの最適化器の記述と検証である。なお、例題のプログラム全体は A に記
載する。
2.2.1
初期プログラム
While 言語の構文を BNF で定義すると、以下のようになる。
A ::=
|
|
B ::=
|
|
|
|
|
S ::=
|
|
|
|
v
x
A+A
true
false
not B
B and B
A=A
A<A
x := A
skip
if B then S else S
while B do S
S ;S
(定数)
(変数)
(加算)
(真値)
(偽値)
(論理否定)
(論理積)
(算術等価)
(小なり)
(代入)
(no-op)
(条件分岐)
(繰り返し)
(連結)
ここでは、算術式を A で、ブール式を B で、文を S で記述している。この While
言語の抽象構文を Coq を用いて記述すると図 2.2 となる。Aexp は A に、Bexp は B
に、Stm は S に相当する。なお、今回の問題ではブール式がそれほど重要ではない
ため、定義を省略している。
While 言語の意味論を自然意味論として記述したものは図 2.3 のようになる。こ
れを Coq で記述した物が図 2.4 である。算術式、ブール式、文それぞれの意味は
Aeval、Beval、NS によってつけられる。これらは全て big-step semantics として定
義されているが、前二者は Coq の関数として定義されている一方、後者は述語と
して定義されている。これは、Coq が終了しない関数を記述できないため、無限
ループを記述することができる While 言語の意味論を陽に記述することができな
いことによる。
2.2. 問題：拡張に対する指摘
19
Definition Val := Z.
Definition Env := Var ->Val.
Inductive
| Aval :
| Avar :
| Aadd :
Aexp : Set :=
Val ->Aexp
Var ->Aexp
Aexp ->Aexp ->Aexp.
Inductive Bexp : Set := ... ( ∗ o m i t t e d ∗ )
Inductive Stm : Set :=
| Sass
: Var ->Aexp ->Stm
| Sskip : Stm
| Sif
: Bexp ->Stm ->Stm ->Stm
| Swhile : Bexp ->Stm ->Stm
| Scomp : Stm ->Stm ->Stm
図 2.2: Coq による While 言語の抽象構文。
次に、この言語に対する最適化器を導入する。最適化器の対象とするものは、状
態に対して不変な要素の簡約と除去である。ここでは、算術式に関する最適化と
して、定数同士の加算を事前に計算しておき、その結果と置き換えることを行う。
また、文に関する最適化として、条件式に当たるブール式が常に真（または偽）に
定まるような条件分岐を対応する分岐先の文に置き換える、常に偽に定まる繰り
返し文を skip 文に置き換える、ということを行う。このような最適化器を図 2.5 の
ように記述した。なお、ブール式に関する最適化器は省略するが、基本的な内容
は算術式のそれと同じである。
この最適化器の正しさを保証するために、算術式やブール式については最適化
の前後で意味が変わらないことを、文については最適化前の結果が最適化後も保
たれることを証明した。これらの定理は図 2.6 のように記述される。今回は算術
式に対する証明を与え、ブール式については全体を省略、文については証明の最
初の分岐についてのみ言及している。算術式の最適化器の検証では式に対する構
造帰納法を用い、変数や定数の場合の自明なケースを自動証明（intuition）に
任せ、加算に関してのみ明示的に帰納法の仮定を利用して書き換えを行っている。
また、文の最適化器の検証では意味論の導出に関する帰納法（induction）を用
いている。
第2章
20
⟨x:=A, e⟩ ⇒ [x/A(A, e)]e
B(B, e) = true
⟨S 1 , e1 ⟩ ⇒ e2
⟨if B then S 1 else S 2 , e1 ⟩ ⇒ e2
B(B, e) = true
本研究の背景
⟨skip, e⟩ ⇒ e
B(B, e) = false
⟨S 2 , e1 ⟩ ⇒ e2
⟨if B then S 1 else S 2 , e1 ⟩ ⇒ e2
⟨S , e1 ⟩ ⇒ e2
⟨while B do S , e2 ⟩ ⇒ e3
⟨while B do S , e1 ⟩ ⇒ e3
B(B, e) = false
⟨while B do S , e⟩ ⇒ e
⟨S 1 , e1 ⟩ ⇒ e2
⟨S 2 , e2 ⟩ ⇒ e3
⟨S 1 ; S 2 , e1 ⟩ ⇒ e3
図 2.3: While 言語の自然意味論。ただし、A と B はそれぞれ算術式とブール式を
与えられた変数環境で評価する関数である。
2.2.2
拡張
図 2.2 の構文は必要最小限度のものであるため、実際にはより多くの演算子や文
があることが望ましい。そこで、算術演算子として乗算を、文として repeat-until
文を導入する。まず、構文を表す型に対応するコンストラクタを追加する。それ
ぞれ、ここでは Amult および Srepeat とする。本来のプログラムの内容から、こ
れらのコンストラクタを追加した後、いくつかの修正をしなければならない。修
正箇所としては乗算の意味論、repeat-until 文の意味論、それぞれの最適化器や定
理の証明がある。図 2.7 と図 2.8 に本来行われるべき修正を示す。プログラマは、
これらの修正箇所を何らかの形で知る必要がある。
もっとも一般的な修正箇所の探索方法は、コンストラクタを追加したプログラ
ムを Coq に読み込ませ、エラーが出た箇所を見ていくものである。例えば、算術
式の評価関数である Aeval はパターンマッチにおいて乗算に関するパターンが存
在しないため、定義箇所において以下のようなエラーを出力する。
Error: Non exhaustive pattern-matching:
no clause found for pattern Amult _ _
プログラマは、このエラーに基づいて乗算の意味論を追加する。そのため、この
手法をエラーに基づく修正と呼ぶことにする。
一方で、この手法における問題として、エラーが発生しない箇所の存在が挙げ
られる。まず、文の意味論を表している述語 NS は定義上 repeat-until 文に関する意
味論を持っていないが、述語の定義は全域性の判定が行われないため、エラーが
2.2. 問題：拡張に対する指摘
Fixpoint
| Aval
| Avar
| Aadd
end.
21
Aeval (a : Aexp) (e : Env) := match a with
z => z
v => e v
a1 a2 => (( Aeval a1 e) + (Aeval a2 e))%Z
Inductive NS
| NSass
:
NS (Sass v
| NSskip
:
| NSif_T
:
Beval b e1
|
|
|
|
: Stm ->Env ->Env ->Prop :=
forall v a e,
a) e ( ExtEnv v ( Aeval a e) e)
forall e, NS Sskip e e
forall b S1 S2 e1 e2 ,
= true -> NS S1 e1 e2
-> NS (Sif b S1 S2) e1 e2
NSif_F
: forall b S1 S2 e1 e2 ,
Beval b e1 = false -> NS S2 e1 e2
-> NS (Sif b S1 S2) e1 e2
NSwhile _T : forall b S e1 e2 e3 ,
Beval b e1 = true -> NS S e1 e2
-> NS ( Swhile b S) e2 e3
-> NS ( Swhile b S) e1 e3
NSwhile _F : forall b S e,
Beval b e = false -> NS ( Swhile b S) e e
NScomp
: forall S1 S2 e1 e2 e3 ,
NS S1 e1 e2 -> NS S2 e2 e3
-> NS ( Scomp S1 S2) e1 e3.
図 2.4: Coq による While 言語の意味論。
発生しない。述語の性質上このような記述をエラーとして検出することは不可能
であり、プログラマが見つけなければならない。
次に、算術式用の最適化器である Aopt もエラーを発生しない。算術式の最適化
器は定義上加算以外の全ての場合で元の値を返すため、乗算の際もそのままを返
してしまう。これは最適化器の意図と必ずしも一致せず、むしろ最適化の漏れで
あると考えられる。しかしながら、記述上乗算の場合もパターンマッチにおける
ワイルドカードパターン7 によって補完されてしまうため、エラーとして報告され
ず、やはりプログラマ自身が見つけなければならない。同様の理由により、Sopt
もエラーを発生しない。
最後に、証明に関してもエラーが発生しない場合がある。証明時に場合分けな
どをすると、比較的自明なゴールが多数出現することがある。このような自明な
7
アンダースコアによるパターン。全てのコンストラクタと合致する。
第2章
22
本研究の背景
Fixpoint Aopt (a : Aexp) := match a with
| Aadd a1 a2 => match (Aopt a1 , Aopt a2) with
| (Aval z1 , Aval z2) => Aval (z1+z2)%Z
| (a1 ’, a2 ’) => Aadd a1 ’ a2 ’
end
| _ => a
end.
Fixpoint Sopt (S : Stm) := match S with
| Sass x a => Sass x (Aopt a)
| Sif b S1 S2 => match Bopt b with
| Btrue => Sopt S1
| Bfalse => Sopt S2
| b’ => Sif b’ (Sopt S1) (Sopt S2)
end
| Swhile b S’ => match Bopt b with
| Bfalse => Sskip
| b’ => Swhile b’ (Sopt S ’)
end
| Scomp S1 S2 =>
match (Sopt S1 , Sopt S2) with
| (Sskip , S2 ’) => S2 ’
| (S1 ’, Sskip ) => S1 ’
| (S1 ’, S2 ’) => Scomp S1 ’ S2 ’
end
| _ => S
end.
図 2.5: While 言語の最適化器。
ゴールはプログラマにとって単純作業に過ぎず、本質的に難しい問題ではない。そ
のため、これらをまとめて自動証明によって解決するという手法をとることが多
い8 。しかし、その結果追加されたはずのゴールが証明されてしまう場合もある。
例えば、Aopt keep result における証明は、加算の場合以外の証明は自動証明に
任せている。最適化器は（上の問題により）乗算も元と同じ値を返すため、定数
や変数の場合と同様に自明であり、この自動証明によって補完される。また、文
に対する最適化器は、意味論中に追加した文が存在しないため、帰納法の場合分
けに現れず、やはり証明は終了する。
一般に証明においてエラーが発生せずに終了することは問題ではないが、しか
8
事実、Ltac の構文には特定の処理の後に指定された戦略で証明を試みる、という類の構文が多
数存在する。
2.2. 問題：拡張に対する指摘
23
Lemma Aopt_keep_ result :
forall (a : Aexp) (e : Env),
Aeval a e = Aeval (Aopt a) e.
Proof .
induction a; intuition ; simpl in *;
rewrite IHa1; rewrite IHa2;
case (Aopt a1 ); case (Aopt a2 ); auto.
Qed.
Lemma Bopt_keep_ result :
forall (b : Bexp) (e : Env),
Beval b e = Beval (Bopt b) e.
... ( ∗ o m i t t e d f o r b r e v i t y ∗ )
Qed.
Theorem Sopt_keep_ semantics :
forall (S : Stm) (e1 e2 : Env),
NS S e1 e2 -> NS (Sopt S) e1 e2.
Proof .
intros S e1 e2 H; induction H;
try ( rewrite Aopt_keep_ result );
try constructor ; auto; simpl .
... ( ∗ o m i t t e d f o r b r e v i t y ∗ )
Qed.
図 2.6: 最適化器の性質と証明（一部）。
し他の問題と重なった場合に問題となる。証明は、関数などの定義でエラーが発
生しなかった場合にプログラマが修正箇所に気付く機会となるが、しかしエラー
が出なければプログラマが気付く機会は得られず、意図とは異なる結果のまま証
明が完了してしまう。
以上の問題の多くは、記述方法による補完が原因であり、この問題が発生しな
いようにプログラムを記述することは十分に可能である。しかし、これらの機能
そのものは非常に有用であり、使用しなければ証明が非常に大きくなる可能性も
ある。図 2.6 を例にとると、全体を提示した Aopt keep result では、induction
の後の intuition を Aexp のコンストラクタ毎の証明で記述する必要がある。ま
た、Sopt keep semantics の if の意味に関する証明で、条件式を最適化した結果
によって分岐させている。このとき、条件式が true と評価されたとすると、最適
化後のプログラムでも条件式は true と評価されるはずである。これは複数の論理
演算子や比較演算子に対して同様であるため、多くの分岐後のサブゴールで同じ
第2章
24
Inductive
| Amult :
Inductive
| Srepeat
本研究の背景
Aexp : Set := ...
Aexp ->Aexp ->Aexp.
Stm : Set := ...
: Stm ->Bexp ->Stm.
Inductive NS : Stm ->Env ->Env ->Prop := ...
| NSrepeat _T : forall b S e1 e2 ,
NS S e1 e2 -> Beval b e2 = true
-> NS ( Srepeat S b) e1 e2
| NSrepeat _F : forall b S e1 e2 e3 ,
NS S e1 e2 -> Beval b e2 = false
-> NS ( Srepeat S b) e2 e3
-> NS ( Srepeat S b) e1 e3.
図 2.7: While 言語の構文などの型の修正箇所。図 2.2 と同じ箇所は . . . で省略して
いる。
戦略で証明できる。実際、今回は 5 つの戦略を連結させたものによって、6 つのサ
ブゴールのうち 4 つのサブゴールが証明できた。同様の条件式の分岐は証明時に
4 回出現しており、連結した戦略によって 16 個のサブゴールを証明したことにな
る。一方、連結した戦略を用いない場合、類似した証明を 4 回ずつ記述する必要
があり、単純に 4 倍の記述量になってしまう。このように、補完を利用しない場合
何度も同じような戦略の列が出現し、証明が長くなってしまう。
述語の定義に関しては、存在する記述が元々正しく、また網羅性の判定などが
存在しないため、コンストラクタの追加による影響を受けにくい。したがって、述
語の定義において型エラーが発生する可能性は少なく、エラーを頼りに修正箇所
を見つけることはできない。
一方で、述語の使用を回避することも難しい。今回使用した述語は自然意味論
だが、これを構造的操作的意味論にすることで関数として定義することもできる。
しかし、自然意味論は直感的な意味論であり、証明が容易になるという利点があ
る。また非決定性のように関数で表しにくい意味も述語としてならば容易に記述
可能である。このように、述語の使用には利点が存在するため、常に述語を使わ
ないという手法は現実的ではない。
2.3. 既存研究の問題
25
Fixpoint Aeval (a : Aexp) (e : Env) := match a with
...
| Amult a1 a2 => (( Aeval a1 e) * (Aeval a2 e))%Z
end.
Fixpoint Aopt (a : Aexp) := match a with
...
| Amult a1 a2 =>
match (Aopt a1 , Aopt a2) with
| (Aval z1 , Aval z2) => Aval (z1*z2)%Z
| (a1 ’, a2 ’) => Amult a1 ’ a2 ’
end
| _ => a
end.
Fixpoint Sopt (S : Stm) := match S with
...
| Srepeat S’ b => match Bopt b with
| Btrue => Sopt S’
| b’ => Srepeat (Sopt S ’) b’
end
| _ => S
end.
図 2.8: While 言語に関係する関数の修正箇所。図 2.4 や図 2.5 と同じ箇所は . . . で
省略している。
2.3 既存研究の問題
2.3.1 Expression problem
一般に前節において対象としたプログラムの拡張は、Expression problem と呼ば
れる問題の典型である [35]9 。問題自体は非常に単純で、算術式を表現するデータ
と、その計算を行う操作を実現したプログラムに対し、算術式の種類や操作を増
やした際に必要となる修正を考える問題である。
ここでは、初期のプログラムとして、算術式が（整数）定数と加算、操作がそ
の評価を実現したものを考える。例えば、OCaml で代数的データ構造を用いて記
述したプログラムは以下の通りである。
9
類似の問題は何度も提案されているが、この名前が使われたのは 1998 年の Java Genericity
mailing list における Wadler の投稿が初めてである。
26
第2章
本研究の背景
type exp =
| Const of int
| Add of (exp*exp)
let rec eval = function
| Const n -> n
| Add (e1 ,e2) -> eval e1 + eval e2
また、Java で記述した場合、以下のようになる。
abstract class Exp {
abstract public int eval ();
}
class Const extends Exp {
private int val;
public Exp(int val) { this.val = val; }
public int eval () { return val; }
}
class Add extends Exp {
private Exp e1 , e2;
public Add(Exp e1 , Exp e2) { this.e1 = e1; this.e2 = e2; }
public int eval () { retrun e1.eval () + e2.eval (); }
}
ここで、二つの変更を考える。一つは算術式への乗算の追加、もう一つは算術式を
標準出力に印字する操作の追加である。後者を OCaml で行うことや、前者を Java
で行うことは容易であり、それぞれ以下のようになる。
let rec print = function
| Const n -> print _int n
| Add (e1 ,e2) -> print e1; print _ string "+"; print e2
class Mult extends Exp {
private Exp e1 , e2;
public Mult(Exp e1 , Exp e2) { this.e1 = e1; this.e2 = e2; }
public int eval () { return e1.eval ()* e2.eval (); }
}
しかし、OCaml で記述したプログラムに対する乗算の追加や、Java で記述したプ
ログラムに対する印字操作の追加は、上記のコードのように単純な追加では記述
できない。OCaml では宣言した代数的データ構造 exp の定義を書き換え、乗算を
表すコンストラクタを追加する必要がある。また、Java では抽象クラスとして宣
2.3. 既存研究の問題
27
言した Exp クラスや、その子クラスである Const クラス、Add クラスに print メ
ソッドを追加する必要がある。
Expression problem では、拡張性の指標として以下の性質について議論する。
1. 拡張の回数に制限がないこと
2. 既存のコードを書き換える必要がないこと
3. 単純なものを除いてコードの重複がないこと
4. 処理できないデータ種などが存在しないこと
5. 型安全であること
6. 既存のコードの再コンパイルが必要ないこと
本研究における対話的修正機構は、再コンパイルの必要性に関しては議論の余地
があるが、他は全て満たしている。これは、結果として得られるプログラムがバ
イナリなどの実行形式ではなく Coq の内部表現であり、これはある種の再コンパ
イルであるとも取れるためである。また、第 4 章では証明を容易にするために既
存のコードを読み直し、新しく内部表現を作るという手法をとっている。一方で、
手法単体では特に既存のコードを再度処理する必要がないため、再コンパイルを
していないと考えることもできる。
2.3.2
既存手法
ここでは関数型言語の視点から Expression problem について見る。この問題を解
決するために必要な拡張は、データ型に対する種類の追加と、既存の処理（関数）
への追加したデータ型の操作の追加である。ここでは、既存研究における拡張に
対するサポートと、関数に対する引数の追加について議論する。
Expression problem の解法としては、現在 Haskell で広く使われている型クラス
[36] や、OCaml で利用されている polymorphic variant[15] がある。型クラスにおけ
る記述では、型クラスの記述（データ型の宣言に相当する）とインスタンスの記
述（データ型の種類の記述）とが分かれているため、容易に種類を追加すること
ができる。また、関数も各インスタンスごとに通常の関数と同様の記述が可能で
ある。例えば、Haskell における型クラスを用いて上に挙げた例を記述すると、次
のようになる。
28
第2章
本研究の背景
data Const = Const Int
class Eval a
where eval :: a ->Int
instance Eval Const
where eval ( Const n) = n
data Add a b = Add a b
instance (Eval a, Eval b) => Eval (Add a b)
where eval (Add a b) = eval a + eval b
関数の追加やインスタンスの追加は新しいクラスの追加や instance 宣言によって
容易に対応できる。
一方 polymorphic variant では、型の構造が使用するラベルの種類によって決定
されるため、容易に型が拡張可能になっている。上と同様の例を記述すると、次
のようになる。
type ’a exp =
[‘Const of int | ‘Add of ’a * ’a ]
let map_exp (f : _ -> ’a) : ’a exp -> ’a = function
‘Const _ as n -> n
| ‘Add(e1 , e2) -> ‘Add (f e1 , f e2)
let eval_exp eval_rec (e : ’a exp) : ’a =
match map_exp (eval_rec ()) e with
‘Add(‘ Const m, ‘Const n) -> ‘Const (m+n)
| e -> e
let rec eval () = eval_exp eval
このとき eval の引数は exp の型と同様になっている。それぞれ型の宣言（’a exp）
や関数の宣言（eval exp eval rec）においてパラメータを利用して宣言し、最
終的に全体を再帰的に構築する、という手段をとっているため、関数の宣言と構
築を行うことで拡張が可能となっている。
これらの問題点として、型クラスではパターンマッチの網羅性の欠如、polymorphic variant では関数の記述の複雑さが挙げられる。型クラスはインスタンスの宣
言を任意のタイミングで行うことが可能であるため、インスタンスの列挙自体が
不可能である。例えば、関数を宣言した時点では 3 つのインスタンスが存在する
場合でも、関数の宣言後に新たなインスタンスを宣言することで列挙できていな
2.3. 既存研究の問題
29
いインスタンスが出現する。これは場合分けという形で証明中に列挙することが
多い証明支援系への導入を難しいものとしている10 。また polymorphic variant は上
の例でもわかるとおり、再帰関数の記述に工夫が必要である。そのため、プログ
ラマにかかる負荷とともに、終了性などの判定が難しいことからやはり導入は非
常に難しい。
より通常の代数的データ構造の記述に近くした研究としては open data type[24]
が挙げられる。これは Haskell の拡張として作られており、データ型の記述や関数
に open という指定子を付けることで後に型や関数を拡張することが可能となる。
open data Expr :: *
Const :: Int -> Expr
open eval :: Expr -> Int
eval ( Const n) = n
Add :: Expr -> Expr -> Expr
eval (Add e1 e2) = eval e1 + eval e2
ここでは連続して宣言しているが、eval の宣言や Add の宣言は異なるファイルで
あってもかまわない。なお、制限として open 指定子が付けられるのはトップレベ
ルで宣言されたデータ型および関数のみ、というものがあるが、多くの場合この
制約はそれほど問題とならないと主張されている。このように、非常に簡潔に記
述することができるため、プログラマ側の負担も最小限となっている。
一般のプログラミング言語における Expression problem の解法について、問題を
考えると以下のことが挙げられる。
• 拡張をすべき場所を全て知っている必要がある。拡張されうる箇所を全て元
の作成者が予想せねばならない。また、ある拡張の結果、連鎖的に拡張が必
要となる箇所は全てプログラマが知っていなければならない。
• Coq をはじめとする対話的証明支援系にはこれらの複雑な型システムは導入
されていない。これは、内部の論理の無矛盾性とこれらのシステムの兼ね合
いをとることが困難であることに起因する。
二つ目については明らかであるためこれ以上の分析は必要ないが、一つ目につい
てはいくつかの例を見る。
Expression problem では問題の本質的部分のみを記述しているため、データの種
類を追加すると全ての処理が拡張の対象となる。しかし、現実のプログラムにお
10
Coq には v8.2 より、依存型とレコードを組み合わせることで型クラスを実現している。しか
し、この場合の性質の記述では同様の理由により場合分けが不可能である。
30
第2章
本研究の背景
いて全体が拡張の対象となることはほとんどありえず、一部の拡張で事足りる。こ
のとき、プログラマは拡張すべき箇所を全て事前に知っていなければならないが、
一般にプログラム全体を認識することは難しい。
拡張すべき箇所を知る手段としては、Coq における問題と同様、パターンマッ
チの網羅性検査によって発見するというものがある。網羅性検査は open data type
でも、Main モジュールのコンパイル時に限定されるが実現されている。しかし、
open data type では、より具体的なパターンを優先する best-fit パターンマッチとい
う手法を用いている。そのためより一般的な（変数による）パターンを記述して
いたとしても後に追加したコンストラクタについて別途記述することでその分岐
が優先されるため、頻繁に変数によるパターンが用いられる。その結果、もし追
加したコンストラクタについて記述を忘れた場合であっても、網羅性の検査は常
に通過してしまう。このように、エラーに基づく修正は既存手法でも同様に危険
であることがわかる。ただし、これらの言語では通常テストを用いてこれらの追
加漏れを検知することができるため、それほど大きな問題にはなりにくい。一方、
Coq により検証したプログラムでは、証明という検証プロセスを通過しているた
めにこのようなテストを行わず、バグを残してしまう可能性がある。
他の手法としては、open data type における open 指定子のように、特定の指定子
を持つ関数を探すという手法も考えられる。これにより、拡張しうる箇所を全て
探すことが可能となり、比較的容易に拡張すべき場所を知ることができる。一方、
この open 指定子により、プログラムの拡張可能な箇所が制限されるという問題が
ある。これは open data type における拡張可能な関数がトップレベルでないといけ
ないという制限のために問題となる。例えば式を最適化する関数を考える11 。
open optimize :: Expr -> Expr
optimize v = v
optimize (Add e1 e2) = fold ( optimize e1) ( optimize e2)
fold :: Expr -> Expr -> Expr
fold ( Const n1) ( Const n2) = Const (n1+n2)
fold v1 v2 = Add v1 v2
この中で、Add の場合に内部で最適化の結果を fold 関数に渡して展開している。
この fold 関数は通常の関数として定義しているが、open function として記述する
ことで定数の種類が増えた場合にも対応できるようになる。これらの定義の後に
乗算を導入したとする。このとき、追記する部分は以下のように、fold に似た関
数を記述する必要がある。
11
現時点では定数と演算子しか考慮していないので通常の評価とほとんど同じだが、変数が入っ
た場合などに有用である。
2.3. 既存研究の問題
31
Mult :: Expr -> Expr -> Expr
optimize (Mult e1 e2) = fold2 ( optimize e1) ( optimize e2)
fold2 :: Expr -> Expr -> Expr
fold2 ( Const n1) ( Const n2) = Const (n1*n2)
fold2 v1 v2 = Mult v1 v2
さて、fold2 も fold 同様の処理をしているが、差は畳み込みが乗算であることと
畳み込みがない場合に使用するコンストラクタを変えている点のみである。この
後、定数の種類が追加された場合、fold2 も対応するための拡張を施すべきであ
る。このように考えていくと、結果としてほとんどの関数は open function として
定義されるべきとなってしまう。
プログラマは非常に多くの場合についてデータ構造や関数が拡張されることを
考慮する必要がある。この場合、最終的に得られるプログラムは多くのデータ構
造や関数に open 指定子がついており、プログラム全体を見る場合とほとんど変わ
らなくなってしまう。一方で、拡張対象を制限した場合は、追加の記述がうまく
行かない可能性がある。
33
第 3 章 対話的修正機構
対話的修正機構は、プログラムの修正用コマンド、修正箇所の検知、型検査機
構などの総称である。本章では、対話的修正機構を用いた帰納型の拡張を行うこ
とで修正の流れを説明する。ここでは、対話的修正機構を組み込んだ Coq を ECoq
（Extensible Coq）と呼ぶ1 。
対話的修正機構では、型がつけられるプログラムを拡張した場合に、拡張後の
プログラムも型がつくことを保証する必要がある。そのために、対話的修正機構
の挙動の定義と結果の議論を行う。
3.1 対話的修正機構の挙動
対話的修正機構における修正の流れは以下の通りである。
1. 既存のプログラム全体を読み込ませる。これにより拡張するプログラムの範
囲を限定する。
2. 既存のプログラムの修正を命令によって記述する。
3. 対話的修正機構の出す出力を元に、対話的に影響を受けた箇所を修正する。
本章で導入する修正は以下の二種である。
• 帰納型に新たなコンストラクタを追加する。これはプログラマが明示的に記
述する命令である。
• 対話的修正機構が提示する、コンストラクタの影響を受けたパターンマッチ
に新しいパターンを追加する。これは対話的修正機構からの要求に対するも
のであり、プログラマは証明モードを通して修正を行う。
以下では、前者の命令による修正を能動的修正、対話的修正機構からの提示に応
じて行う修正を受動的修正と呼ぶ。上に示した修正の流れでは、2 が能動的修正で
あり、3 が受動的修正である。
1
対話的修正機構は手法であり、ECoq は実装である。
第 3 章 対話的修正機構
34
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Extend Inductive Aexp : Set :=
| Amult : Aexp ->Aexp ->Aexp.
Extend Inductive Stm : Set :=
| Srepeat : Stm ->Bexp ->Stm.
Extend Inductive NS : Stm ->Env ->Env ->Prop :=
| NSrepeat _T : forall S b e1 e2 ,
NS S e1 e2 -> Beval b e2 = true
-> NS ( Srepeat S b) e1 e2
| NSrepeat _F : forall S b e1 e2 e3 ,
NS S e1 e2 -> Beval b e2 = false
-> NS ( Srepeat S b) e2 e3
-> NS ( Srepeat S b) e1 e3.
Deploy .
(∗ Extensions f o r Aeval ∗)
exact (( Aeval a0 e) * ( Aeval a1 e))%Z.
Defined .
( ∗ E x t e n s i o n s f o r o p t i m i z e _A ∗ )
...
図 3.1: ECoq を用いた構文拡張用のコード。
実際に ECoq において修正を行ったコードは図 3.1 のようになる。ECoq は、Vernacular の拡張として、コンストラクタを追加するためのコマンドである Extend
Inductive コマンド（1–2 行目、3–4 行目、5–12 行目）を備えている。プログラ
マはこのコマンドを通してコンストラクタを追加する。なお、このコマンドの入
力時点では関数や証明などで修正が行われるべき場所を出力することはない。
3–4 行目のコマンドでは文への repeat-until 文の追加を行っている。この結果、
ECoq は以下のような出力を行う。
Stm is extended.
You may extend the following types : NS
2 行目の出力は、NS が Stm に依存しているため、プログラマに修正を提案してい
る。この出力は提案に過ぎず、プログラマが必要ないと判断すれば無視して問題な
い。今回は NS にも拡張が必要であるため、5 行目から 12 行目のように拡張した。
この拡張により、想定していたコンストラクタの追加が完了するので、能動的修
正の終了を知らせる Deploy コマンド（13 行目）により能動的修正を展開する。こ
の展開によって、ECoq は行われた修正の影響を受けた箇所が存在するかを要素の
定義順に確認する。今回の例では、Aexp の宣言から確認を行うが、最初に検知さ
れるのは Aeval による Aexp の展開である。これは、それまでに宣言される Bexp、
3.1. 対話的修正機構の挙動
35
Stm がともに能動的修正の影響を受けていないためである。Aeval における展開は
以下のように表示される。
In Aeval (1 destructors )
fix Aeval (a : Aexp) (e : Env) { struct a} : Val :=
match a with
...
| Amult a0 a1 => _
ˆˆˆˆˆˆˆˆˆˆˆˆˆˆˆˆ
end
このように、拡張する必要のある箇所を、その文脈と共に表示する。文脈は直接関
係のある部分だけであり、例えば同じ箇所でのパターンである Aval などのパター
ンに関しては出力されない。これは、他のパターンが大きな項となっていたとき
に、修正箇所が一見してわからなくなってしまうためである。
ECoq が影響があると判断する箇所は、ワイルドカードパターンなどを考慮せず、
拡張した型を展開するパターンマッチの存在する箇所全てとなっている。そのた
め、2.2 節におけるエラーの検出結果と異なり、Aopt や Sopt などにおけるパター
ンマッチも同様に検知される。
修正箇所が検知されると、ECoq はその場所に入るべき値、すなわちパターン
マッチの返す値を要求する。上の例では、Amult の場合に返す値（この場合は Val
型の値）である。Coq では、証明用の対話によって関数を構築することができる
ため、この要求に対して証明のように記述を行う。そのため、ECoq は上の出力に
続き、以下の出力を行う。
1 subgoal
Aeval : Aexp -> Env -> Val
a : Aexp
e : Env
a0 : Aexp
a1 : Aexp
============================(1/1)
Val
図 3.1 では 15 行目の exact 戦略によって掛け算の評価方法を記述している。なお、
証明による関数の構築はあまり一般的ではないが、図 3.1 で用いている exact や
apply などの戦略を利用することで通常の関数に近い記述が可能であるため、そ
れほどプログラマへの負担は大きくない。
Aeval の補完が終了することで、次の修正箇所の検出と補完が行われる。全て
の要素に対して処理が終了すると、プログラムと証明の修正が完了となる。
第 3 章 対話的修正機構
36
対話的修正機構では既存研究の問題として挙げた点について以下のようにして
解決している。
1. 事前に拡張する型を指定する必要なく全ての型を修正、拡張することがで
きる。
2. 記述はほぼ標準の Coq と同じ記法である。
3. 拡張しうる型について提示することができ、プログラマが拡張の必要性に気
付く機会を増やしている。
3.2 形式的定義
本節では、プログラムの拡張命令と命令に対する挙動の定義を行う。なお、前
節において説明した流れのうち、プログラム全体の読み込みは既に終わったもの
とする。このプログラム全体を宣言の環境 Edef を用いて表す。また、コンストラ
クタの追加が全て終了した時点の拡張の宣言を Eext と表す。ただし、Eext は型の拡
張の宣言のみが含まれる環境である。
前節で説明したとおり、対話的修正機構の持つ機能は帰納型へのコンストラク
タの追加とパターンマッチへのパターンの追加である。しかし、対話の中ではこ
れらの応答の他に帰納型の提案をしていた。本節では、この帰納型の提案の仕組
みについて述べた後、対話的修正機構に基づいて行った修正が健全な修正となっ
ていることの証明を行う。
対話的修正機構では、証明と関数を区別せず、全て pCIC の項として取り扱う。
これにより、議論を pCIC の項における拡張に集中させることができる。
3.2.1
帰納型の提案
経験的に、述語のパラメータとなる型は、その構造をある程度述語に反映して
いることが多い。例えば NS は Stm のそれぞれのコンストラクタについて言及して
おり、非常に密接に関係している。このような述語はコンストラクタの追加時に
拡張される可能性が高いため、提案という形で情報を提示する。
帰納型の依存性検出は、以下の二つの観点によって行われる。
• 拡張した型をパラメータとする。
• コンストラクタの型として拡張した型のコンストラクタを利用する。
3.2. 形式的定義
37
なお、ここでいうパラメータとはコンストラクタの持つパラメータではなく、型
自体についているパラメータである。例えば、Stm はコンストラクタである Sass
にパラメータとして Aexp を持つが、Aexp の拡張時に検出されることはない。
より形式的には、次の通りに定義される。定義環境 E に含まれる帰納型の宣言
について、以下のように宣言されているとする。
I (v1 : T 1 ) . . . (vn : T n ) : T := C1 : T 1′
|
...
| Cm : T m′
型 I ′ が拡張されたとき、T i または T に I ′ が含まれる場合で、かつ T ′j に I ′ のコン
ストラクタを含んでいる場合（かつ I ′ は I ではない場合）にプログラマに拡張を
提案する。
3.2.2
拡張の適用
ここで定義する処理は型の拡張が終了し、要素中のパターンマッチを探す処理
である。この処理には項に対するものと環境中の要素を見つけるものがあり、そ
れぞれ ext と extE と表現する。
まず項 T に対する処理である ext について定義する。この処理は OCaml 風の疑似
コードを用いると図 3.2 のようになる。この中で用いている request term of type
は、プログラマに引数として渡された型の値を要求する関数であり、これが呼ば
れることで第 3.1 節における対話が行われる。なお、pCIC の項と疑似コードを区
別するために、pCIC の項を二重クオートで囲んで表記している。この ext の概要
は以下の通りとなる。
• 項 T が部分項を含む場合、ext を全ての部分項に対し再帰的に適用する。
• 項 T がパターンマッチであり、かつ展開する型 I が Eext にてコンストラクタ
C ′ を追加されているとき、T のパターンに C ′ のパターンを追加し、プログ
ラマにこのパターンが返す値を要求する。この値の型は T の型になる。
ここで定義した ext を Aeval に適用した場合、以下のようになる。なお、fix に
ついては定義していないが、関数抽象同様の扱いをする。
1. Aeval は fix から始まっているため、引数の型および本体に対して eval を
適用する。
2. 引数の型はそれぞれ Aexp と env であり、パターンマッチではなく、また部
分項もないためこれらをそのまま返し値とする。
3. 関数の本体部分はパターンマッチであるため、
第 3 章 対話的修正機構
38
let rec ext T =
match T with
| "Set" | "Prop" | "Type" | "x" | "C" | "I" -> "T "
| "(T 1 T 2 )" -> "((ext T 1 ) (ext T 2 ))"
| "fun x : T 1 => T 2 " -> "fun x : (ext T 1 ) => (ext T 2 )"
| "∀x : T 1 , T 2 " -> "∀x : (ext T 1 ), (ext T 2 )"
| "let x := T 1 in T 2 " -> "let x := (ext T 1 ) in (ext T 2 )"
| "match T ′ return T r with Ptn1 => T 1 | . . . | Ptnn => T n end"
-> let T ′′ = (ext T ′ ) in
let T r′ = (ext T r ) in
∀i ∈ {1..n}, let T i′ = (ext T i ) in
let I ′ = typeof T ′ in
if I ′ ∈ Eext then
begin
∀C j : I ′ ∈ Eext ,
let Ptn′j = pattern _for_ constructor C j in
let B j = request _term_of_type T r′ in
"match T ′′ return T r′ with
Ptn1 => T 1′ | . . . | Ptnn => T n′
| Ptn′1 => B1 | . . . | Ptn′m => Bm end"
end
else
"match T ′′ return T r′ with Ptn1 => T 1′ | . . . | Ptnn => T n′ end"
図 3.2: 疑似コードで表現した項の拡張処理。
Edef の拡張処理 extE では、Edef で定義された全ての定数と帰納型について ext
を用いて拡張し、また Eext における帰納型の宣言を統合する。この処理を疑似コー
ドで書くと図 3.3 の通りである。
3.3 型拡張の制限
前節で述べた処理の健全性は、原則として型が変わらないことを元に証明され
る。そのためには、コンストラクタの追加により型の挙動が変わってしまうよう
な場合を排除する必要がある。コンストラクタの追加によって挙動が変わるのは
パターンマッチの型とソート多相の二点であり、本節ではこれらについて挙動の
変化を回避する制限を述べる。
3.3. 型拡張の制限
39
let rec extE Edef =
match Edef with
| "·" -> Edef
| "x : T ; Edef " -> "x : (ext T ); (extE Edef )"
| "x := T 1 : T 2 ; Edef " -> "x := (ext T 1 ) : (ext T 2 ); (extE Edef )"
| "I (x1 : T 01 ) . . . (x0n : T 0n ) : T :=
| C1 (x11 : T 11 ) . . . (x1m1 : T 1m1 ) : T 1
| ...
| Cl (xl1 : T l1 ) . . . (xlml : T lml ) : T l " ->
∀i ∈ {1..n}, j ∈ {1..l}, k j ∈ {1..m j },
let T 0i′ = ext T 0i in
let T ′jkk = ext T jkk in
let T ′j = ext T j in
if I ∈ Eext then
let C E is a list of constructor of I in Eext in
′ ) . . . (x
′
"I (x1 : T 01
0n : T 0n ) : (ext T ) :=
′
′ ) : T′
| C1 (x11 : T 11 ) . . . (x1m1 : T 1m
1
1
| ...
′ ) : T′
| Cl (xl1 : T l1′ ) . . . (xlml : T lm
l
l
| CE "
else
′ ) . . . (x
′
"I (x1 : T 01
0n : T 0n ) : (ext T ) :=
′
′ ) : T′
| C1 (x11 : T 11 ) . . . (x1m1 : T 1m
1
1
| ...
′ ) : T ′"
| Cl (xl1 : T l1′ ) . . . (xlml : T lm
l
l
図 3.3: 環境 Edef の拡張処理。
3.3.1
パターンマッチの型
パターンマッチの型付け規則は、依存型などの点を除くと一般の関数型言語に
おけるパターンマッチと同様の規則となっている。しかし、述語に対するパター
ンマッチについては制限がかかっている。ここでは、この制限とその例外につい
て説明する。
原則として、述語を分解するパターンマッチは Prop ヒエラルキの要素を返さな
ければならない。なお、Prop ヒエラルキとは、述語およびそれらの要素2 である。
この制約は Coq の関数を他の言語の関数に変換するために存在する。変換時に、
Coq は Prop ヒエラルキに属する定理や証明といった要素を消去し、Set や Type
に属する要素のみを残す。このとき、以下のようなコードを許すと、変換ができ
2
つまりその述語が成立することの証明である。
40
第 3 章 対話的修正機構
なくなる。
fun (t : or P Q) =>
match t with
| or_ introl _ => 0
| or_ intror _ => 1
end
ただし、P および Q は共に述語とする。このような記述が可能である場合、プログ
ラム変換に問題が発生する。変換後のプログラムでは、t が Prop ヒエラルキに属
するため消去されるはずである。しかし、パターンマッチは t の内容に応じて返す
値を変えており、変換後のプログラムは存在しない引数で結果を変えている。こ
のようなプログラムは不可能であるため、変換を考慮している Coq のシステムで
は、パターンマッチは述語を展開する場合 Prop ヒエラルキに属する要素を返さな
ければならない。
ただし、この原則には例外が存在する。述語を展開する場合でも、その型が empty
definition や singleton definition と呼ばれる定義である場合、Prop ヒエラルキ以外
の型を返すことが許される。Empty definition とはコンストラクタを持たない型の
定義であり、また Singleton definition とは、単一のコンストラクタを持ち、かつコ
ンストラクタのパラメータが全て Prop ヒエラルキに属する型の定義である。これ
らの型を展開する場合では、パターンマッチにより現れる全てのパラメータは変
換時に無視され、結果としてそのパターンマッチによって生成された要素は一切
変換後の実行に寄与しない。そのため、変換時にパターンマッチそのものを無視
することにより変換が可能となる。例えば、eq は singleton definition であるため、
以下の宣言は変換可能であり、記述が許される。
Definition f (t : eq x) : nat :=
match t with
| refl_ equal => 0
end.
型 eq の唯一のコンストラクタである refl_equal はパラメータを持たないため、
t はパターンマッチの結果に寄与していない。この宣言を OCaml のプログラムへ
変換すると以下のコードになる。
let f _ = 0
これらの例外はコンストラクタの数に依存している。したがって、ECoq でコン
ストラクタを増やした場合、例えば singleton definition の型を拡張した場合、その
型が singleton でなくなってしまうため、パターンマッチが記述できなくなる場合
が考えられる。
3.3. 型拡張の制限
41
この問題を回避するために、対話的修正機構では singleton definition の拡張を
禁止し、また empty definition の拡張を singleton にするまでに制限する。Empty
definition および singleton definition は一般に特殊な状態の表現に用いられるため、
拡張を行うことはまれであると考えられる。したがって、この制約は十分に実用
的である。
3.3.2
ソート多相
帰納型はパラメータを受け取り、結果としてソート（Set、Prop または Type）
に属する。このソートを帰納型の結果のソートと呼ぶことにする。また、パラメー
タが残っている状態の型をアリティと呼ぶ。
ソート多相とは帰納型における結果のソートをできる限り小さくするものであ
る。ソートは Prop、Set、Type の順に大きいとみなされる3 。より小さなソートは
Conv 規則によってより大きなソートとして扱えるため、結果のソートが小さい方
がより適用可能な範囲が広く、有用である。
Coq におけるソート多相は pCIC におけるそれと異なり、結果のソートが Type
である帰納型にのみ適用される。このソート多相は以下の手順で決定される。この
帰納型が、empty または singleton definition として見られる場合、この結果のソー
トを Prop とみなす。そうでない場合に、もしも Set として見られるほど小さい場
合、結果のソートを Set とみなす。どちらにも当てはまらない場合は、定義通り
に Type とみなす。
ソート多相はパラメータによっても発生する。この点においても、Coq では Type
型および結果が Type 型である全称型のパラメータに限定している。この典型的な
例としてはライブラリに存在する list が挙げられる。Coq で用いられている list
の定義は以下の通りである4 。
Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.
この定義では、list は Type->Type として定義されている。しかし、パラメータ A
には conversion rule によって Set や Prop の要素も与えられる。例えば、nat は Set
に属するが、Conv 規則によって Type に属すると扱うことによって、list nat は
正しい型となる。
3
2.1.2 節のサブタイプ関係で定義されている。Coq8.2 までは Prop と Set に大小関係は存在し
なかったが、8.3 から Prop は Set より小さくなった。
4
2.1.1 節の list とはパラメータのソートが異なるが、それ以外は同じである。
第 3 章 対話的修正機構
42
このとき、Coq では list nat を Set として扱うことができる。これは list の
定義においてパラメータ A を nat に置き換えたときに、list の大きさが Set の要
素となる程度に小さいためである。
しかし、コンストラクタの追加によって、このソート多相が破壊される可能性
がある。例えば、次のコンストラクタを list に追加してみる。
ins : forall B : Type , B -> list A -> list A
このコンストラクタは、list に任意の型の要素を入れることを可能にする。しか
し、このコンストラクタを list に追加した場合、list のソート多相の挙動が変化
する。例えば list nat は自然数のリストだったものだが、コンストラクタ ins は
あらゆる要素をリストに入れることを許しており、ins の型は常に Type に属する。
このため、ins のコンストラクタを追加した list nat は Type として扱われる。
次節で議論する健全性には型の保存が必要であり、したがってソート多相の挙
動が変化する拡張は許容できない。そのため、コンストラクタの追加によってソー
ト多相が保存されているかを常に確かめなければならない。幸い、Coq 内部にお
いてソート多相は、型に存在するどのパラメータに依存してソートが変わるかを
保存しており、使用時はその中の最も小さいソートとするように実装されている。
したがって、この依存性を拡張前の定義と比較することでソート多相が保存され
ているかを容易に確かめることができる。
3.4 拡張の健全性
3.2 節の定義では、命令の挙動について述べた。本節では、この挙動に基づいて
行われる拡張が健全な形での拡張になっていることを証明する。
まず、対話的修正機構における仮定について確認する。
• 拡張前のプログラムは正確に型がつく。
• 拡張は既存のプログラム構成を変更しない。
• 拡張箇所はその時点での環境、文脈の整合性を壊さない。
これらの仮定を元に、次の健全性について証明を行う。
定理 1 (拡張の健全性). 拡張前の環境 E においてある環境で E[Γ] ⊢ t : T が成立し、
また WF (E)[Γ] も成立すると仮定する。E 、Γ、t、T に対して拡張処理を行った結
果を Ee 、Γe 5 、te 、T e とすると、Ee [Γe ] ⊢ te : T e が成立する。また、WF (Ee )[Γe ] も
成立する。
5
局所文脈に対する拡張は定義していないが、内部に含まれる項を全て拡張する処理とする。
3.4. 拡張の健全性
43
元のプログラムにおける型付けの導出木の高さに基づく完全帰納法を用いて証
明する。
導出木の高さが 1 の場合、使用可能な規則は W-E 規則のみであり、これは E = ·
および Γ = · を意味する。拡張する対象が存在しないため、Ee = · および Γe = · と
なり、明らかに拡張後も W-E 規則を適用できる。よって、高さが 1 の場合定理が
成立する。
導出木の高さが自然数 n に対し n + 1 と表現できるとき、帰納法の仮定から高さ
n 以下である型付けの導出木は拡張後も同様に型がつけられる。以下では、導出木
の最後に使用した規則に応じて場合分けを行う。
多くの規則では導出の仮定部分が型付けの導出規則に依存しており、帰納法の仮
定を使うことで拡張後も導出が可能であることを示すことができる。例えば、ソー
トの型付けを見ると、次の形をしている。
WF (E)[Γ]
E[Γ] ⊢ Prop : Typei
この規則を利用したことから、WF (E)[Γ] が成立することがわかる。一方、この
文脈の整合性の導出木は高さが n であるから、帰納法の仮定から WF (Ee )[Γe ] を
導くことができる。したがって、同じ規則を使うことで、Ee [Γe ] ⊢ Prop : Typei を
示すことができる。このように、導出の仮定として出現する文脈の整合性や項の
型付けに関する規則に関しては拡張後も成立することを直ちに示すことができる
ため、同じ規則を用いることを前提として証明を行うことで多くの導出の仮定を
満たすことを容易に示すことができる。そのため、以下の証明では仮定に文脈の
整合性や項の型付けに関してのみ用いる規則の証明は省略する。
これら以外を含む、または仮定から直接導けない要素を含む規則は、Conv 規則、
W-Ind 規則、Ind-Family 規則、match 規則の 4 つである。以降、これらについて
証明を行う。
Conv 規則の場合 Conv 規則は、項 t に型 T が付けられ、T ≤βιδζη U を満たす U
が型であるとき、項 t は型 U が付けられるという規則である。帰納法の仮定から、
項 te に型 T e がつくこと、および Ue が型であることが得られる。ただし、ここで
te は t を拡張した項、T e は T を拡張した項、Ue は U を拡張した項であるとする。
残る仮定は、T e ≤βιδζη Ue である。この関係を成立させるため、まず各種の簡約に
ついて考える。
定理 2 (簡約の保存). 拡張前の環境 E および文脈 Γ において、E[Γ] ⊢ T ▷ x T ′ (ただ
し x は β, ι, δ, ζ のいずれか）とする。このとき、拡張後の環境 Ee 、文脈 Γe 、項 T e
に対して、Ee [Γe ] ⊢ T e ▷ x T e′ となる T e′ が存在し、この T e′ は T ′ への拡張によって
得られる。
44
第 3 章 対話的修正機構
証明. x について分けて考え、T と T e の関係から証明を行う。なお、どの簡約に対
しても簡約基が拡張の結果簡約基でなくなることはないため、この点については
省略する。β 簡約や ζ 簡約の場合、それぞれの簡約における右辺において代入が行
われている対象を代入後に拡張することで T e′ が得られる。δ 簡約の場合、置き換
えた環境や文脈の要素が既に拡張後の要素であるため T e′ は明らかである。ι 簡約
の場合、簡約の結果はパターン本体に対して代入が行われるが、代入結果に対し
て β 簡約や ζ 簡約と同様に拡張を行うことで T e′ が得られる。
□
この結果を再帰的に適用することで、T =βιδζη U であれば T e =βιδζη Ue であるこ
とが証明でき、また T ≤βιδζη U から T e ≤βιδζη Ue が導出できることについても帰納
法によって証明できる。これにより、型付け規則における Conv 規則の仮定が全て
成立することがわかった。したがって、拡張後の項も Conv 規則を用いて導出さ
れる。
W-Ind 規則の場合 コンストラクタの増加によって仮定にコンストラクタが一つ
追加されている。しかし、仮定として拡張時には文脈は整合性があり、また追加
されたコンストラクタの型は元の宣言と同じものであるため、ソートは同様に付
けられる。したがって、帰納法の仮定と合わせることで全体は W-Ind 規則を用い
て型をつけられる。
Ind-Family 規則の場合 3.3.2 節にて導入した制限は、この規則に対する挙動が不
変であることを保証していた。したがって、拡張後の項も Ind-Family 規則によっ
て型がつけられる。
match 規則の場合 導出木の仮定には、パターンマッチによって展開する項の型
付け、返し値の型の型付け、帰納型についてのパターンマッチが許されるもので
あることと、それぞれのパターンに関する型付けである。これらの仮定から拡張
後の結果を直接導くことができないものは、帰納型についてのパターンマッチが
許されるものであること、また追加したパターンに関する型付けである。しかし、
帰納型のパターンマッチの型については、3.3.1 節において与えられたパラメータ
によらず不変であるように制限したため、拡張前同様に保持されていることがわ
かる。追加されたパターンについては、追加する処理において求める型がパター
ンマッチの結果の型であり、したがって他のパターン同様に型がつけられる。
以上帰納法により、拡張処理後も型がつけられ、また文脈が整合性を保つこと
が示された。
□
拡張の健全性から、対話的修正機構を用いた拡張では、元のプログラムで型が
付くならば修正後のプログラムでも型が付くことが保証される。言い換えると、
3.5. 帰納原理関数
45
ECoq で修正を行った定理の正しさはこの健全性によって保証されている。逆に言
えば、健全性の証明にミスがある場合、ECoq で修正を行った定理は正しくない可
能性がある。
通常、定理証明支援系では証明した定理の正しさを最小限度の型や論理の体系
によって保証する。これは人間の行う定理証明には誤りが混入しうるためであり、
そのようなことが起こらないように体系を小さくし、証明をできる限り小さくし
ている。表層言語の記述での正しさは、その体系へ変換することで保証する。例
えば Coq における定理の正しさは pCIC の型体系の健全性に基づいている。この
視点では、ECoq で修正を行った定理の正しさを上で証明した拡張の健全性に求め
ることは危険である。
拡張の健全性を別の視点から見ると、これは対話的修正による拡張の後戻りを
防ぐことを意味している。修正後の定理は pCIC の項であるため、その正しさを
pCIC によって保証することができる。この場合、修正後に pCIC の型検査が行わ
れ、結果として型付けできない場合がある。拡張の健全性はこのようなことが起こ
らないことを示しており、対話的修正が終了しながら定理の証明をやり直す必要
はなくなる。この視点では、修正後の定理の正しさは pCIC に依存しており、Coq
の信頼性と同等であるといえる。
本研究において実装した ECoq では前者の視点に基づいているため、正しさの保
証が十分ではない。しかし後者の視点とするために修正後の項に対して pCIC によ
る検査を導入することは容易であり、本質的な問題とはならない。
3.5 帰納原理関数
pCIC に対する拡張の健全性を証明したが、ECoq として実装する際に一つ問題
が発生する。それは構造帰納法（以下単に帰納法）のために定義される帰納原理
関数（induction scheme）である。
帰納原理関数は、帰納型の宣言時に自動で定義される関数であり、帰納型 I に対
して、I rect、I rec、I ind の三つ、または最後の一つだけが定義される。これ
らはそれぞれ帰納法を表し、Type に属する要素を返す場合、Set に属する要素を
返す場合、Prop に属する要素を返す場合に使用される。なお、これらの関数では
内部でパターンマッチが使用されているため、3.3 節にて述べたパターンマッチの
型の制約によって定義されない関数も存在する6 。
帰納原理関数の型について説明するために、ここでは Aexp ind の型について述
べる。乗算を追加する前の Aexp ind の型は以下のようになっている。
6
したがって、singleton/empty definition ではない Prop 型に対しては最後の一つだけが宣言され、
他は三つとも宣言される。
46
第 3 章 対話的修正機構
1 Aexp_ind :
2
forall (P : Aexp -> Prop),
3
( forall v : Val , P (Aval v)) ->
4
( forall v : Var , P (Avar v)) ->
5
( forall a : Aexp , P a -> forall a0 : Aexp , P a0 ->
6
P (Aadd a a0)) ->
7
forall a : Aexp , P a
ここで、パラメータになっている P は帰納法によって証明する命題である。また、
続く三つのパラメータは帰納法における、それぞれのコンストラクタの場合に対
する証明である。具体的には、一つ目は値について、二つ目は変数について、三
つ目は加算についての証明となっている。
これらの P に続くパラメータの数は帰納型のコンストラクタの数に対応してい
る。つまり、帰納型に新しいコンストラクタを追加すると、結果的に帰納原理関
数はパラメータ数が増えてしまう。実際に、Aexp に乗算を追加した後の Aexp ind
の型は以下のようになる。
1 Aexp_ind :
2
forall (P : Aexp -> Prop),
3
( forall v : Val , P (Aval v)) ->
4
( forall v : Var , P (Avar v)) ->
5
( forall a : Aexp , P a -> forall a0 : Aexp , P a0 ->
6
P (Aadd a a0)) ->
7
( forall a : Aexp , P a -> forall a0 : Aexp , P a0 ->
8
P (Amult a a0)) ->
9
forall a : Aexp , P a
比較すると、7 行目から 8 行目にかけて記述されているパラメータが追加されてお
り、それが乗算に対する命題 P の証明であることがわかる。場合分けと対比した
場合、対話的修正機構はこの追加された証明を要求すればよいと考えられる。そ
の場合、この証明の追加はパターンマッチにおけるパターンの追加と同様に行う
ことができる。
しかし、この手法はパターンマッチと大きく異なる点があり、定数として宣言
された帰納原理関数の型が拡張処理によってありうる変更を超えて異なっている
点である。そのため、定数における型付けの規則が成立しなくなってしまう。こ
れは、帰納原理関数が高階関数の引数として与えられたときに顕著であり、引数
としての型が合わなくなる。この型を合わせるには他の箇所で型を変更する必要
があり、この変更が連鎖する。
一方、帰納原理関数を帰納法における使用に限った場合、帰納原理関数が出現
する箇所は全てパラメータが与えられている。この場合、帰納原理関数に増えた
3.5. 帰納原理関数
47
let rec ext T =
match T with
| ((. . .((c T 1 ) T 2 ) . . .) T n )
where c is induction _ scheme for I and I is extended ->
let m = number _of_ parameter x in
if m > n then abort ( ∗ b r e a k i n g l i m i t a t i o n ∗ )
else
∀i ∈ {1..n}, let T i′ = ext T i in
∀C j : I ∈ ΓE , let B j = request _term_of_type T 1′ in
"((. . .(((. . .(((. . .((c T 1′ ) T 2′ ) . . .) T m′ ) B1 ) . . .) B j )
′
T m+1
) . . .) T n′ )"
| . . . ( ∗ t h e same a s Figure 3.2 ∗ )
図 3.4: 帰納原理関数に対応した拡張処理。ただし図 3.2 に書かれた部分は . . . とし
ている。
パラメータは関数適用の形で与えることで、型の変化を局所に抑えることができ
る。よって、ECoq では帰納原理関数は全て出現した場所で全てのパラメータを与
えられていなければならないとする。
このパラメータの検査と拡張を行うため、図 3.2 で定義した ext を修正した（図
3.4）。追加した処理は、まず与えられた項が関数適用である間、関数側を再帰的
に展開し、適用される関数の位置に帰納原理関数が用いられているかを調べる7 。
用いられていなければ通常の処理に戻り、用いられていれば与えられているパラ
メータの数を数える。与えられているパラメータの数が帰納原理関数のパラメー
タの数を下回っていた場合、制限に違反しているので拡張そのものを中止する。こ
れは、修正すべき箇所を ECoq が判断することが困難となるためである。充分な数
のパラメータが与えられていれば、そのパラメータを再帰的に全て拡張し、さら
に追加されたコンストラクタに対応する証明をプログラマに要求する。
Coq では帰納原理関数として別途プログラマが定義した関数を用いる場合があ
る。コンストラクタを追加した場合、これらの関数は新しいパラメータが必要に
なる可能性が高いが、現在の ECoq にはパラメータを追加する機能が存在せず、拡
張が不可能である8 。そのため、ECoq においては Coq が自動で作成する帰納原理
関数に限定して拡張に対応している。
7
関数適用が存在せず、直接定数がある場合もこの分岐に入る。
整楚帰納法のように特定の述語に従った帰納法の場合は述語にコンストラクタを追加すること
で対応できる場合もある。この場合、帰納法としてではなく通常の関数として扱う限り、ECoq で
対応できる。
8
第 3 章 対話的修正機構
48
3.6 使用例と問題点
対話的修正機構は、2.2 節に挙げた検証済みプログラムに対してのみならず、数
学的な定理に対しても適用可能である。例えば Curry-Howard 同型における対応関
係を証明するには、定義として
• 型付きラムダ計算の型と項、変数の型環境、型付け規則
• 論理式、仮定の環境、推論規則
• 論理式と型の対応関係
が必要となる。これらは全て帰納型として定義される。
ここで、型付きラムダ計算に組を入れることを考える。 起点を組を作る項の宣
言とすると、このときの流れは次のようになる。
1. 要素として組を入れると、パラメータとの関係から型付け規則の拡張を促さ
れる。
2. 型付け規則に組を追加するには型を追加しなければならないので、型の拡張
について記述する。
3. 型の拡張によって、論理式と型の対応関係の拡張を促される。
4. 論理式に論理積を増やす必要があるので追加する。
5. 論理式の拡張によって推論規則の拡張を促される。
このように、全て帰納型の拡張から次の拡張をたどるという流れになる。この中
では一切関数による処理は出てこないため、エラーに基づく修正は困難だが、対
話的修正機構の提案によって全体の修正を行うことができる。
一方、起点を論理式への論理積の追加とすると、論理式と方の対応関係の拡張
を促され、そこから型やラムダ計算の要素の追加につながる。このように、比較
的変更の開始地点はある程度自由に選ぶことができる。
対話的修正機構は、既存の挙動を置き換えることができないが、一方で置き換
えない拡張であれば記述が可能である。これを利用すると、重要な機能のみを検
証し、段階的に機能を追加することが可能となる。このような場合、性質の記述
や証明手法は最初に検証した機能に強く依存するため、他の機能の導入には挙動
を置き換える必要がないことが多い。また、この場合段階的に導入する機能に関
する検証はそれほど困難な作業ではないため、導入の分業などを考えることがで
きる。
3.6. 使用例と問題点
49
fun a : Aexp =>
Aexp_ind
(fun a0 : Aexp =>
forall e : Env , Aeval a0 e = Aeval (Aopt a0) e)
(fun (v : Val) (e : Env) =>
eq_refl ( Aeval (Aopt (Aval v)) e))
(fun (v : Var) (e : Env) =>
eq_refl ( Aeval (Aopt (Avar v)) e))
(fun (a1 : Aexp)
(IHa1 : forall e : Env , Aeval a1 e = Aeval (Aopt a1) e)
(a2 : Aexp)
(IHa2 : forall e : Env , Aeval a2 e = Aeval (Aopt a2) e)
(e : Env) =>
eq_ind_r
(fun v : Val =>
(v + Aeval a2 e)%Z =
Aeval
match Aopt a1 with
| Aval z1 =>
match Aopt a2 with
| Aval z2 => Aval (z1 + z2 )%Z
| Avar _ => Aadd (Aopt a1) (Aopt a2)
| Aadd _ _ => Aadd (Aopt a1) (Aopt a2)
end
| Avar _ => Aadd (Aopt a1) (Aopt a2)
| Aadd _ _ => Aadd (Aopt a1) (Aopt a2)
end e)
... ( ∗ 80 l i n e s l e f t ∗ )
図 3.5: Aopt keep result の証明を表す項の一部。
一方で、この手法における問題として、証明を項として扱っていることが挙げ
られる。この問題を明らかにするために、最初の例題の中にある、算術式の最適
化の正しさに関する証明項を見る。項の一部を図 3.5 に記載した。この項に出現す
るパターンマッチ式は 11 個あり、その全てが Aexp を展開しているため、拡張時
に ECoq が拡張を要求する。一方で、エラーに基づく修正を行った場合（ただし証
明以外は全て適切に修正を行ったものとする）、実際に提示した証明では使う戦略
の範囲では変更は不要であり、連結を一部解除すると乗算の場合に関する証明の
み追加する必要があった。
このように、ECoq の検知は保守的であり、検知する数は実用的ではない。次章
では、この問題を解決するために、証明を項だけでなく既存の証明から再構築す
50
る方法について議論する。
第 3 章 対話的修正機構
51
第 4 章 記述の再利用
前章における対話的修正機構では、確実なプログラムの拡張が可能であること
を示した。しかし、例題において説明したとおり、プログラムの拡張箇所はエラー
を元にした修正に比べると多くなりがちであり、また特に証明においては非常に
修正対象のわかりにくいものが少なくない。本章では、既存のプログラム記述を
用いることで、修正を容易にする方法を導入する。
4.1 問題点
ECoq に基づく検知は、エラーに基づく修正に比べて非常に多く検知する。この
中には本来修正すべき箇所も存在するが、経験的には証明項において検知される
箇所は大半がエラーに基づく修正で要求される場所ではない。証明項における過
剰な検知を行った箇所では、場合分けに相当するパターンマッチの返し値の型が
展開している値に依存していることが多く、結果的に型においてもパターンマッ
チが生成される。このパターンマッチは非常にわかりにくく、プログラマが何を
記述すべきかを理解するのは難しい。例えば inversion 戦略を用いると、次のよ
うなパターンマッチが現れる。
eq_ind (Sass v1 a1)
(fun e6 : Stm =>
match e6 with
| Sass _ _ => True
| Sskip => False
| Sif _ _ _ => False
| Swhile _ _ => False
| Scomp _ _ => False
end) I Sskip H12
これは与えられた文に対してどのケースが起こりうるかを True または False で表
している。しかし、repeat-until 文の導入時に Srepeat に対してどちらを返すべき
かを判断することは難しい1 。
1
なお、この場合は与えられた文が Sskip であることを表しているため、Srepeat に対しては
False を返すべきである。
第4章
52
記述の再利用
これらは、証明時に戦略が自動で生成し、依存性に対応したゴールを生成して
いるため、プログラマはほぼ意識する必要のない箇所である。したがって、プロ
グラマの負荷を抑えるためにも、上のように難解なパターンマッチは自動で処理
をすべきである。そのためには、どの戦略によってそのパターンマッチが生成さ
れたかを考える必要がある。
本章で導入する記述の再利用では、元の記述から処理可能な箇所について処理
を行う。しかし、関数と証明では、全ての箇所で自動的な修正を行ってよいか否
かの判断が異なる。
証明の場合、一般に証明の過程はほぼ問題ではなく、本質的には証明ができた
か否かを重視する。それゆえ、自動的に処理可能な箇所を最大限埋めることは問
題ないことが多い。よって、証明に対して、ECoq は可能な限り自動処理を行う。
なお、自動処理の結果 ECoq が検出した箇所に埋め込まれる項を修正候補と呼ぶ。
関数については、2.2 節において述べたとおり常に修正候補を用いて良いとは限
らない。第 3 章における ECoq はこの問題に対して全て修正候補を用いない選択を
したと考えられるが、この選択はプログラマに全てのパターンマッチの処理を要
求してしまう。一方、同じ例題にも出現したが、ワイルドカードパターンの中に
は修正候補としてそのまま使ってよい場合もある。したがって、プログラマに使
用可能な状態で修正候補を提示することが有用と考えられる。
これらの違いのために、関数と証明を明確に区別する必要がある。通常 Coq を
使用する場合、証明には戦略を、関数には項を用いて記述する2 。よって、本章の
手法では、プログラムは全て関数で書かれており、また証明は全て戦略を使って記
述されているとする。この仮定の下では、関数における補完を保守的にし、修正
候補の利用についてプログラマに問うことで安全に拡張を行うことができる。ま
た、証明では戦略によって導出された修正候補を最大限利用し、可能な限り検知
を減らすことができる。
なお、本章の記述は元のプログラムを記述したコードが存在することを仮定し
ている。これは、プログラムを対話的に入力した場合や、コンパイル結果しか残っ
ていない場合、Coq は元のプログラムをどのように作成したかという履歴を一切
持たないためである。
4.2 関数の補完
パターンマッチにおける拡張では、ワイルドカードパターンや変数によるパター
ンによって起こる補完を無視することですべてのパターンマッチを対象にした。し
かし、これらのパターンを使うパターンマッチの中には拡張部分もこれらのパター
2
依存型の記述に戦略を用いることはある。今回はこの場合について考えない。
4.2. 関数の補完
53
ンに基づいて動くものもある。例えば第 2.2 節で挙げたプログラムでは、Aopt に
おいて検出の対象となるパターンが二箇所で用いられている。このうち、外側の
パターンマッチ（引数を直接展開しているパターンマッチ）では、コンストラク
タの追加時に最適化できないとして無視されてしまう。一方で、内側のパターン
マッチ（加算だった場合に部分式の最適化の結果で分岐している）では、定数の
場合以外には処理できないため、多くの場合コンストラクタの追加時にも新しい
パターンを追加する必要はない。
このように、同じ関数内のパターンマッチであっても、頻繁にパターンが追加
される場所と希にしか追加されない場所があり、またそれぞれも確実に追加され
るかされないかが決定できない。この決定はプログラマによってのみ可能である
ため、対話的修正機構は既存のパターンマッチで補完されうる要素をプログラマ
に問うことで容易な拡張を可能とする。
補完候補の発見は以下の手順で行われる。
1. 関数内のパターンマッチを発見する。
2. 対応するパターンの記述を探す。
3. 現在の帰納型の状態を用いて対応するパターンマッチを展開する。
4. 展開後のパターンマッチの中で、補完候補となるパターンが見つかるかを調
べる。
例えば、Aopt の例を用いると、Amult の追加前の環境には、以下の通りに格納
されている。
fix Aopt (a : Aexp) : Aexp :=
match a with
| Aval _ => a
| Avar _ => a
| Aadd a1 a2 =>
let (a1 ’, a2 ’) := (Aopt a1 , Aopt a2) in
match a1 ’ with
| Aval z1 =>
match a2 ’ with
| Aval z2 => Aval (z1 + z2)%Z
| Avar _ => Aadd a1 ’ a2 ’
| Aadd _ _ => Aadd a1 ’ a2 ’
end
| Avar _ => Aadd a1 ’ a2 ’
| Aadd _ _ => Aadd a1 ’ a2 ’
end
end
54
第4章
記述の再利用
一方、Amult 追加後には、Aopt は以下のように展開される。
fix Aopt (a : Aexp) : Aexp :=
match a with
| Aval _ => a
| Avar _ => a
| Aadd a1 a2 =>
let (a1 ’, a2 ’) := (Aopt a1 , Aopt a2) in
match a1 ’ with
| Aval z1 =>
match a2 ’ with
| Aval z2 => Aval (z1 + z2 )%Z
| Avar _ => Aadd a1 ’ a2 ’
| Aadd _ _ => Aadd a1 ’ a2 ’
| Amult _ _ => Aadd a1 ’ a2 ’
end
| Avar _ => Aadd a1 ’ a2 ’
| Aadd _ _ => Aadd a1 ’ a2 ’
| Amult _ _ => Aadd a1 ’ a2 ’
end
| Amult _ _ => a
end
この中には、Amult が出現するパターンが三箇所ある。これらは全て対話的修正
が修正を求めるパターンである。本節で提案する修正候補の生成では、これらの
本体を修正候補とする。
なお、ここで生成された修正候補のうち、最外のパターンマッチにおける修正
候補は本来の拡張と異なるが、他二つの修正候補は本来の拡張と同じである。こ
れらを用いることで、関数の拡張を重要な箇所に限定して行うことができる。
4.3 証明の補完
あるゴールの証明時に戦略を適用すると、結果としてエラーが発生するか、い
くつかのサブゴールが現れる。いうまでもなく、一度完成したプログラムではエ
ラーは発生しない。したがって、拡張後のプログラムにおいて証明時に発生するエ
ラーは、全て追加したコンストラクタにより引き起こされている。逆に言えば、証
明を再利用するためには追加したコンストラクタによって引き起こされたエラー
を隠蔽し、元のプログラムで存在した証明を同様に模倣すれば、元の証明を記述
から復元することができる。このとき、分岐やエラーを隠蔽するだけでなく、可
能な限り既存の記述による証明を行うことで、証明の補完候補を得る。
4.3. 証明の補完
55
以下では議論のために、拡張したプログラムにだけ現れるサブゴールを追加サ
ブゴールと呼ぶ。また、元のプログラムにおいて出現していたサブゴールを基本
サブゴールと呼ぶ。追加サブゴールはその性質上、必ず証明する箇所を関数とし
て表したときにその文脈中に追加したコンストラクタが現れる。逆に、追加した
コンストラクタを文脈に含まないサブゴールは基本サブゴールである。これらの
用語を用いると、上に記述したエラーの発生する箇所とは全て追加サブゴールで
あるといえる。したがって、まず追加サブゴールを証明中から得ることについて
考える。
Ltac の中には、証明中に発生するエラーから復帰することができるコマンドが
複数ある。今回の範囲では try コマンドや repeat コマンドがそれに当たる。例え
ば try コマンドでは複数のサブゴールに適用する際にいくつかは容易に証明でき
るが、一部のサブゴールではエラーになる場合に使用できる。また、サブゴール
を不可逆に変化させる戦略（constructor などの適用や elim など）を使用する際
に、fail 戦略を末端に用いることで証明できない場合に元の状態へ復帰する、と
いう使用もある3 。repeat コマンドは try コマンドと異なり、通常は同じ戦略の
複数回の適用を行うためだけに使用されるが、失敗時に最後の成功時に復帰する
という意味で try コマンドと同様の記述ができる。
これらのコマンドによって、以下の問題が発生する。
1. 連結された戦略の先頭で複数のサブゴールが出現した。以下はこの中の一つ
のサブゴールに注目したとする。
2. 次に try コマンドが実行された。
3. try コマンドの内部で induction や descruct などで場合分けが行われた。
4. 基本サブゴールは全て正常に終了した。したがって、拡張前のプログラムで
はこの try コマンドは正常に通過している。
5. 追加サブゴールが失敗し、try コマンドがその失敗を補足した。したがって、
状態が try コマンドの直前に戻された。
この流れでは、いくつかの問題が発生している。まず、本来は正常に通過するは
ずの証明が行われていない点である。これは 4 に述べたとおり、基本サブゴール
は正常に終了したため、拡張前のプログラムは正常に戦略が実行されたはずであ
る。しかし、結果として try ブロックの直前に戻ったため、本来行われるはずだっ
た処理が行われていないことになる。
3
Sopt keep semantics の証明時にこのパターンを用いた。特定のサブゴールを除くと全て証
明できる場合に使用している。
56
第4章
記述の再利用
もう一点の問題は、戻った状態は基本サブゴールである点である。したがって、
前述の通り証明の流れが変わってしまうため、証明の記述はどこかでエラーを発
生してしまうが、一方でそのエラーには追加サブゴールが関与していないという
状態になる。そのため、プログラマにとっては証明に存在する問題が非常にわか
りにくくなってしまう。
これらの問題点は、基本的に追加サブゴールを基本サブゴールと同様に扱って
いる点にある。そのため、追加サブゴールの失敗に引きずられて全体が失敗する、
という流れになっている。これは try コマンドを用いずともやはり発生する問題
であるため、追加サブゴールは基本サブゴールと異なる扱いをする必要がある。
追加サブゴールと基本サブゴールの扱いの違いは、追加サブゴールにおけるエ
ラーはエラーとして捉えず、基本サブゴールにおけるエラーはエラーとして扱う
点にある。したがって、分岐によって複数のサブゴールが得られた場合、即座にそ
れらを追加サブゴールと基本サブゴールに分ける。そして、基本サブゴールに対
して戦略を実行し、失敗しなければ追加サブゴールに対して戦略を実行する、と
いう流れになる。これを疑似コードとして表現したものが図 4.1 と図 4.2 である。
なお、candidate は基本サブゴールと追加サブゴールにわけながら基本サブゴー
ルを優先して証明する処理であり、candidateA は追加サブゴールだけの証明を試
みる処理である。
candidate が返す値は (O, A p , A s ) という三つ組みであり、それぞれ基本サブゴー
ルの集合、追加サブゴールのうちエラーを出さなかったものの集合、追加サブゴー
ルのうちエラーを出したものの集合である。追加サブゴールについて分けている
二つは、続く戦略が存在する場合に処理するか否かによって分かれている。A p は
candidate において基本サブゴールが正常に終了した場合に candidateA に渡さ
れ、可能な限り証明を進められる（図 4.1 の 9 行目）。これらの処理では execute
や filter という関数を使用しているが、これらはそれぞれ与えられた戦略を通常
通りに実行する関数と、与えられたサブゴールの集合から基本サブゴールと追加
サブゴールとに分ける関数である。なお、ここでは execute 関数はエラーを起こ
した場合に error という例外を投げるものとする。また、上で述べたとおり基本
サブゴールと追加サブゴールは証明の文脈に追加したコンストラクタが含まれる
かによって分けられる。
追加サブゴールに対する処理である candidateA では、try コマンドや repeat
コマンドについて処理する際に、A s が空かどうかを調べている。これは A s が追
加サブゴールのうち既に処理においてエラーを起こしたものであり、要素が存在
するということは try コマンドや repeat コマンドが補足しなければならない。そ
のため、空かどうかの判定によって結果をそのまま返すか candidateA に渡され
た状態に戻すかに分岐している。
4.3. 証明の補完
let rec candidate t o =
match t with
| "atomic tac" ->
let (O, A p ) = filter ( execute t o) in
(O, A p , ϕ)
| "t1 ; t2 " ->
let (O, A p , A s ) = candidate t1 o in
∀oi ∈ O, let (Oi , A pi , A si ) = candidate t2 oi in
∀a j ∈ A p , let (A′p j , A′s j ) = candidateA t2 a j in
∪
∪
∪
∪
∪
( i Oi , i A pi ∪ j A′p j , A s ∪ i A si ∪ j A′s j )
| "t′ ; [t1 | t2 | . . . |tn ]" ->
let (O, A p , A s ) = candidate t′ o in
if |O| <> n then raise error
else
∀oi ∈ O, let (Oi , A pi , A si ) = candidate ti oi in
∪
∪
∪
( i Oi , A p ∪ i A pi , A s ∪ i A si )
| "try t′ " ->
try
candidate t′ o
with
error -> ({o}, ϕ, ϕ)
| "repeat t′ " ->
try
let (O, A p , A s ) = candidate t′ o in
∀oi ∈ O, let (Oi , A pi , A si ) = candidate t oi in
∀a j ∈ A p , let (A′p j , A′s j ) = candidateA t a j in
∪
∪
∪
∪
∪
( i Oi , i A pi ∪ j A′p j ∪ j A′s j , A s ∪ i A si )
with
error -> ({o}, ϕ, ϕ)
図 4.1: 優先的に基本サブゴールに戦略を適用する処理。
57
第4章
58
記述の再利用
let rec candidateA t a =
match t with
| "atomic tac" ->
try
let ( , A p ) = filter ( execute t a) in
(A p , ϕ)
with
error -> (ϕ, {a})
| "t1 ; t2 " ->
let (A p , A s ) = candidateA t1 a in
∀a j ∈ A p , let (A p j , A s j ) = candidateA t2 a j in
∪
∪
( j A p j, As ∪ j As j)
| "t′ ; [t1 | t2 | . . . |tn ]" ->
let (A p , A s ) = candidateA t′ a in
(ϕ, A p ∪ A s )
| "try t′ " ->
let (A p , A s ) = candidateA t′ a in
if A s <> ϕ then ({a}, ϕ)
else (A p , ϕ)
| "repeat t′ " ->
let (A p , A s ) = candidateA t′ a in
if A s <> ϕ then ({a}, ϕ)
else
∀a j ∈ A p , let (A p j , A s j ) = candidateA t a j in
∪
∪
( j A p j ∪ i A si , ϕ)
図 4.2: 追加サブゴールに対して与えられた戦略を実行する処理。
最後に、candidate が再帰呼び出しを終了しトップレベルへ返すと、ECoq は
A p と A s を追加サブゴールとして保存し、O の中にある基本サブゴールの処理を
続ける。定理の証明が終わると、O の中身は空であるはずであり4 、残った追加サ
ブゴールの修正を求める。
ここでは、例題として Aexp に Amult だけでなく、単項の負号を表す Aneg を追
加した状態で、Aopt keep result の証明を試みる。なお、この場合の能動的修正
は以下のように宣言する。
Extend Inductive Aexp : Set :=
| Amult : Aexp ->Aexp ->Aexp
| Aneg : Aexp ->Aexp.
また、Aeval や Aopt は適切に拡張されたとする。Aopt の Aneg に対する適用は、
4
そうでなければ何か処理が誤っており、エラーである。
4.3. 証明の補完
59
以下のように振る舞う。
• 引数の項を最適化した結果が定数 Aval z であれば、Aval (-z) を結果とし
て返す。
• 最適化した結果が負号から始まる式 Aneg a であれば、a を結果として返す。
• それ以外の式となった場合は、結果の式に負号を付けて返す。
このとき、Aopt keep result の証明（図 2.6 を参照）を candidate によって試
みると、以下のようになる。
1. induction a により、5 つのサブゴールが生成される。それぞれ a が定数、
変数、加算、乗算、負号の場合である。後二者は追加サブゴールであるため、
処理を一旦止める。
2. 定数、変数、加算の場合のそれぞれに対し、intuition 戦略を実行する。こ
れにより、定数と変数の場合が証明され、加算のみが残る。
3. 加算に対して証明が続行される。simpl 戦略や rewrite 戦略が実行された
後、case 戦略によって式の場合分けが行われる。
4. 場合分けのうち定数と変数と加算の場合について続行し、再度 case 戦略で
場合分けが行われる。
5. 場合分けのうち定数と変数と加算の場合について auto 戦略が実行される。
これらのサブゴールは全て証明される5 。
6. 4 で行われた場合分けのうち、乗算と負号について（candidateA として）
auto 戦略が実行される。これらのサブゴールも証明される。
7. 3 で行われた場合分けのうち、乗算と負号について（candidateA として）
case 戦略によって場合分けが行われる。
8. エラーは起こらないので続いて auto 戦略が実行される。結果として全ての
場合が証明される。
9. 1 で生成された追加サブゴールに対して残りの戦略を実行する。intuition
ではゴールの整形が行われるが証明はされない。続く simpl 戦略でも同様で
ある。
5
加算の場合に「両辺の最適化結果が定数の場合以外はそのまま加算を返す」という証明。3 と
4 の場合分けが全て定数であれば定数に置き換えられた結果になる。
60
第4章
記述の再利用
10. 続く rewrite 戦略では、乗算のサブゴールでは IHa1 が存在するが、負号の
サブゴールでは存在しない。その結果負号のサブゴールではエラーが発生す
るため、このサブゴールに関してはここで戦略の続行を打ち切る（A s へと
移す）。
11. 乗算のサブゴールについては加算の場合と同様に実行され、全てのサブゴー
ルが証明される。
この結果、candidate によって負号の場合の証明が残される。ECoq はこの証明を
プログラマに要求することで、全体の証明を構築する。
このように、3.6 節において挙げた検出数より非常に少ない 1 箇所だけがプログ
ラマの証明すべきサブゴールとなる。この手法の提案は証明すべきサブゴールの
削減を目的としていたが、もう一点重要な観点があり、それはサブゴールの内容
である。
candidate による戦略の実行は原則として与えられた戦略が生成しうるサブゴー
ルのみがプログラマに提示される。4.1 節で提示した inversion によって生成さ
れた項は奇妙な形をしているため、プログラマにはその箇所の補完が難しい。一
方、candidate によって生成されるサブゴールは inversion を実行した結果につ
いてのみであり、このように途中の式が出現することはない。したがって、この
処理によって要求される証明は通常の証明において要求される形とほぼ同じであ
ると言え、それは補完の難しさを本来の証明における難しさと同程度に抑えるこ
とにつながる。
この処理は大半の証明においてうまくいくが、特殊な場合において処理の過程
で異なる証明の流れになってしまう場合がある。例えば try constructor という
戦略について考える。これは与えられたゴールが帰納型である場合にその帰納型
のコンストラクタを順に適用し、うまくいった場合その結果を返し、全て適用でき
なければ何もしない、という戦略になる。拡張前のプログラムではこの戦略の適
用によって何も起こらない場合でも、拡張した結果基本サブゴールがこの戦略に
対して追加したコンストラクタを適用してしまう可能性がある（例えばパラメー
タが追加したコンストラクタのパラメータと合致した場合）。残りの証明はこの戦
略で何も起こっていないことを期待して記述されているため、全体としては証明
に失敗することが予想される。
この問題を回避するために、ECoq は candidate がトップレベルに値を返した時
点で（未証明の部分が不足した）証明の項を調べ、拡張前の証明の項と比較する。
もし追加したコンストラクタの文脈を除いて一致する場合は証明の流れが変わっ
ていないと考え、以降の証明を続行する。しかし、これが一致しない場合、ECoq
は証明の候補を探すことを諦め、第 3 章で導入した手法によって全ての修正候補の
4.3. 証明の補完
61
記述を求める。これは candidate がエラーを返した場合や、証明の記述が終わっ
たにも関わらず基本サブゴールが残っている場合も同様である。なお、上に挙げ
た戦略は作為的な例であり、このような例は調べた限り発生していないため、現
実的にはほとんど問題がないと考える。
63
第 5 章 拡張のモジュール化
プログラムの拡張は必ずしも一人で行うものではない。共通の元プログラムに
対し、複数の拡張を行うことは頻繁に行われる。一方で、このときに複数の拡張
を合成し、全体として大きなプログラムを作ることは簡単ではない。
本章では、複数の拡張を適用する際に発生する問題を分析し、先に挙げた手法
によって作成した拡張を一つの機能を実現するモジュールとして扱うことで、複
数の拡張を統合する方法について述べる。このモジュールは、独立した処理を可
能な関数やクラスなどのモジュールと異なり、単一での処理を想定しておらず、ま
た対象とするプログラムも限定している。本章で定義する拡張モジュールは機能
指向プログラミングにおける機能（feature）やアスペクト指向プログラミングに
おけるアスペクトなどのモジュールに近い概念である。
5.1 拡張の衝突
第 3 章で定義した対話的修正は、拡張するパターンマッチの位置を対話的修正
機構との対話の順序によって決定していた。その結果、対話に用いた記述単体で
は、どの部分でどのパターンマッチを修正しているのかが判定できない。これは、
対象とするプログラムに別の修正を施した後にこの記述を適用することができな
いことを意味する。
例として、Amult の拡張によって Aopt の拡張を行った後の構成を考える。拡張
前の Aopt の中には（pCIC の観点からは）3 つのパターンマッチが存在した。一
方、拡張後の Aopt の中には 5 つのパターンマッチが存在する。このとき、Aexp に
異なるコンストラクタを追加したとすると、この 5 つのパターンマッチが全て修
正箇所として検出される。しかし、Amult の拡張前では、3 箇所のみが検出される
はずである。
このように、互いが互いに依存しない独立した二つの拡張を考慮すると、適用
の順序により検出箇所の増減が発生し、結果として拡張を扱うことができないこ
とがわかる。この検出箇所の増減は本質的にそれぞれの拡張で考慮していないこ
とであり、二つの拡張を同時に考えて初めて発生する。これは二つ以上の拡張を
第5章
64
拡張のモジュール化
同時に考慮すると、その結果として修正しなければならない箇所が発生すること
を意味する。
二つ以上の重なりにより新たな修正が必要なことは不可避だが、ここで問題と
なるのは、第 3 章の記述ではこのような修正箇所を限定することができないこと
である。したがって、本章ではまずそれぞれの修正と修正箇所を結びつける構造
を定義し、第 3 章で定義した対話的修正によってその構造を作成することを考え
る。その後、複数の拡張に対する構造を合成し、一つの拡張として取り扱う手法
を考える。
5.2 拡張モジュール
第 3 章において定義した処理では、拡張するパターンマッチの位置と対応する
項の記述がない点が問題となる。本節では、拡張箇所を明示するために、処理の
順序のみで規定されていたものを項として記述し、それらの間の合成関係を定義
する。
処理において追加しているものは、帰納型のコンストラクタ、パターンマッチの
パターン、そして帰納原理関数の引数である。ここでは、議論の単純化のために、
帰納原理関数については考えないものとする。なお、帰納原理関数の処理は、コ
ンストラクタの順序にしたがって適用する要素を追加するだけである。
以上から、拡張を表現する要素の定義は図 5.1 のようになる。直感的には、pCIC
の定義に対して、変数などを残したまま構造の一部分のパターンマッチにパター
ンを追記するものとなっている。追記されているパターンやコンストラクタは、+|
を用いて表現されている。なお、このモジュールの仮定として以下のものを想定
する。
• 全ての MD の宣言は同名、同種の宣言が Edef に含まれる。
• 要素の定義順序は元となるプログラム Edef の順序に従うものとする。
• モジュールでは全ての妥当な拡張を行っている。
これらが満たされない場合は合成においてエラーを出力する。
以降では、MT に属する要素を拡張項、MI に属する要素を拡張型宣言、M に属
する要素を拡張モジュールと呼ぶ。3.1 節の拡張を例とすると、拡張型宣言に
:= +| Amult : Aexp->Aexp->Aexp が存在し、また Aeval の拡張項
Aexp :
の一部に match with +| Amult a1 a2 => Aeval a1 e * Aeval a2 e end が
存在する。
5.3. 対話による拡張モジュールの作成
MT ::=
|
|
|
|
|
(MT MT)
fun x : MT => MT
∀x : MT, MT
let x := MT in MT
match MT return MT with
( | C x∗ => MT )∗
( +| C x∗ => T )∗ end
MI ::= I (x : MT)∗ : MT := ( | C (x : MT)∗ : MT )∗
( +| C (x : MT)∗ : MT )∗
MD ::= c : MT | c : MT := MT | MI
M
::= ·
|
MD; M
65
(拡張非依存な項)
(関数適用の拡張)
(関数抽象の拡張)
(全称限量の拡張)
(let 式内部の拡張)
(パターンマッチの拡張)
(パターンの追加)
(既存の帰納型の拡張)
(追加のコンストラクタ)
(宣言の拡張)
(終端)
(拡張記述)
図 5.1: 拡張モジュールの定義。
次にこの拡張モジュールとプログラムの合成について図 5.2 として定義する。こ
の処理は、拡張前の項や型宣言と拡張項や拡張型宣言を構造比較し、拡張部分に
項を挿入する操作である。これは単一の拡張モジュールに対してのみの処理となっ
ている。複数の拡張モジュールに関しては 5.4 節にて扱う。
なお、merge 処理によってプログラムと拡張モジュールを合成した場合、合成
結果であるプログラムは型がつくとは限らない。これは例えば型の拡張のみを記
述した拡張モジュールを合成することで、網羅性検査によってエラーが発生する
項が作成されることから容易にわかる。そのため、拡張モジュールをプログラマ
が自由に書くことは想定しておらず、次節にて説明する対話的修正による作成の
みを想定している。
5.3 対話による拡張モジュールの作成
前節では拡張モジュールの構造と、プログラムとの合成処理について定義した。
本節では、3.1 節で記述した処理にしたがって拡張モジュールを作る過程を定義す
る。これは図 3.2 における処理を、項を返さずに拡張項を返す形にした処理に相当
する。
項に関する拡張記述の作成は図 5.5 に定義した extM が、環境全体に関する拡張
モジュールの作成は図 5.4 に定義した extM がそれぞれ行う。それぞれの処理の手
第5章
66
拡張のモジュール化
let rec merge E M :=
match E with
| "·" -> "·"
| "c : T 1 ; E ′ " ->
match M with
| "c : T 1′ ; M ′ " -> "c : ( mergeT T 1 T 1′ ); (merge E ′ M ′ )"
| _ -> "c : T 1 ; (merge E ′ M)" ( ∗ n o t h i n g t o do f o r c ∗ )
| "c : T 1 := T 2 ; E ′ " ->
match M with
| "c : T 1′ := T 2′ ; M ′ " -> "c : ( mergeT T 1 T 1′ ) := ( mergeT T 2 T 2′ ); (
merge E ′ M)"
| _ -> "c : T 1 := T 2 ; (merge E ′ M)" ( ∗ n o t h i n g t o do f o r c ∗ )
| "I (x1 : T 01 ) . . . (x0n : T 0n ) : T :=
| C1 (x11 : T 11 ) . . . (x1m1 : T 1m1 ) : T 1
| ...
| Cl (xl1 : T l1 ) . . . (xlml : T lml ) : T l as Ind; E ′ " ->
match M with
| "I (x1 : MT 01 ) . . . (x0n : MT 0n ) : MT :=
| Ci (xi1 : MT i1 ) . . . (ximi : MT imi ) : MT i
| ...
| C j (x j1 : MT j1 ) . . . (x jm j : MT jm j ) : MT j
′ : T ′ ) . . . (x′
′
′
(+| C1′ (x11
11
1m1 : T 1m1 ) : T 1 )
(+| . . .)
′ : T ′ ) . . . (x′ : T ′ ) : T ′ ); M ′ " ->
(+| Cl′ (xl1
l1
lml
lml
l
let T ′′ = mergeT T MT in
∀i, let T i′′ = if MT i exists then mergeT T i MT i else T i in
∀i, j, let T i′′j = if MT i j exists then mergeT T i j MT i j else
T i j in
′′ ) . . . (x
′′
′′
"I (x1 : T 01
0n : T 0n ) : T :=
′′ ) . . . (x
′′
′′
| C1 (x11 : T 11
1m1 : T 1m1 ) : T 1
| ...
′′ ) : T ′′
| Cl (xl1 : T l1′′ ) . . . (xlml : T lm
l
l
′
′ ) : T′
′
′
′
| C1 (x11 : T 11 ) . . . (x1m′ : T 1m
′
1
1
1
| ...
′ ) : T ′ ; (merge E ′ M ′ )"
| Cl′′ (xl′′ 1 : T l′′ 1 ) . . . (xl′′ m′ : T lm
′
l′
l′
| _ -> "Ind; ( merge E ′ M ′ )"
l′
図 5.2: 環境に対する拡張モジュールの合成。
5.3. 対話による拡張モジュールの作成
67
let rec mergeT T MT :=
match MT with
| "_" -> T
| "(MT 1 MT 2 )" ->
match T with
| "(T 1 T 2 )" -> "((mergeT T 1 MT 1 ) (mergeT T 2 MT 2 ))"
| _ -> abort ( ∗ MT i s n o t k e e p i n g T ’ s s t r u c t u r e ∗ )
| "fun x : MT 1 => MT 2 " ->
match T with
| "fun x : T 1 => T 2 " -> "fun x : (mergeT T 1 MT 1 ) => (mergeT T 2 MT 2 )"
| _ -> abort
| "∀x : MT 1 , MT 2 " ->
match T with
| "∀x : T 1 , T 2 " -> "∀x : (mergeT T 1 MT 1 ), (mergeT T 2 MT 2 )"
| _ -> abort
| "let x := MT 1 in MT 2 " ->
match T with
| "let x := T 1 in T 2 " -> "let x := (mergeT T 1 MT 1 ) in (mergeT T 2 MT 2 )"
| _ -> abort
| "match MT ′ return MT r with Ptni => MT 1 | . . . | Ptn j => MT j
+| Ptn′1 => T 1′ +| . . . +| Ptn′m => T m′ end" ->
match T with
| "match T ′ return T r with Ptn1 => T 1 | . . . | Ptnn => T n end" ->
let T ′′ = (mergeT T ′ MT ′ ) in
let T r′ = (mergeT T r MT ′r ) in
∀i ∈ {1..n}, let T i′′ = if MT i exists then (mergeT T i MT i ) else
T i in
"match T ′′ return T r′ with
Ptn1 => T 1′′ | . . . | Ptnn => T n′′
| Ptn′1 => T 1′ | . . . | Ptn′m => T m′ end"
| _ -> abort
図 5.3: 項に対する拡張の合成。
68
第5章
拡張のモジュール化
let rec extMT T =
match T with
| "Set" | "Prop" | "Type" | "x" | "C" | "I" -> "_"
| "(T 1 T 2 )" -> "((extMT T 1 ) (extMT T 2 ))"
| "fun x : T 1 => T 2 " -> "fun x : (extMT T 1 ) => (extMT T 2 )"
| "∀x : T 1 , T 2 " -> "∀x : (extMT T 1 ), (extMT T 2 )"
| "let x := T 1 in T 2 " -> "let x := (extMT T 1 ) in (extMT T 2 )"
| "match T ′ return T r with Ptn1 => T 1 | . . . | Ptnn => T n end"
-> let T ′′ = (extMT T ′ ) in
let T r′ = (extMT T r ) in
∀i ∈ {1..n}, let T i′ = (extMT T i ) in
let I ′ = typeof T ′ in
if I ′ ∈ Eext then
begin
∀C j : I ′ ∈ Eext ,
let Ptn′j = pattern _for_ constructor C j in
let B j = request _term_of_type T r′ in
"match T ′′ return T r′ with
Ptn1 => T 1′ | . . . | Ptnn => T n′
| Ptn′1 => B1 | . . . | Ptn′m => Bm end"
end
else
"match T ′′ return T r′ with Ptn1 => T 1′ | . . . | Ptnn => T n′ end"
図 5.4: 項の拡張部分の作成。
順は 3.1 節と同様である。
extMT や extM を用いることで、直接拡張したプログラムを得るのではなく、拡
張モジュールを得ることができる。しかし、これにより得た拡張モジュールをプ
ログラムと合成すると元の拡張と同一となることを証明する必要がある。
定理 3. 同一の拡張順序で行われる対話的修正に対して、項 T に対し、ext T =
mergeT T (extMT T ) が成立する。また、同様の仮定下で、環境 E に対し、extE E =
merge (extM E) が成立する。
証明. 項 T や環境 E に関する帰納法を用いる。extMT により作った拡張項は引数であ
る項の構造を写している。そのため、部分項に関しては帰納法の仮定から merge の
結果と ext の結果が一致する。また、対話的に拡張する箇所は同一であるため、合成
結果は対話的拡張と同じ項を構成する。したがって、ext T = mergeT T (extMT T )
の成立が示される。帰納法の仮定と項に関する性質により、拡張モジュールにつ
いても同様に等価となることが示される。
□
5.4. 複数のモジュールの合成
69
let rec extM Edef =
match Edef with
| "·" -> "·"
′ " -> "x : (extMT T ); (extM E ′ )"
| "x : T ; Edef
def
′ " -> "x := (extMT T ) : (extMT T ); (extM E ′ )"
| "x := T 1 : T 2 ; Edef
1
2
def
| "I (x1 : T 01 ) . . . (x0n : T 0n ) : T :=
| C1 (x11 : T 11 ) . . . (x1m1 : T 1m1 ) : T 1
| ...
′ " ->
| Cl (xl1 : T l1 ) . . . (xlml : T lml ) : T l ; Edef
∀i ∈ {1..n}, j ∈ {1..l}, k j ∈ {1..m j },
let MT ′0i = extMT T 0i in
let MT ′jkk = extMT T jkk in
let MT ′j = extMT T j in
if I ∈ Eext then
let C E is a list of constructor of I in Eext in
′ ) . . . (x
′
"I (x1 : T 01
0n : T 0n ) : ( extMT T ) :=
| C1 (x11 : MT ′11 ) . . . (x1m1 : MT ′1m1 ) : MT ′1
| ...
| Cl (xl1 : MT ′l1 ) . . . (xlml : MT ′lml ) : MT ′l
′ "
+| C E ; Edef
else
"I (x1 : MT ′01 ) . . . (x0n : MT ′0n ) : ( extMT T ) :=
| C1 (x11 : MT ′11 ) . . . (x1m1 : MT ′1m1 ) : MT ′1
| ...
′ "
| Cl (xl1 : MT ′l1 ) . . . (xlml : MT ′lml ) : MT ′l ; Edef
図 5.5: 拡張モジュールの作成。
以上により、正確な拡張モジュールを対話的に作成することが可能となった。拡
張モジュールは明確に修正箇所を保持しているため、複数の拡張が混在した場合
でも修正が可能である。
5.4 複数のモジュールの合成
ここでは、複数の拡張モジュールを合成し、一つの拡張モジュールとして取り
扱う手法を提案する。なお、以下の手法では、二つの拡張モジュールについての
み議論し、それぞれの対象とするプログラムは同一であるとする。
基本的に複数の拡張モジュールを合成した場合に問題となるのは、それぞれが
拡張した結果新しいパターンが必要になる場合である。これは、追加するパター
70
第5章
拡張のモジュール化
ンの本体でさらにパターンマッチを行っている場合に発生しうる。このことは、拡
張モジュールから見える範囲について分析すると明らかである。
ある環境 E に対する二つの拡張モジュール M1 、M2 について考える。M1 が影響
を調べた範囲は E の内部と M1 自身である。 したがって、M1 がこれら全体のうち、
影響を調べ切れていない箇所は M2 の内部のみである。これは M2 についても同様
である。
この分析から、互いが互いの内部について拡張を行うことで、重なりによる影
響を排除することができる。これは、 M1 が拡張する型の環境を Eext1 、 M2 が拡張
する型の環境を Eext2 としたときに、 M1 に対して extE に相当する操作を、拡張す
る型の環境 Eext2 の下で行い、また M2 に対しては拡張する型の環境を Eext1 の下で
行うことに他ならない。例えば、Amult を追加する拡張と Aneg を追加する拡張で
は、それぞれ Aopt において追加するパターンの内部でパターンマッチをしている
ため、これが検出対象となり、修正が行われる。
互いの拡張後は、merge 相当の処理を行うことで一つの拡張モジュールにする
ことができる。このモジュールは M1 と M2 の拡張をどちらも含んでいるため、環
境 E に適用することで二つの拡張を順次（適切にパターンを補いながら）適用し
たときと同様の効果になる。このモジュールを合成した結果型がつくことの証明
は将来課題とし、ここでは合成後の項を型検査することで安全性を確保する。
71
第 6 章 関連研究
6.1 関数型言語
2.3 節で挙げていない Expression problem の解法として、ここでは Milstein らの
EML[26] を挙げる。これは ML にオブジェクト指向言語におけるクラスを導入し
た言語である。既に述べたとおり、オブジェクト指向言語では操作の追加が問題と
なる。そのため、EML では通常の関数型言語におけるパターンマッチと同様にし
て処理を行うようにしている。この場合に問題となるのは、パターンマッチによ
る分岐を固定させてしまう可能性だが、これは open data type と同様により具体的
な（つまり継承関係が一番近い）ものから選ぶことで回避している。また、open
data type と異なり、関数の拡張対象はトップレベルである必要がない、という利
点もある。一方で、この場合の関数の網羅性を確保するには、デフォルトケース
が必要となっている。これは変数を用いたパターンそのものであり、したがって
やはり網羅性の問題が同様に残っている。
2.3 節において、Expression problem の解法の一つとして型クラスを挙げた。Coq
ではバージョン 8.2 より型クラスが利用可能 [34] であるが、証明の場合分けを用
いることができないという欠点を持つ。また、実装の問題として関数の追加時に
多くの冗長な記述が必要な点が挙げられる。以下が Coq における Type class を利
用した Expression problem の記述である。なお、簡単化のために式は定数と加算、
処理は評価関数に加えて簡単な命令列にコンパイルする操作にした。
Class Exp := { E :> Exp ; Eval : nat }.
Instance EConst (n : nat) : Exp := { Eval := n }.
Instance EAdd (e1 e2 : Exp) : Exp :=
{ Eval := let (n1) := e1 in let (n2) := e2 in n2 + n1 }.
Class CompExp := { E :> Exp ; Compile : list Word }.
Instance CEConst n : CompExp :=
{ E := EConst n ; Compile := WPush n :: nil }.
Haskell の type class では、新しいクラスを宣言し、その関数を記述するだけで解
決できたが、Coq では次の点が冗長になっている。
第 6 章 関連研究
72
• クラスの宣言は他のインスタンスを自動でインポートすることはできない。
したがって、新しいクラスのインスタンスは自分で基となっているインスタ
ンスを指定しなければならない。
• 関数は常にレコードの中にある。レコードの拡張はクラスを追加することで
しかできない。
また、Haskell と同様の問題として拡張したクラスにおけるインスタンスの網羅性
が確認できないという問題がある。今回の例では、加算に関するコンパイル操作
を実現していないが、エラーは発生しない。
6.2 機能指向プログラミング
オブジェクト指向における Expression problem は 2.3.1 節にて述べたとおり、操
作の追加に弱いという側面が現れる。これは、操作の分散によるものであり、ク
ラスが後から拡張できないため解決は難しい。
操作を別途追加する技術としてはトレイトや mixin が挙げられる。トレイトや
mixin は実装付きインターフェースと考えることができ、単一継承を保ったまま比
較的自由にモジュールに付けることが可能である。一方で、Expression problem に
おける各クラスは異なる処理をしているため、それぞれのクラスに付けるトレイ
トを切り替える必要がある。
機能指向プログラミング（Feature-oriented Programming）は、機能という単位で
複数の拡張単位をモジュール化する手法である [31]。機能指向プログラミングで
は、各機能を実装する機能モジュールと、それを連結する記述に分かれている。し
たがって、Expression problem の解法は比較的単純である。各要素の各処理を実装
する機能モジュールを記述し、それらを組み合わせて一つのデータ型を表現する
のみでよい。
mixin やトレイトと異なり、優先順位などは順序ではなく連結を決定する記述に
よって決定される。機能指向の型システムは比較的モジュラーであり、連結を行う
前にある程度の型検査が可能である。型検査については機能指向を Featherweight
Java[18] に導入した FFJ などで議論されている [1]。
機能指向に基づいて Coq で記述したプログラムを拡張可能にする手法として、
Delaware らが提案した、Core Featherweight Java（以下 CFJ）[11] の記述における
手法が挙げられる [13]。CFJ は、Coq によって記述された Featherweight Java から
キャストを除いたサブセットである。この中で使用されている手法は、型の拡張
が可能な箇所をモジュール中でパラメータとして宣言することにより、複数の拡
張を結合し、また任意の他のモジュールを取り込むことができる。彼らはこのモ
6.3. アスペクト指向
73
ジュールを機能モジュール（feature modules）と呼んでおり、また複数のモジュー
ルを結合する記述が存在する意味で、この手法は機能指向に基づいているといえ
る。公開しているプログラムでは、CFJ にキャストを追加するモジュール、イン
ターフェースを追加するモジュール、ジェネリクスを追加するモジュール、など
が用意されている。
この手法の対話的修正機構に対する優位な点として、新しい処理系が必要なく、
通常の Coq を用いることができる点が挙げられる。これは記述にセクション機能、
パラメータなどの Coq に既に存在する要素のみで構成されていることによる。一
方、この手法における問題点は主に以下の三点である。
1. プログラマは拡張可能な箇所を全てパラメータ化しなければならない。
2. 証明は直接帰納法を用いることができない。パラメータ化した帰納原理関数
を自身で作成し、またそれを適切に適用しなければならない。
3. 期待される挙動をパラメータとして要求する必要がある。このパラメータの
指標はほとんどない。これらは通常簡易な定理に過ぎないものばかりである。
これらは対話的修正機構の思想と明らかに異なる点である。この手法におけるプ
ログラマの負担は非常に大きいため、本研究の手法がより汎用に用いることがで
きると考える。
6.3 アスペクト指向
アスペクト指向は、横断的関心事をモジュール化することを主として作られた
手法である。ここでは最も広く用いられているポイントカット・アドバイスモデ
ルに基づく言語に対してのみ言及する。
ポイントカット・アドバイスモデル [20] では、アスペクトモジュールの中に変
更したい箇所を記述したポイントカットと、変更する内容を記述したアドバイス
を記述する。対話的修正機構において、ポイントカットとアドバイスは第 5 章で
導入した拡張モジュールにおける項の拡張部分に対応する。また、拡張モジュー
ル自身はアスペクトモジュールとして考えられる。
このようなプログラムの拡張を目的としてアスペクトを利用したコンパイラフ
レームワークとして、JastAdd[17] がある。JastAdd では言語の拡張や静的検査など
のコンパイラの機能拡張をアスペクトとしてモジュール化し、組み合わせて使用
することを想定している。例えば Java のコンパイラとして JastAddJ[14] が実装さ
れているが、Java1.4 のパーサをメインにし、コンパイルの機能をアスペクトとし
て作成している。また、別のアスペクトとして Java1.4 のパーサを拡張し、Java5.0
第 6 章 関連研究
74
の構文に対応させたパーサを作るモジュールを提供している。これら二つを組み
合わせると、新しい構文をパースしてもコンパイルできない状態になってしまう。
この状態は、新しいアスペクトとして Java5.0 の構文をコンパイルするアスペクト
を作成し、組み合わせることで解決できる。本研究における拡張モジュールの組
み合わせについては JastAdd から着想を得ている。
特に本研究と似た立ち位置の言語として Aspectual Caml[25] がある。Aspectual
Caml は OCaml に対してアスペクト指向の概念を取り入れた言語であり、次の機
能を持つ。
• アドバイスの挿入。ポイントカットは多相性もサポートしている。
• データ型の拡張。本研究と同様、コンストラクタをデータ型に追加すること
ができる。
• 関数の引数の追加。任意の関数に引数を追加することができる。
Aspectual Caml でのデータ型の拡張は、対話的修正機構と同様の機能である。一
方、この場合のパターンマッチにおけるパターンの追加は、アドバイスとしてプロ
グラマが記述する必要がある。また、パターンが不足する場合の問題は基本的には
コンパイラの網羅性検査に依っている。これは 2.2 節にて挙げたワイルドカードパ
ターンや変数を用いたパターンによる問題が発生することを示している。Aspectual
Caml におけるデータ構造は代数的データ構造であるため、ワイルドカードパター
ンの使用を抑制することで、ある程度は回避が可能である。しかし、この回避は
確実ではないことは既に述べたとおりである。
対話的修正機構にない機能として、Aspectual Caml では関数の引数を追加でき
る。これは OCaml のデフォルト引数を用いることで、既存の関数呼び出しの見か
けの型を変更することなく対応している。この方式を参考に引数の追加を対話的
修正機構に取り込むことは十分に検討の価値がある。
6.4 Coq の検証手法
対話的修正機構の利点は、Coq におけるプログラムを直接拡張できる点にある。
しかし、第 3 章では複数の制約を導入したため、Coq において提案された検証手
法や機能との併用が可能かを考える必要がある。ここでは、プログラミング言語
に関係する検証手法や、Coq における記述の拡張について考察する。
プログラミング言語に関する検証手法としては、対象言語における変数束縛に
関するものがある。Coq において変数束縛を扱う手法としては、locally nameless
representation[4] や parametric higher-order abstract syntax（PHOAS）[6] が代表的で
6.4. Coq の検証手法
75
ある。Locally nameless representation では、変数の生成に cofinite quantification と
いう手法を用いることで、変数の一致や重複を防ぐことが可能になる。これはラ
イブラリとして提供されているため [23]、容易に使用することができる。対話的
修正機構は拡張する帰納型に対する制約しかもたないため、この手法と併用する
ことは全く問題ない。一方、PHOAS では、束縛を帰納型に行わせている。本来
の higher-order abstract syntax[29] における記述では、帰納型の制約の一つである
positivity condition に抵触してしまう。PHOAS では帰納型における束縛を行う関
数の型をパラメタライズすることでこの問題を回避している。対話的修正機構の
制約は、帰納型に関するソート多相、allowed elimination sort、そして帰納原理関
数の三つに関するものであり、PHOAS で用いている手法とは干渉しない。
また、Coq のコマンドとは異なる文法を用いる機能として SSreflect[16]、Russel、
Equations[33] が挙げられる。SSreflect は定義や関数の記述などより証明記述やラ
イブラリに重点を置いている。証明記述は通常の Ltac や戦略とはやや異なる記述
をするため、過剰に用いた場合第 4 章にて述べた証明の再利用が頻繁に失敗する
可能性がある。
Russel は Coq に組み込まれた Program コマンドに関わるシステムである。Program
コマンドでは、制限された再帰関数などではなく通常の関数型言語における自由
な記述が可能となっている。Russel はその記述に対して述語の埋め込みを行い、停
止性の自動証明を試み、証明できなかったゴールについてプログラマに証明を要求
する。この停止性の証明によって Coq における関数として利用できるようになる。
また、Equations はパターンマッチを match 式を用いずに Haskell のように関数
のトップレベルで行うことを目的としたシステムである。このパターンマッチで
は依存型の解決に力を入れており、通常の Coq におけるパターンマッチ以上に柔
軟な記述が可能となっている。また、Equations を利用して記述した関数も、最終
的には通常の Coq における関数として扱われる。
対話的修正機構の特性上、関数の拡張は文脈の表示によってサポートされてい
る。しかし、Russel では再帰呼び出しやパターンマッチに述語の埋め込みを行い、
また Equations ではトップレベルでのパターンマッチを通常のパターンマッチに変
換している。そのため、文脈として表示されるものは Russel や Equations を利用し
て記述した関数とは大きく異なっている。多くの場合では、これらの機能が対話
的修正機構の制限に抵触することはないが、修正を考えたときには決して使いや
すいとは言えない。この問題に対応するには、記述したプログラムと内部の関数
との対応を取り、また記述に使用したシステムに依存した表記をする必要がある。
このような対応は一般的には不可能であり、また個別の対応もシステムを複雑化
していくため、この問題は解決できない考える。したがって、これらの機能と対
話的修正機構の併用はやや難しいといえる。
77
第 7 章 結論
7.1 まとめ
Expression problem を対象とした研究は非常に広く行われているが、これらは記
述の柔軟性に特化したものが多い。したがって、プログラマが適切に記述すれば
プログラムの拡張ができるものの、記述する場所を調べる方法はほとんど提案さ
れておらず、ほとんどが関数型言語におけるパターンマッチの網羅性のように、既
存の手法に依存している。しかしこの手法ではいくつかの見落としが発生してし
まう。
本論文で提案した対話的修正機構では、拡張可能な範囲をコンストラクタの追
加に制限することで、拡張の起点はプログラマが知る必要はあるものの、それに
関連する箇所を網羅的に検出することができた。実際に検出されるのは以下の二
点である。
• コンストラクタを追加した型を展開しているパターンマッチ。新たに追加さ
れたコンストラクタに関するパターンが不足している。
• 他の帰納型のうち、型のパラメータとして拡張した型を持ち、さらにコンス
トラクタが出現しているもの。追加されたコンストラクタに関する拡張が必
要な場合がある。
特に後者は網羅性検査が不可能であるため、非常に有効であるといえる。
しかし、この手法では証明も関数と同様に扱うことで統一的な手法とした代わ
りに、過剰な検出が多数行われることになった。そこで、拡張前に行った証明の
記述から、過剰な検出を行っている箇所に埋め込む修正候補を生成し、自動で処
理を行う手法について提案した。その結果拡張後のプログラムにはそのまま適用
できない証明を再利用し、過剰な検出が行われないようなった。
最後にこうして作った拡張をモジュールとすることで、取り外しが容易になり、
また異なる二つの拡張の合成も可能となった。このとき、二つの拡張の重なりから
さらに拡張が必要となる場合があるため、これをさらに対話的修正を行うことで
解決した。行われた対話的修正は、二つの拡張モジュールを接続する拡張モジュー
ルとなる。
第7章
78
結論
以上の手法により、プログラムの拡張および拡張の合成が可能となった。この
ことは、プログラムの重要な機能についてのみ検証をした後に、段階的にプログ
ラムに機能を追加し、再検証を行うことができることを示している。このことか
ら、本論文で提案した対話的修正は大規模なソフトウェア開発において問題とな
る保守性の低下や拡張性の低下を解決することのできる手法といえる。
7.2 残された課題
本論文で提案した対話的修正機構は、汎用性と拡張の健全性に特化したもので
ある。したがって、次の二つの方向に進めることができる。
1. 拡張の種類の拡大。汎用性を保ったまま、拡張がアドホックに適用されるこ
とを許すことでより多くの拡張が可能になる。
2. 手法の特化。言語処理系に特化した命令を導入することで、プログラマに
とって拡張が容易になる。
前者の例としては、関数へのパラメータの追加、関数の置き換えがある。関数
へのパラメータの追加は、帰納原理関数に対して行った制約を適用することで導
入が可能となる。しかし、帰納原理関数と異なり、通常の関数は高階関数として
利用することがあるため、制約が強すぎると考えられる。この解決には Aspectual
Caml の用いていたデフォルト引数が有効と考えている。パラメータを追加する状
態ではないときに、デフォルト引数を使うことで見かけ上の型を不変にすること
ができる。今後、この手法に基づいた検出と、健全性について議論していきたい。
関数の置き換えは、ナイーブな実装で証明した後に高速な実装に切り替える、と
いう場合に利用できる。このとき、ナイーブな実装と高速な実装の間で等価性を
証明することで、全体の証明を実現できる。一方、置き換えの問題は、置き換え
た関数内のパターンマッチが修正対象になった場合に発生する。このとき、証明
はナイーブな実装に基づいたものとなるため、証明に修正対象となる箇所は出現
しない。したがって、再度等価性の証明を行うなどして整合性を取り直す必要が
ある。しかし、関数の置き換え時に他の拡張を許さないようにすれば、単純作業
に近い証明を自動化できる点で優れている。
手法の特化については、CompCert における意味論の変化がよい入り口となり
得る。CompCert では、初期は直感的な理解のしやすさと証明の容易さのために
big-step semantics を取っていたが、終了しないプログラムのために余帰納的な意
味論を用い、goto 文に対応するために small-step semantics を取っている。しかし、
別の意味論に変化した場合でも、既存の補題の証明はほぼ同じようになっている。
7.2. 残された課題
79
したがって、意味論の変化時に、追加する機能のみに関する証明を行い、元のプロ
グラムとの意味論の対応を取ることで全体を構築する、という流れも考えられる。
これはワークフローが非常に限定されているため、より詳細な分析を行い、設計
する必要がある。
81
参考文献
[1] Sven Apel, Christian Kästner, and Christian Lengauer. Feature featherweight java:
a calculus for feature-oriented programming and stepwise refinement. In Yannis
Smaragdakis and Jeremy G. Siek, editors, GPCE, pp. 101–112. ACM, 2008.
[2] Robert S. Arnold and Shawn A. Bohner. Impact analysis - towards a framework for
comparison. In Proceedings of the International Conference on Software Maintenance 1993, pp. 292–301. IEEE Computer Society Press, September 1993.
[3] L. Augustsson. Compiling pattern matching. In Functional Programming Languages and Computer Architecture, Vol. 201 of LNCS, pp. 368–381. Springer Verlag, 1985.
[4] Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and
Stephanie Weirich. Engineering formal metatheory. In ACM SIGPLAN-SIGACT
symposium on Principles of programming languages, pp. 3–15, 2008.
[5] Brian Campbell. An executable semantics for compcert C. In Chris Hawblitzel
and Dale Miller, editors, CPP, Vol. 7679 of Lecture Notes in Computer Science,
pp. 60–75. Springer, 2012.
[6] Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN international conference on Functional programming, pp. 143–156, 2008.
[7] The CompCert project. http://compcert.inria.fr/.
[8] The Coq proof assistant reference manual version8.4. http://coq.inria.fr/
distrib/current/files/Reference-Manual.pdf.
[9] Coqtail project. http://sourceforge.net/projects/coqtail/.
[10] Th. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, Vol. 76, pp. 96–120, 1988.
[11] core featherweight java + extensions. http://www.cs.utexas.edu/˜bendy/
MMMDevelopment.php.
[12] Darcs. http://darcs.net/.
[13] Benjamin Delaware, William Cook, and Don Batory. Product lines of theorems.
In Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications, OOPSLA ’11, pp. 595–608, New
York, NY, USA, 2011. ACM.
[14] Torbjörn Ekman and Görel Hedin. The JastAdd extensible Java compiler. In ACM
SIGPLAN conference on Object Oriented Programming Systems and applications,
pp. 1–18, 2007.
[15] Jacques Garrigue. Programming with polymorphic variants. In ACM SIGPLAN
Workshop on ML , informal proceedings, September 1998.
[16] Georges Gonthier and Assia Mahboubi. A small scale reflection extension for the
Coq system. Research Report 6455, Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France, 2008.
[17] Görel Hedin and Eva Magnusson. Jastadd - a java-based system for implementing
front ends. January 01 2001.
[18] Atsushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A
minimal core calculus for Java and GJ. TOPLAS, Vol. 23, No. 3, pp. 396–459,
May 2001.
[19] Isabelle home page.
[20] Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm, and
William G. Griswold. An overview of AspectJ. In J. Lindskov Knudsen, editor, ECOOP 2001 — Object-Oriented Programming 15th European Conference,
Vol. 2072 of Lecture Notes in Computer Science, pp. 327–353. Springer-Verlag,
Budapest, Hungary, June 2001.
[21] Gregor Kiczales, John Lamping, Anurag Menhdhekar, Chris Maeda, Cristina
Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented programming. In
11th European Conference on Object-Oriented Programming, Vol. 1241 of LNCS,
pp. 220–242, June 1997.
[22] Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, Vol. 43, No. 4, pp. 363–446, December 2009.
[23] LN : Locally nameless representation with cofinite quantification. http://www.
chargueraud.org/softs/ln/.
[24] Andres Löh and Ralf Hinze. Open data types and open functions. In ACM SIGPLAN international conference on Principles and practice of declarative programming, pp. 133–144, 2006.
[25] Hidehiko Masuhara, Hideaki Tatsuzawa, and Akinori Yonezawa. Aspectual Caml:
an aspect-oriented functional language. In ACM SIGPLAN International Conference on Functional Programming, pp. 320–330, 2005.
[26] Todd Millstein, Colin Bleckner, and Craig Chambers. Modular typechecking for
hierarchically extensible datatypes and functions. In Proceedings of the seventh
ACM SIGPLAN international conference on Functional programming, ICFP ’02,
pp. 110–122, New York, NY, USA, 2002. ACM.
[27] Ulf Norell. Towards a practical programming language based on dependent type
theory. PhD thesis, Chalmers University of Technology, 2007.
[28] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, Vol. 828 of Lecture
Notes in Computer Science. Springer-Verlag, 1994.
[29] F. Pfenning and C. Elliot. Higher-order abstract syntax. In ACM SIGPLAN conference on Programming Language Design and Implementation, pp. 199–208, 1988.
[30] Andy Podgurski and Lori A. Clarke. A formal model of program dependences and
its implications for software testing, debugging, and maintenance. IEEE Transactions on Software Engineering, Vol. 16, No. 9, pp. 965–979, September 1990.
[31] Christian Prehofer. Feature-oriented programming: A fresh look at objects. In
ECOOP, pp. 419–443, 1997.
[32] Jaroslav Sevcı́k, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan,
and Peter Sewell. Relaxed-memory concurrency and verified compilation. In
Thomas Ball and Mooly Sagiv, editors, POPL, pp. 43–54. ACM, 2011.
[33] Matthieu Sozeau. Equations: A dependent pattern-matching compiler. In Matt
Kaufmann and Lawrence C. Paulson, editors, ITP, Vol. 6172 of Lecture Notes in
Computer Science, pp. 419–434. Springer, 2010.
[34] Matthieu Sozeau and Nicolas Oury. First-class type classes. In 21st International
Conference Theorem Proving in Higher Order Logics, Vol. 5170 of LNCS, pp.
278–293, August 2008.
[35] Mads Torgersen. The expression problem revisited. In Proceedings of European
Conference on Object-Oriented Programming (ECOOP’04), Vol. 3086 of LNCS,
pp. 123–146. Springer Verlag, June 2004.
[36] P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th annual ACM SIGPLAN-SIGACT symposium on Principles of
programming languages, pp. 60–76. ACM Press, January 1989.
[37] Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic.
Formalizing the llvm intermediate representation for verified program transformations. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on
Principles of programming languages, POPL ’12, pp. 427–440, New York, NY,
USA, 2012. ACM.
85
謝辞
本研究を行うにあたり、日頃からの指導をくださった渡部卓雄准教授に深く感
謝いたします。また、様々な悩みにアドバイスをくださった権藤克彦教授、米崎直
樹教授、西崎真也准教授に心からのお礼を申し上げます。上の先生方に加え、審
査時に有用な意見をくださった佐伯元司教授に感謝します。
渡部研究室の学生、OB の皆様にはゼミなどでの意見をいただいたことに感謝し
ます。同じフロアの学生の方々と交流を持つことで私の視野が広がったと思って
います。ありがとうございます。また、出張などの事務作業をしていただいた、研
究室秘書の岸本歩美様に感謝します。
そして最後に、両親と兄、妹、祖父母、従兄弟、そしていつも私の作る資料を
彩ったるろ・ぽーだ氏（以下の絵）に感謝の念を捧げます。
87
付 録A
While 言語とその最適化器
コメントアウトしている部分は、本文中で記述した拡張を行うためのコードで
ある。
Require Import ZArith .
Require Import Bool.
Require Import Sumbool .
Variable Var : Set.
Axiom VarDec : forall v1 v2 : Var ,
{v1 = v2 }+{ v1 <> v2 }.
Variable VarEq : Var ->Var ->bool.
Axiom VarEqT : forall v : Var , VarEq v v = true.
Axiom VarEqF : forall v1 v2 : Var ,
v1 <> v2 -> VarEq v1 v2 = false .
Definition Val := Z.
Definition Env := Var ->Val.
Inductive Aexp : Set :=
| Aval : Val ->Aexp
| Avar : Var ->Aexp
| Aadd : Aexp ->Aexp ->Aexp
( ∗ | A m u l t : Aexp -> Aexp -> Aexp ∗ )
.
Inductive Bexp : Set :=
| Btrue : Bexp
| Bfalse : Bexp
| Bnot
: Bexp ->Bexp
| Band
: Bexp ->Bexp ->Bexp
| Beq
: Aexp ->Aexp ->Bexp
| Blt
: Aexp ->Aexp ->Bexp.
Inductive Stm : Set :=
| Sass
: Var ->Aexp ->Stm
| Sskip : Stm
| Sif
: Bexp ->Stm ->Stm ->Stm
付録A
88
While 言語とその最適化器
| Swhile : Bexp ->Stm ->Stm
| Scomp : Stm ->Stm ->Stm
( ∗ | S r e p e a t : Stm -> Bexp -> Stm ∗ )
.
Fixpoint Aeval (a : Aexp) (e : Env) { struct a} :=
match a with
| Aval z => z
| Avar v => e v
| Aadd a1 a2 => (( Aeval a1 e) + ( Aeval a2 e))%Z
( ∗ | A m u l t a1 a2 => ( ( A e v a l a1 e ) ∗ ( A e v a l a2 e ))%Z ∗ )
end.
Fixpoint Beval (b : Bexp) (e : Env) { struct b} :=
match b with
| Btrue => true
| Bfalse => false
| Bnot b’ => negb ( Beval b’ e)
| Band b1 b2 => andb ( Beval b1 e) ( Beval b2 e)
| Beq a1 a2 => Zeq_bool ( Aeval a1 e) ( Aeval a2 e)
| Blt a1 a2 => Zlt_bool ( Aeval a1 e) ( Aeval a2 e)
end.
Definition ExtEnv (v : Var) (z : Z) (e : Env) : Env :=
fun x : Var => if ( VarEq x v) then z else e x.
Inductive NS
| NSass
:
NS (Sass v
| NSskip
:
| NSif_T
:
Beval b e1
|
|
|
|
(∗
: Stm ->Env ->Env ->Prop :=
forall v a e,
a) e ( ExtEnv v ( Aeval a e) e)
forall e, NS Sskip e e
forall b S1 S2 e1 e2 ,
= true -> NS S1 e1 e2
-> NS (Sif b S1 S2) e1 e2
NSif_F
: forall b S1 S2 e1 e2 ,
Beval b e1 = false -> NS S2 e1 e2
-> NS (Sif b S1 S2) e1 e2
NSwhile _T : forall b S e1 e2 e3 ,
Beval b e1 = true -> NS S e1 e2
-> NS ( Swhile b S) e2 e3
-> NS ( Swhile b S) e1 e3
NSwhile _F : forall b S e,
Beval b e = false -> NS ( Swhile b S) e e
NScomp
: forall S1 S2 e1 e2 e3 ,
NS S1 e1 e2 -> NS S2 e2 e3 -> NS ( Scomp S1 S2) e1 e3
89
| N S r e p e a t _T : f o r a l l b S e1 e2 ,
NS S e1 e2 -> B e v a l b e2 = t r u e
-> NS ( S r e p e a t S b ) e1 e2
| N S r e p e a t _F : f o r a l l b S e1 e2 e3 ,
NS S e1 e2 -> B e v a l b e2 = f a l s e
-> NS ( S r e p e a t S b ) e2 e3
-> NS ( S r e p e a t S b ) e1 e3
∗)
.
Fixpoint Aopt (a : Aexp) :=
match a with
| Aadd a1 a2 =>
match (Aopt a1 , Aopt a2) with
| (Aval z1 , Aval z2) => Aval (z1+z2)%Z
| (a1 ’, a2 ’) => Aadd a1 ’ a2 ’
end
( ∗ | A m u l t a1 a2 =>
match ( A o p t a1 , A o p t a2 ) w i t h
| ( A v a l z1 , A v a l z 2 ) => A v a l ( z 1 ∗ z 2 )%Z
| ( a1 ’ , a2 ’ ) => A m u l t a1 ’ a2 ’
end ∗ )
| _ => a
end.
Fixpoint Bopt (b : Bexp) :=
match b with
| Bnot b’ =>
match Bopt b’ with
| Btrue => Bfalse
| Bfalse => Btrue
| b => Bnot b
end
| Band b1 b2 =>
match (Bopt b1 , Bopt b2) with
| (Btrue , Btrue ) => Btrue
| (Bfalse , _) | (_, Bfalse ) => Bfalse
| (b1 ’, b2 ’) => Band b1 ’ b2 ’
end
| Beq a1 a2 =>
match (Aopt a1 , Aopt a2) with
| (Aval z1 , Aval z2) =>
match Zeq_bool z1 z2 with
| true => Btrue
90
付録A
| false => Bfalse
end
| (a1 ’, a2 ’) => Beq a1 ’ a2 ’
end
| Blt a1 a2 =>
match (Aopt a1 , Aopt a2) with
| (Aval z1 , Aval z2) =>
match Zlt_bool z1 z2 with
| true => Btrue
| false => Bfalse
end
| (a1 ’, a2 ’) => Blt a1 ’ a2 ’
end
| _ => b
end.
Fixpoint Sopt (S : Stm) :=
match S with
| Sass x a => Sass x (Aopt a)
| Sif b S1 S2 =>
match Bopt b with
| Btrue => Sopt S1
| Bfalse => Sopt S2
| b’ => Sif b’ (Sopt S1) (Sopt S2)
end
| Swhile b S’ =>
match Bopt b with
| Bfalse => Sskip
| b’ => Swhile b’ (Sopt S ’)
end
| Scomp S1 S2 =>
match (Sopt S1 , Sopt S2) with
| (Sskip , S2 ’) => S2 ’
| (S1 ’, Sskip ) => S1 ’
| (S1 ’, S2 ’) => Scomp S1 ’ S2 ’
end
( ∗ | S r e p e a t S ’ b =>
match B o p t b w i t h
| B t r u e => S ’
| b ’ => S r e p e a t ( S o p t S ’ ) b ’
end ∗ )
| _ => S
end.
While 言語とその最適化器
91
Lemma Aopt_keep_ result : forall (a : Aexp) (e : Env),
Aeval a e = Aeval (Aopt a) e.
induction a; intuition ;
simpl in *; rewrite IHa1; rewrite IHa2;
case (Aopt a1 ); case (Aopt a2 ); auto.
Qed.
Lemma Bopt_keep_ result : forall (b : Bexp) (e : Env),
Beval b e = Beval (Bopt b) e.
induction b; intuition ; simpl in *.
rewrite IHb; case (Bopt b); auto.
rewrite IHb1; rewrite IHb2; case (Bopt b1); case (Bopt b2);
intros ; simpl ; auto.
case ( Beval b e); auto.
case ( Beval b e && Beval b0 e); auto.
case (Zeq_bool ( Aeval a e) ( Aeval a0 e)); auto.
case (Zlt_bool ( Aeval a e) ( Aeval a0 e)); auto.
rewrite (Aopt_keep_ result a); rewrite (Aopt_keep_ result a0);
case (Aopt a); case (Aopt a0 ); auto.
intros ; case_eq (Zeq_bool v0 v); auto.
rewrite (Aopt_keep_ result a); rewrite (Aopt_keep_ result a0);
case (Aopt a); case (Aopt a0 ); auto.
intros ; case_eq (Zlt_bool v0 v); auto.
Qed.
Theorem Sopt_keep_ semantics : forall (S : Stm) (e1 e2 : Env),
NS S e1 e2 -> NS (Sopt S) e1 e2.
intros S e1 e2 H; induction H; simpl.
rewrite Aopt_keep_ result ; constructor .
constructor .
case_eq (Bopt b); intros ; auto; rewrite Bopt_keep_ result in H;
rewrite H1 in H; try ( apply NSif_T; auto ); inversion H.
case_eq (Bopt b); intros ; auto; rewrite Bopt_keep_ result in H;
rewrite H1 in H; try ( apply NSif_F; auto ); inversion H.
case_eq (Bopt b); intros ; auto; rewrite Bopt_keep_ result in H;
rewrite H2 in H; simpl in IHNS2; rewrite H2 in IHNS2;
try ( eapply NSwhile _T; eauto ); inversion H.
case_eq (Bopt b); intros ; auto; rewrite Bopt_keep_ result in H;
rewrite H0 in H; try ( apply NSwhile _F; auto ); constructor .
case_eq (Sopt S1 ); intros ; try ( rewrite H1 in IHNS1 );
try ( rewrite H1 in IHNS2 );
try ( inversion IHNS1 ; auto; fail ).
92
付録A
While 言語とその最適化器
inversion IHNS1 ; case_eq (Sopt S2 ); intros ;
rewrite H6 in IHNS2 ; simpl in IHNS2;
try ( eapply NScomp ; eauto ).
inversion IHNS2 ; rewrite <- H9; auto.
case_eq (Sopt S2 ); intros ; rewrite H2 in IHNS2;
try ( econstructor ; eauto ; fail ).
inversion IHNS2 ; rewrite <- H5; auto.
case_eq (Sopt S2 ); intros ; rewrite H2 in IHNS2;
try ( econstructor ; eauto ; fail ).
inversion IHNS2 ; rewrite <- H5; auto.
case_eq (Sopt S2 ); intros ; rewrite H2 in IHNS2;
try ( econstructor ; eauto ; fail ).
inversion IHNS2 ; rewrite <- H5; auto.
(∗
c a s e _ eq ( S o p t S2 ) ; i n t r o s ; r e w r i t e H2 i n IHNS2 ;
t r y ( econstructor ; eauto ; f a i l ) .
i n v e r s i o n IHNS2 ; r e w r i t e <− H5 ; a u t o .
c a s e _ eq ( B o p t b ) ; i n t r o s ; a u t o ;
r e w r i t e B o p t _ k e e p _ r e s u l t i n H0 ;
r e w r i t e H1 i n H0 ; a p p l y N S r e p e a t _T ; a u t o .
c a s e _ eq ( B o p t b ) ; i n t r o s ; s i m p l i n IHNS2 ; r e w r i t e H2 i n IHNS2 ;
a u t o ; r e w r i t e B o p t _ k e e p _ r e s u l t i n H0 ; r e w r i t e H2 i n H0 ;
t r y ( e a p p l y N S r e p e a t _F ; e a u t o ) .
s i m p l i n H0 ; i n v e r s i o n H0 . ∗ )
Qed.
93
業績一覧
論文誌 (査読あり)
1. 森口 草介・渡部 卓雄, 定理証明支援系 Coq への対話的修正機構の導入, 情報
処理学会論文誌 プログラミング（PRO）, 5(4), pp. 27-38, Sep 2012.
国際会議 (査読あり)
1. Sosuke MORIGUCHI and Takuo WATANABE, An Interactive Extension Mechanism for Reusing Verified Programs, 28th ACM Symposium On Applied Computing, pp.1236-1243, Mar., 2013.
2. Sosuke MORIGUCHI and Takuo WATANABE, Abstraction of Operations of
Aspect-Oriented Languages, Theory and Practice of Computation, Proceedings
in Information and Communications Technology, Vol. 5, pp. 187-201, SprinterVerlag, Springer-Verlag, 2012. DOI: 10.1007/978-4-431-54106-6 15
3. Sosuke MORIGUCHI and Takuo WATANABE, A Calculus for Advice Weaving
Mechanisms (Position paper), 4th Asian Workshop on AOSD (AOAsia 4), Dec.,
2008. https://sites.google.com/site/aoasiaworkshop/aoasia-2008
口頭発表 (査読なし)
1. 安原 由貴・森口 草介・渡部 卓雄, 実時間システム向け文脈思考言語 ProcneJ,
第 93 回 情報処理学会 プログラミング研究会, Feb., 2013.
2. 安原 由貴・森口 草介・渡部 卓雄, 組込みシステムのための文脈指向仕様記
述に向けて, 日本ソフトウェア科学会 第 29 回大会, Aug., 2012.
3. 森口 草介・渡部 卓雄, Coq のための対話的修正機構を用いた変更の織り込み
手法, 日本ソフトウェア科学会 第 28 回大会, Sep., 2011.
4. 森口 草介・渡部 卓雄, 証明支援系 Coq のプログラムに対する対話的修正機
構の提案, 第 83 回 情報処理学会 プログラミング研究会, Apr., 2011.
5. 山田 一宏・渡部 卓雄・森口 草介・西崎 真也, 証明支援系を用いた Morris の二
分木走査アルゴリズムの検証情報処理学会ソフトウェア工学研究会, SE-171,
No. 26, 1-4, Mar., 2011.
6. 渡部 卓雄・森口 草介・山田 一宏・西崎 真也, プログラム変換を用いたポイ
ンタ操作プログラムの検証にむけて: Morris の二分木走査アルゴリズムによ
るケーススタディ, 電子情報通信学会ソフトウェアサイエンス研究会, 信学技
報, Vol. 110, No. 458, pp. 97-102, Mar., 2011.
7. 森口 草介・渡部 卓雄, Coq における仕様の拡張と証明の再利用, 日本ソフト
ウェア科学会 ディペンダブルシステムワークショップ (DSW2010), Jul., 2010.
8. 森口 草介・渡部 卓雄, アスペクトの適用範囲の明示に対する制御機構, 日本
ソフトウェア科学会 第 26 回大会, Sep., 2009.
9. 森口 草介・渡部 卓雄, アスペクト指向言語における操作の抽象化方式, 第 74
回 情報処理学会 プログラミング研究会, Jun., 2009.
10. 森口 草介・渡部 卓雄, LMC: アスペクト指向拡張の計算, 日本ソフトウェア
科学会 第 25 回大会, Sep., 2008.
11. 森口 草介・渡部 卓雄, LMC: ポイントカット・アドバイスモデルの計算, 電
子情報通信学会ソフトウェアサイエンス研究会, 信学技報 Vol. 108, No. 173
(SS2008-19), pp. 37-42, Jul., 2008.
ポスター発表 (査読なし)
1. 森口 草介・渡部 卓雄, 証明支援系 Coq における対話的修正機構の提案, 第 13
回 日本ソフトウェア科学会 プログラミングおよびプログラミング言語ワー
クショップ, Mar., 2011.
2. Sosuke MORIGUCHI, Aspect Passing Style: On the Confluence of an Aspectual Calculus, ACM AOSD ’10, Mar., 2010.
3. 森口 草介・渡部 卓雄, ジョインポイントモデルにおける操作の抽象化, 第 11
回 日本ソフトウェア科学会 プログラミングおよびプログラミング言語ワー
クショップ, Mar., 2009.
4. 森口 草介・渡部 卓雄, LMC: A Calculus for Aspect Extension, 第 10 回 日本
ソフトウェア科学会 プログラミングおよびプログラミング言語ワークショッ
プ, Mar., 2008.
以上