2009 Fiscal Year Annual Research Report
| Project/Area Number |
19500003
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 Tohoku University, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Keywords | 情報基礎 / プログラム変換 / 定理自動証明 / 書き換えシステム / 書き換え帰納法 / 融合変換 / 変換パターン / 補題自動導入法 |
|---|
| Research Abstract |
変換パターンに基づくプログラム変換を多くのプログラム変換に適用するためには、変換パターンの蓄積が必要である。そこで、具体的なプログラム変換やより一般的でない変換パターンから、より一般的な変換パターンを抽出する方法について検討を進めた。2階の一般化アルゴリズムを提案し、その健全性の証明を与えた。一般化アルゴリズムに基づき、変換パターン抽出実験システムを構築し、変換パターンの抽出実験を行った。現存のアルゴリズムでは変換に利用するには不適当なパターンも多数同時に抽出してしまう。そこで、変換に利用可能なパターンの抽出を容易にするためヒューリスティクスについて検討を行い、とくつかの変換パターンの抽出に成功した。また、プログラム変換をより広いクラスに適用するためのS式書き換えシステムのための停止性証明法について検討を進めた。プログラム変換の正当性検証時に必要な書き換え帰納法を強化するために、書き換え帰納法の高度化の研究を進めた。特に反証機能つきの書き換え帰納法に適した補題自動導入法について検討を行った。発散鑑定法を改良し、健全性を持つ発散鑑定法を提案した。実験システムを実装するとともに証明システムのベンチマークとなる例題集を抽出し、他の書き換え帰納法に基づく定理証明器との比較実験を行った。また、プログラム変換の正当性検証や反証付き書き換え帰納法を利用するために必要な合流性を保障する方法について検討を進めた。停止性の検証器は多数提案されているのに対して、合流性の検証器の提案はあまりなされていないため、合流性の自動検証法について実験システムを構築し検討を行った。合流性の十分条件を満たさない項書き換えシステムについて分解手法を用いる判定法を利用することの検討を行い、分解手法を利用した合流性検証器の提案を行った。
|
