研究課題
項書き換えシステムの合流性を自動的に判定する方法を提案し、それにもとづく合流性自動判定システムACPの実装と改良を進めるとともに、その応用についても検討した。本自動判定システムの特徴は、項書き換えシステムを部分システムに分解して合流性を判定する分割統治法を利用している点である。本年度の主な研究実績は以下のとおりである。(1) 合流性に関する国際ワークショップ(IWC 2012)における合流性自動判定システムの第１回コンペティションにおいて、本研究で開発されたACPは、参加３システム中第１位の成績で優勝することができた。(2) 合流性の自動判定に重要な役割をはたす到達可能性の判定法について検討した。具体的には、ボトムアップ項書き換えシステムのクラス(BU)を最内書き換えに変更した最内ボトムアップ項書き換えシステムのクラス(IBU)を提案し、IBUに含まれる項書き換えシステムの最内書き換え到達可能性が判定可能であることを明らかにした。(3) 等式が帰納的定理であるか否かは一般的には決定不能であるが、いくつかの部分クラスに対する決定手続きが知られている。本研究では、書き換え帰納法に基づく外山(2002)の決定手続きとFalkeら(2006)は決定手続きを組み合わせることで、両者が保証している決定可能な帰納的定理のクラスを拡張することに成功した。
24年度が最終年度であるため、記入しない。
すべて 2013 2012
すべて 雑誌論文 (4件) (うち査読あり 4件) 学会発表 (1件) (うち招待講演 1件)
コンピュータソフトウェア
巻: Vol.30, No.1 ページ: 187-202
Logical Methods in Computer Science
巻: Vol.8, No.1:31 ページ: 1-29
http://www.lmcs-online.org/ojs/viewarti cle.php?id=1099&layout=abstract
Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012)
巻: LNCS 7562 ページ: 172-186
巻: Vol.29, No.1 ページ: 211-239
