2010 Fiscal Year Annual Research Report
| Project/Area Number |
22500002
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Keywords | 書き換えシステム / 合流性 / 自動検証 / 停止性 / モジュラ性 |
|---|
| Research Abstract |
(1)項書き換えシステムの合流性を自動的に判定する方法を提案し、それにもとづく合流性自動判定システムのプロトタイプの実装と改良を進めた。本システムの特徴は、項書き換えシステムを部分システムに分解して合流性を判定する分割統治法を利用している点である。本年度は、与えられた項書き換えシステムのリダクション関係を保存してままシステムの変形を繰り返すことで合流性を自動証明する拡張完備化手法を提案し、それを合流性自動判定システムに組み込むことで、従来手法では困難であったAC規則を含む項書き換えシステムの合流性自動判定が可能となることを明らかにした。また、多くの文献から抽出した例題をもちいて合流性自動判定の実験を行い、本判定システムの有効性を示した。
(2)基底項書き換えシステムの合流性の多項式時間判定アルゴリズムでは、カリー変換とフラット変換という前処理が従来もちいられていた。本年度は、これらの前処理が不要となる効率的な判定アルゴリズムを提案し、アルゴリズムの正当性の証明を与えるとともに、実験を通してその有効性を検証した。
(3)項書き換えシステムの多項式サイズ正規形を保証する新しい経路順序として擬置換軽経路順序を提案し、従来知られていた軽多重集合経路順序の真の拡張になっていることを示した。
|
