| 研究課題/領域番号 |
25330004
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| 研究分担者 |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 項書き換えシステム / 合流性 / 定理自動証明 / 自動検証 |
|---|
| 研究概要 |
項書き換えシステムの合流性を自動的に検証する方法を提案し、それに基づいて合流性自動証明システムACPの実装と改良を進めるとともに、プログラム自動検証や定理自動証明に必要となる関連技術を検討した。本年度の主な研究実績は以下のとおりである。
(1) 項書き換えシステムの合流性証明法としてルールラベリングに基づく減少ダイアグラム法が知られている。しかし、非線型項書き換えシステムに対してはこの証明法をそのまま適用することが困難である。そこで、永続性と型情報を利用した減少ダイアグラム法を提案し、従来手法では困難であった非線型項書き換えシステムの合流性自動証明に成功した。
(2) 項書き換えシステムの到達可能性判定問題を効率的に解くための単純な閉包操作手続きは、基底項書き換えシステムに対してはすでに提案されていた。この閉包操作手続きを拡張することで、より広いクラスである右基底項書き換えシステムに対する効率の良い到達可能性自動判定手続きを実装した。
(3) 自動検証を目的としたプログラム変換法である文脈移動法と文脈分割法を適用することにより、文脈移動法と文脈分割法に基づく項書き換えシステムの自動変換法を提案するとともに、変換の正当を保証する条件を明らかにした。さらに、項書き換えシステムの自動変換法と書き換え帰納法に基づいて、帰納的定理の自動証明システムを実現した。
(4) 束縛変数をもつ書き換えが可能である名目書き換えシステムの形式化を行い、合流性の実効的な判定手続きが実現可能となるための十分条件を明らかにした。従来の合流条件は、無限個の危険対に対する交差性を検証することが必要となるため、実効的な判定手続きの実現が困難であった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
下記の項目で計画以上の進展があった．
(1) リダクションの到達可能性： 右基底項書き換えシステムの到達可能性を判定する閉包操作手続きを提案し，判定時間の計算量を理論的に解析するとともに，実装・実験を行った．
(2) 合流性の自動判定： 項書き換えシステムの永続性と型情報を利用することで，従来は困難であった減少ダイアグラム法による合流性判定が非線型項書き換えシステムに対して適応可能となることを明らかにした．
(3) 高階システムの合流性： 名目書き換えシステムの形式化と合流性の実効的な十分条件を与えた．
(4) プログラム自動検証： 自動検証のためのプログラム変換法である文脈移動法と文脈分割法が，項書き換えシステムに対しても有効であること理論的に示した．
|
| 今後の研究の推進方策 |
以下方針で研究を進める．
(1) リダクションの到達可能性： 閉包操作に基づく到達可能性判定法を改良することで，右基底項書き換えシステムよりも広いクラスに対して適用できることを明らかにする．
(2) 合流性の自動判定： 減少ダイアグラム法，危険対解析，階層構造解析，永続性，型情報などを組み合わせることによって，項書き換えシステムの新しい合流性判定法を提案する．
(3) 高階システムの合流性： 名目書き換えシステムの完備化手続きの実現と，それに基づく高階定理自動証明の実験を行う．
(4) プログラム自動検証： 書き換え帰納法と項書き換えシステム変換法を組み合わせた高機能なプログラム自動検証法を検討する．
|
| 次年度の研究費の使用計画 |
今年度に予定していた論文の出版が遅れたため，論文掲載料が年度内に執行できなかった．
次年度に論文を出版し，論文掲載料として使用する．
|
