| 研究課題/領域番号 |
22700028
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
GARRIGUE Jacques 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| キーワード | プログラミング言語論 / プログラムパラダイム / 定理証明支援系 |
|---|
| 研究概要 |
この一年では、データ型および可変なデータ型の実装方法を検討し、実装を始めた。そこで特に問題になったのは、今まで作って来た証明の全ての補題を拡張する必要があり、場合によって補題の命題自体も変える必要があった。このため、もっとモジュラリティの高い証明の構築方法を検討し始めた。来年度はこれを用いて拡張を完成させたい。
また、今回のインタープリターに含まれないものの、再帰モジュールにおける参照関係の判定可能性に関する研究をタリン大学の中田景子さんと一緒に行っており、そのアルゴリズムの正しさをCoqで証明した。その際、扱っている対象が高階関数を含めないことを利用して、束縛変数を相対的ではなく絶対的に扱うことができた。それによって、様々な証明がやりやすくなったので、こういう方法が高階関数を含む体系にも応用できないか、検討し始めた。
少し趣きが違うが、この研究の対象でもあるOCamlの開発にも遂行しており、昨年Jacques Le Normandと一緒に手がけた一般化代数データ型(GADT)の実装を完成させた。そこで今回の研究でも対象になっている主要性が問題になり、フランスのINRIAのDidier Remyと一緒に検討した結果、曖昧性の問題を解決する方法が見つかった。曖昧性のなさは主要性より弱い性質だが、GADTに関して本当の意味での主要性は完全な型注釈がなければ得られないので、曖昧性の解決がより重要な性質になる。将来的に当検証された型検証器についても、主要性と曖昧性のなさを区別する必要が出てくると思われる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
もとの方針では、機能を次々とコア言語に追加する予定であったが、これでは相乗効果で証明が複雑になり、新たに機能を追加する際の壁が段々高くなる。そのために、そういうことの起きない証明の構造を考えなければならない。
|
| 今後の研究の推進方策 |
研究実績の概要や現在までの達成度に書いたように、今までの方法で次々と新しい機能を追加して行くのはかなりの労力を必要とする。モジュラリティの高いやり方を考えながら、各機能を別々で証明して行く形で進めるつもりである。最終的には全ての部分をまとめて一つの型検証器を作らなければならないが、それぞれの部分に対して新しい試みができ、より良い方法が見つかる可能性がある。
|
