| 研究課題/領域番号 |
25730004
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 項書換え / 合流性 / 国際研究者交流 / オーストリア |
|---|
| 研究概要 |
インスブルック大学、名古屋大学のグループと共同研究を行い次の４つの成果を得た。
現在の合流性解析における困難な問題の１つは、結合律・交換律を含むシステムの解析である。その合流性の自動解析に必要になる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）をインスブルック大学・東北大学と共催した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究会合での検討において、合流性解析の鍵となる危険対の性質について発見があったため、次年度に合流性解析に関する研究課題の１つを前倒した。一方で、課題の優先順序の変更により予定していた構文解析の研究は年度内に完了しなかった。
|
| 今後の研究の推進方策 |
引き続き、構文解析の研究に取り組む。来年度の中心テーマになる合流性解析については、非線形項書換えに関する合流性研究のエキスパートである大山口教授（名古屋大学）を研究協力者に迎え、研究に取り組む。
また、合流性解析ツールの効率性・利便性向上には高速な（相対）停止性解析が必要になることが、今年度の研究において明確になった。効率的な停止性解析の実現を図る。
|
