2011 Fiscal Year Annual Research Report
| Project/Area Number |
22700009
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| Keywords | 計算理論 / 関数型プログラム |
|---|
| Research Abstract |
本研究の目的は、関数型言語や定理証明システムに対して有用でありながらも、研究成果がほとんどなかった「非決定的な」(非直交な)項書き換えシステムの理論を構築することである。本年度は、(1)計算の答え(正規形)の一意性を保証する合流性と、(2)答えに辿り着く書き換えの仕方(正規化戦略)の研究、また(3)定理証明への応用へ向けた研究を行った。
まず合流性の研究について。前年度までに「減少合流性」の定理を得ていたが、その証明は繁雑な部分を含んでいた。減少ダイアグラムの拡張版、並行ステップの証明項と直交化手法を用いることで簡潔な証明を得ることに成功した。また規則ラベルと呼ばれる合流性解析手法の拡張に取り組んだ。これらの成果は国際論文誌JARに採録された。
当初、上記の定理をDevelopment Closure Theoremを包含する形へ一般化することを予定していたが、他の研究者がその試みを表明したため、より難易度の高い左非線形システムのための合流性条件の研究を行うことにした。結果、Knuth-Bendixの合流性条件の一般化に成功した。ストリームなど停止性を持たない体系に対する定理証明の基盤になることが期待される。またこの定理に基づく合流性自動解析のため、E単一化理論に関する性質を証明し、その強力さを実験により示した。これらの成果をまとめた論文は国際会議LPAR-18に受理された。
前年度、定理自動証明の基盤である完備化アルゴリズムに対し、極大完備化という簡易で高効率な手法を開発した。これを帰納的定理証明システムに適用するため、制約付き等式という概念を考案した。さらにそれに基づく定理証明システムを実装した。来年度も引き続き研究を行う。
戦略については、前年度に最外戦略が正規化戦略になることを証明したが、証明に自明でない部分があること判明した。ギャップの対処は来年度に引き継ぐ。
|
| 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 |
本研究分野を、項書き換え研究における新たなメインストリームとして位置付けるため、研究コミュニティの形成が必要と考えている。そのため来年度、合流性に関する第一回国際ワークショップおよび合流性解析ツールの第一回国際大会を開催する。研究テーマである非決定計算に関する項書き換え理論の応用に関しては、計画当時は定理証明のみを想定していた。しかしAaron Stump(アイオワ大学)との共同研究で構文解析へも応用可能であることを突き止めた。来年度はこの研究を既存の課題に加えて行う。最後に、研究協力者に合流性・戦略のエキスパートであるVincent Oostrom(ユトレヒト大学)を加える予定である。
|
