| 研究課題/領域番号 |
17K00011
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | 項書換え / 正規化性 / 自動定理証明 / 完備化 |
|---|
| 研究実績の概要 |
項書換えは等式変形によって計算を行う計算モデルであり、宣言型プログラミング言語および自動定理証明システムの理論基盤となっている。「（弱）正規化性」は計算結果が存在することを保証する性質であり、実数や無限リストなどを扱うための遅延評価や、帰納的定理の自動証明において重要な役割を果たす。しかしながら強力な解析技法が多く存在する停止性と異なり、正規化性の自動解析技術は発展途上の段階にある。本研究の目標は正規化性を自動解析する技術を開発・発展させることである。
本年度の研究成果は以下の通り。
１．計算結果が存在する場合に必ず計算結果に辿り着く系統的な計算方法は「正規化戦略」と呼ばれる。平成３０年度は「正規化性の自動解析」手法を開発し、そして「戦略抽出」に、つまり正規化戦略を自動構成する手法の研究に取り組む予定であった。しかし研究を進めるうちにこの構想と計画は逆転させたほうがよいと気づいた。まず平成３１年度に行う予定であった「局所解析」の課題を前倒して行い、最左最外書き換えの正規化性を停止性に帰着させる変換を開発した。次に最左最外書き換えが正規化戦略になるように書き換えシステムを変換する手法を開発した。先述の通り項書換えの停止性証明に関しては強力な手法が確立しており、今回得られた２つの変換と既存の停止性解析手法を組み合わせることで、遅延評価戦略を用いる（一階の）プログラムの正規化性を自動証明できるようになった。
２．前年度は正規化性の調査から研究が派生し、完備化定理（自動定理証明の基盤技術）に関する成果が得られた。その一つは順序付き完備化 (ordered completion) の健全性定理に対する簡潔な形式証明であった。その理論整備を進めることで順序付き完備化の完全性定理 (Bachmair et al, 1989) に対しても見通しの良い形式証明を与えることに成功した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
先述の通り変換手法によるアプローチが奏功し前年度の遅れは解消された。
|
| 今後の研究の推進方策 |
先述の通り、正規化性解析の枠組が一通り完成した。今後は正規化性自動解析ツールを実装し解析能力の強化を図る。特に局所解析の強化に取り組む。またツールの性能評価のため遅延評価を用いるプログラムを集め、正規化性の問題集を作成する。
|
