2020 Fiscal Year Annual Research Report
Normalization Analysis for Term Rewriting
| 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 |
項書換えは等式変形によって計算を行う計算モデルであり、宣言型プログラミング言語および自動定理証明システムの理論基盤となっている。「(弱)正規化性」は計算結果が存在することを保証する性質であり、実数や無限リストなどを扱うための遅延評価や、帰納的定理の自動証明において重要な役割を果たす。しかしながら強力な解析技法が多く存在する停止性と異なり、正規化性の自動解析技術は発展途上の段階にある。本研究の目標は正規化性を自動解析する技術を開発・発展させることである。
本年度の研究成果は以下の通り。必須戦略は遅延評価を実現する代表的な計算手法であるが、必須戦略に基づく計算やその性質の解析が難しいという問題がある。昨年度までの研究により、構成子システムの必須戦略を最左最外戦略で模倣できるようにする「左正規化変換」を開発した。この手法は一階の関数に限定されていたが、本年度は高階関数を扱える作用型構成子システムへと変換手法の体系を拡張した。また作用型構成子システムの書換えにおいては、左正規化変換による変換可能性が、強逐次性と呼ばれる必須戦略の計算可能を保証する性質と同値になることを証明した。これらの成果をとりまとめた論文の投稿準備を進めている。
研究期間全体を通じた研究成果は以下の通り。遅延評価を変換を介して実現するための左正規化変換、および最左最外戦略の停止性を自動証明する技法を考案した。二つを組み合わせることにより正規化性を自動証明できる。また戦略の研究からの派生成果として、定理自動証明の基盤をなす（標準および順序付き）完備化手続きの新しい簡潔な健全性・完全性証明、さらに左線形項書換えシステムの計算結果の一意性を保証する強力な合流性の定理を得た。
|
