| 研究課題/領域番号 |
17K00011
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | 項書換え / 正規化性 / 定理自動証明 / 完備化 |
|---|
| 研究実績の概要 |
項書換えは等式変形によって計算を行う計算モデルであり、定理自動証明システムや宣言型プログラミング言語の理論基盤となっている。正規化性は計算結果が存在することを保証する性質であり、帰納的定理自動証明や遅延評価において重要な役割を果たす。しかしながら、強力な解析技法が多く存在する停止性と違い、正規化性の解析技術はまだ発展途上の段階にある。
平成２９年度は最内・最外停止性を用いた正規化性の自動証明技法、ループ検出による自動反証技法、そして正規化性問題を小さな問題に分割するモジュラリティによる変換手法の研究を行った。また、それらをベースにした正規化性の自動解析ツールを実装した。問題集を作成し行った評価実験においてそれらの有効性を確認したが、まだ改善の余地があり平成３０年度もこれらの研究を継続する。
計算結果が存在する場合に必ず計算結果へ辿り着く計算方法は「正規化戦略」と呼ばれる。等式自動証明の基盤手続きである完備化の研究において、正規化戦略がその効率化の鍵となる critical pair criteria に密接に関係していることが判明した。この研究を円滑に行うため、オーストリアの研究協力者らとともに完備化理論の整備を進めた。その結果、定理自動証明システム Waldmeister などに採用されている順序付き完備化 (ordered completion)に対して簡潔な健全性の証明を得た。さらに定理証明支援システム Isabelle/HOL でその形式証明を行った。この成果を取りまとめた論文は FSCD 2017 に採録された。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
先述の通り、定理自動証明の研究が進展し正規化性の応用が見つかった。これは当初予定していなかった成果である。一方その研究にやや時間を割かれたため、正規化性の自動解析技法の研究開発は一部、年度内に完了しなかった。
|
| 今後の研究の推進方策 |
引き続き正規化性解析の自動化に取り組む。また応用として見出した critical pair criteria と正規化戦略の関係については、その考察に基づく定理自動証明システムのプロトタイプを実装し評価実験を行う。来年度の課題である戦略抽出については、停止性・正規化性のモジュラ性を主軸に研究を行う。
|
