2012 Fiscal Year Annual Research Report
| Project/Area Number |
22500002
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Project Period (FY) |
2010-04-01 – 2013-03-31
|
| Keywords | 書き換えシステム / 合流性 / 自動検証 / 停止性 / モジュラ性 |
|---|
| Research Abstract |
項書き換えシステムの合流性を自動的に判定する方法を提案し、それにもとづく合流性自動判定システムACPの実装と改良を進めるとともに、その応用についても検討した。本自動判定システムの特徴は、項書き換えシステムを部分システムに分解して合流性を判定する分割統治法を利用している点である。本年度の主な研究実績は以下のとおりである。
(1) 合流性に関する国際ワークショップ(IWC 2012)における合流性自動判定システムの第１回コンペティションにおいて、本研究で開発されたACPは、参加３システム中第１位の成績で優勝することができた。
(2) 合流性の自動判定に重要な役割をはたす到達可能性の判定法について検討した。具体的には、ボトムアップ項書き換えシステムのクラス(BU)を最内書き換えに変更した最内ボトムアップ項書き換えシステムのクラス(IBU)を提案し、IBUに含まれる項書き換えシステムの最内書き換え到達可能性が判定可能であることを明らかにした。
(3) 等式が帰納的定理であるか否かは一般的には決定不能であるが、いくつかの部分クラスに対する決定手続きが知られている。本研究では、書き換え帰納法に基づく外山(2002)の決定手続きとFalkeら(2006)は決定手続きを組み合わせることで、両者が保証している決定可能な帰納的定理のクラスを拡張することに成功した。
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
