2015 Fiscal Year Annual Research Report
| Project/Area Number |
25730004
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 項書換え / 合流性 / 可換性 / 形式言語 |
|---|
| Outline of Annual Research Achievements |
項書換えシステムはプログラムの実行や定理自動証明の演繹を扱う計算モデルであり、関数型言語や定理証明システムの基盤理論として用いられている。項書換えの合流性は計算結果の一意性を保証する応用において重要な性質であり、その性質を自動的かつ効果的に解析する理論的枠組みと自動化手法の確立は、現在の合流性研究における焦点となっている。本年度（平成２７年度）、私たちの研究グループは次に挙げる合流性解析のための理論的成果と、合流性の応用に関する萌芽的成果を得た。
まず理論的成果について。前年度（平成２６年度）、項書換えシステムの合流性をそのサブシステムの可換性から証明する枠組みを構築、その有効性を示した。しかし一方で、可換性がシグネチャ拡張に対して保存されないという問題が判明した (CADE 2015)。この非保存性は本枠組みの足枷になる懸念事項であった。本年度、問題を解決すべく研究を行い、左線形の書換えシステムではこの問題が生じないことを突き止めた (IWC 2015)。左線形以外で可換性が成立することはほとんどないため、実用上の問題は解決を迎えた。
応用に関する成果ついて。合流性に基づく構文解析は断念したが、そこでの知見を形式言語理論に適用した結果、包含関係の決定問題に応用できることが判明した。与えられた正則言語を包含するかを多項式時間で決定できる文脈自由法のクラスを発見した。この応用は今後も調査を続ける予定である。
最後に学会活動について述べる。８月にベルリンにおいて４回目となる合流性の自動解析ツールの国際コンペティション CoCo 2015 を開催した。これはインスブルック大学・東北大学・名古屋大学との共同開催である。コンペティションの模様と結果はウェブサイト上で一般公開されている。前年度に引き続き、そのプレゼンテーション機能強化のため、バックエンドシステム開発・刷新を行った。
|
Research Products
(4 results)
