2014 Fiscal Year Research-status 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-25 に論文採択済)。 可換性の研究を応用することで、関数型言語の遅延評価の基礎になっている正規化定理に対し簡潔な証明を与えた。この成果と、平成25年度に発表した計算量解析のための手法(RTA-TLCA 2014)を組み合わせることで、基本正規化定理という遅延評価実装に有効な枠組みを構築した(国際ワークショップ IFIP WG 1.6 の招待講演として発表、国際会議 RTA 2015 に論文採択済)。 また合流性を効果的に特徴づける critical-pair-closing system の概念を共同研究により得た(国際ワークショップ IWC 2014 で口頭発表)。 最後に学会活動について。7月にウィーンにおいて3回目となる合流性の自動解析ツールの国際コンペティション(CoCo 2014)をインスブルック大学・東北大学と共催した。また合流性問題の公開データベース Cops の開発・運営を行っているが、そのバックエンドシステムの刷新を行った。
|
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 |
単一化自動化の研究、および合流性自動解析とその理論研究を重点的に行う。前者に関してはインスブルック大学、後者に関しては名古屋大学の研究協力者と連携して行う。
|
-
[Journal Article] AC-KBO Revisited2015
Author(s)
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
-
Journal Title
Theory and Practice of Logic Programming
Volume: 未定
Pages: 印刷中
Peer Reviewed / Open Access / Acknowledgement Compliant
-
-
[Presentation] Leftmost Outermost Revisited2015
Author(s)
Nao Hirokawa, Aart Middeldorp and Georg Moser
Organizer
26th International Conference on Rewriting Techniques and Applications
Place of Presentation
ワルシャワ、ポーランド
Year and Date
2015-06-29 – 2015-07-01
-
-
-
-
-