2017 Fiscal Year Research-status Report
| Project/Area Number |
17K00011
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 項書換え / 正規化性 / 定理自動証明 / 完備化 |
|---|
| Outline of Annual Research Achievements |
項書換えは等式変形によって計算を行う計算モデルであり、定理自動証明システムや宣言型プログラミング言語の理論基盤となっている。正規化性は計算結果が存在することを保証する性質であり、帰納的定理自動証明や遅延評価において重要な役割を果たす。しかしながら、強力な解析技法が多く存在する停止性と違い、正規化性の解析技術はまだ発展途上の段階にある。
平成２９年度は最内・最外停止性を用いた正規化性の自動証明技法、ループ検出による自動反証技法、そして正規化性問題を小さな問題に分割するモジュラリティによる変換手法の研究を行った。また、それらをベースにした正規化性の自動解析ツールを実装した。問題集を作成し行った評価実験においてそれらの有効性を確認したが、まだ改善の余地があり平成３０年度もこれらの研究を継続する。
計算結果が存在する場合に必ず計算結果へ辿り着く計算方法は「正規化戦略」と呼ばれる。等式自動証明の基盤手続きである完備化の研究において、正規化戦略がその効率化の鍵となる critical pair criteria に密接に関係していることが判明した。この研究を円滑に行うため、オーストリアの研究協力者らとともに完備化理論の整備を進めた。その結果、定理自動証明システム Waldmeister などに採用されている順序付き完備化 (ordered completion)に対して簡潔な健全性の証明を得た。さらに定理証明支援システム Isabelle/HOL でその形式証明を行った。この成果を取りまとめた論文は FSCD 2017 に採録された。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
先述の通り、定理自動証明の研究が進展し正規化性の応用が見つかった。これは当初予定していなかった成果である。一方その研究にやや時間を割かれたため、正規化性の自動解析技法の研究開発は一部、年度内に完了しなかった。
|
| Strategy for Future Research Activity |
引き続き正規化性解析の自動化に取り組む。また応用として見出した critical pair criteria と正規化戦略の関係については、その考察に基づく定理自動証明システムのプロトタイプを実装し評価実験を行う。来年度の課題である戦略抽出については、停止性・正規化性のモジュラ性を主軸に研究を行う。
|
Research Products
(4 results)
-
-
-
[Presentation] Infinite Runs in Abstract Completion2017
Author(s)
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler
Organizer
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, Leibnitz International Proceedings in Informatics 84, pp. 19:1-19:16, 2017.
Int'l Joint Research
-
