| 研究課題/領域番号 |
17K00011
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | 項書換え / 正規化性 / 合流性 |
|---|
| 研究実績の概要 |
項書換えは等式変形によって計算を行う計算モデルであり、宣言型プログラミング言語および自動定理証明システムの理論基盤となっている。「(弱)正規化性」は計算結果が存在することを保証する性質であり、実数や無限リストなどを扱うための遅延評価や、帰納的定理の自動証明において重要な役割を果たす。しかしながら強力な解析技法が多く存在する停止性と異なり、正規化性の自動解析技術は発展途上の段階にある。本研究の目標は正規化性を自動解析する技術を開発・発展させることである。
本年度の研究成果は以下の通り。
1. 必須戦略は遅延評価を実現する代表的な計算手法である。昨年度、「左正規化変換」と「停止性グラフ」という手法による正規化性を自動証明する萌芽的な枠組みを構築した。しかし後者は証明能力が不十分であった。本年度は問題集を構成、手法の実験・分析を行い、十分完全性と呼ばれる性質が正規化性証明の鍵となることを突き止めた。停止性グラフの手法を十分完全性をベースに切り替えることで正規化性の証明能力を大きく改善させることに成功した。
2. 停止性グラフを構成する際に非正規化性を検出する簡易な手法を開発した。遅延評価を用いるプログラム・関数は潜在的に停止しない計算を含むため、そのリスクを回避する上で非正規化性の検出は重要である。
3. 正規化性研究から派生した成果として計算結果が一意になることを保証する強力な合流性の定理を２つ得ていたが、それらを論文としてまとめ発表した。定理の１つは strong closedness (Huet 1980) の一般化であり、もう一つは developement closedness (van Oostrom 1997) の一般化である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
実験データの分析から先述の十分完全性の知見を得るまでに時間を要したが、概ね順調に進んでいるといえる。
|
| 今後の研究の推進方策 |
正規化性解析は証明・反証とも可能になった。しかし反証手法はまだ着手したばかりであり反証能力は高くない。その能力強化を図る。
遅延評価を用いる関数型言語、定理証明支援システムは高階関数を扱えるよう設計されているものが多い。開発した「左正規化変換」「停止性グラフ」を作用型項書換えに拡張することで、それらの体系を扱えるようにする。
|
| 次年度使用額が生じた理由 |
国内出張を取り止めたため。翌年度、国内出張が可能ならそれに使用する。可能でなければ実験機材（PC機器）に使用する。
|
