| 研究概要 |
プログラム変換の手法である融合変換と,定理自動証明の手法である完備かを組み合わせた新しいプログラム変換手法を提案することを目的として,プログラム変換の実験と解析を行なった.とくに,帰納的定理の強力な自動証明手法である書き換え帰納法と組み合わせることによって,より広いクラスのプログラムに対して変換が可能となるように改良を行った.
実装では,関数型プログラムの形式的モデルとして,我々の提案したS式書き換えシステムをもちいた.S式書き換えシステムは,高階システムの取り扱いが簡単であり,書き換え帰納法で不可欠なリダクションの停止性を,高階にもかかわらず辞書式経路順序で簡単に判定することが可能である.我々は,S式書き換えシステムに対する書き換え帰納法を実装し,それをもちいてプログラム融合変換が多くの例で実現できることを示した.
我々の開発したプログラム融合変換法の特徴は,書き換え帰納法を直接適用して融合変換を実現しているため,自動証明システムとプログラム変換システムが一体となって働く.したがって,プログラム変換で必要な補題を自動証明しながら,その証明結果を利用して変換を進めることが可能である.
さらに,より強力なプログラム変換システムを開発するために,変換パターンに基づくプログラム変換手法の開発を進めるとともに,プログラム変換に不可欠な基礎技術である高階プログラムの帰納的性質の自動証明手続きや高階プログラムの停止性について理論的な解析を行った.
|
