2008 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 |
(i) プログラム変換をより広いクラスに適用するためには、関数引数の取り扱いを可能とする高階関数型言語への拡張が不可欠である。そこで、高階関数型言語の計算モデルであるS式書き換えシステムの停止性について解析し、非常に簡明な停止性の証明方法を与えた。さらに、その結果に基づいて従来よりも強力な停止性判定方法を提案した。
(ii) プログラム変換の正当性検証や反証付き書き換え帰納法を利用するためには、本研究の計算モデルである項書き換えシステムの合流性を保証することが必要となる。そこで、与えられた項書き換えシステムの合流性を自動的に判定する方法を提案し、それにもとづく合流性自動判定システムのプロトタイプを実装した。本システムの特徴は、項書き換えシステムを部分システムに分解して合流性を判定する分割統治法を利用している点である。多くの文献から抽出した例題をもちいて合流性自動判定の実験を行い、本判定システムの有効性を示した。なお、合流性の自動判定システムの本格的な開発は本研究が世界初であり、ここで得られた実験データは高機能なプログラム変換システムの開発に不可欠である。
(iii) プログラム変換の正当性検証時に必要な書き換え帰納法を強化するために、反証機能つきの書き換え帰納法に適した補題自動導入法について検討を進めた。具体的には、従来知られていた発散鑑定を改良し、健全性を持つ発散鑑定法を開発した。さらに、実験システムの改良を進めるとともに、システムのベンチマークとなる例題集を充実させ、他の証明システムとの比較実験をとおして提案手法の有効性を明らかにした。
|
