2013 Fiscal Year Research-status Report
| Project/Area Number |
25730004
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 項書換え / 合流性 / 国際研究者交流 / オーストリア |
|---|
| Research Abstract |
インスブルック大学、名古屋大学のグループと共同研究を行い次の４つの成果を得た。
現在の合流性解析における困難な問題の１つは、結合律・交換律を含むシステムの解析である。その合流性の自動解析に必要になるAC停止性の自動証明手法を開発した。この成果を取りまとめた論文は国際会議 FLOPS 2014 に採択された。
Ｅ単一化および定理自動証明の基盤技術である Knuth-Bendix の完備化 (1970) について共同研究を行い、現在教科書で採用されている標準の証明よりはるかに簡潔な証明を発見した。定理証明システムや計算機代数システムの理論基盤を刷新するものと期待している。この成果は国際会議 ITP 2014 で発表予定である。
さらに、項書換えシステムの計算過程を解析する手法を開発した。合流性・停止性・計算量解析など様々な性質の検証技法への応用が期待される。この成果は RTA-TLCA 2014 で受理された。
また次年度の課題の１つを前倒して行い、合流性の主要２定理（Rosen 1973, Knuth and Bendix 1970）と可換性定理（Toyama 1988）を左線形システムの場合に統合する萌芽的な定理を得た（IWC 2013で口頭発表）。最後に、学会活動について。第２回合流性に関する国際ワークショップ（IWC 2013）を主催、また合流性の自動解析ツールの国際コンペティション（CoCo 2013）をインスブルック大学・東北大学と共催した。
|
| 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 |
引き続き、構文解析の研究に取り組む。来年度の中心テーマになる合流性解析については、非線形項書換えに関する合流性研究のエキスパートである大山口教授（名古屋大学）を研究協力者に迎え、研究に取り組む。
また、合流性解析ツールの効率性・利便性向上には高速な（相対）停止性解析が必要になることが、今年度の研究において明確になった。効率的な停止性解析の実現を図る。
|
Research Products
(5 results)
-
-
-
[Presentation] AC-KBO Revisited2014
Author(s)
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
Organizer
12th International Symposium on Functional and Logic Programming
Place of Presentation
金沢市石川県立美術館
Year and Date
20140604-20140606
-
-
