2019 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 |
項書換えは等式変形によって計算を行う計算モデルであり、宣言型プログラミング言語および自動定理証明システムの理論基盤となっている。「(弱)正規化性」は計算結果が存在することを保証する性質であり、実数や無限リストなどを扱うための遅延評価や、帰納的定理の自動証明において重要な役割を果たす。しかしながら強力な解析技法が多く存在する停止性と異なり、正規化性の自動解析技術は発展途上の段階にある。本研究の目標は正規化性を自動解析する技術を開発・発展させることである。
本年度の研究成果は以下の通り。
1. 必須戦略は遅延評価を実現する代表的な計算手法である。昨年度、「左正規化変換」と「停止性グラフ」という手法による正規化性を自動証明する萌芽的な枠組みを構築した。しかし後者は証明能力が不十分であった。本年度は問題集を構成、手法の実験・分析を行い、十分完全性と呼ばれる性質が正規化性証明の鍵となることを突き止めた。停止性グラフの手法を十分完全性をベースに切り替えることで正規化性の証明能力を大きく改善させることに成功した。
2. 停止性グラフを構成する際に非正規化性を検出する簡易な手法を開発した。遅延評価を用いるプログラム・関数は潜在的に停止しない計算を含むため、そのリスクを回避する上で非正規化性の検出は重要である。
3. 正規化性研究から派生した成果として計算結果が一意になることを保証する強力な合流性の定理を２つ得ていたが、それらを論文としてまとめ発表した。定理の１つは strong closedness (Huet 1980) の一般化であり、もう一つは developement closedness (van Oostrom 1997) の一般化である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
実験データの分析から先述の十分完全性の知見を得るまでに時間を要したが、概ね順調に進んでいるといえる。
|
| Strategy for Future Research Activity |
正規化性解析は証明・反証とも可能になった。しかし反証手法はまだ着手したばかりであり反証能力は高くない。その能力強化を図る。
遅延評価を用いる関数型言語、定理証明支援システムは高階関数を扱えるよう設計されているものが多い。開発した「左正規化変換」「停止性グラフ」を作用型項書換えに拡張することで、それらの体系を扱えるようにする。
|
| Causes of Carryover |
国内出張を取り止めたため。翌年度、国内出張が可能ならそれに使用する。可能でなければ実験機材（PC機器）に使用する。
|
-
-
-
[Journal Article] Abstract Completion, Formalized2019
Author(s)
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler.
-
Journal Title
Journal of Logical Methods in Computer Science
Volume: 15(3)
Pages: 1:1 - 1:19
DOI
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
