小さな関数を組み合わせて作られたプログラムは、 関数間のデータの受け渡しに大きなコストがかかります。 このようなプログラムを余分なデータを作らない効率的なプログラムへと変換する手法は、 プログラム融合変換とよばれます。
定理自動証明の手法である書き換え帰納法をもちいると、 書き換えシステムで表現されたプログラムの融合変換を実現できます。 書き換え帰納法は、 書き換えシステムで表現されたプログラムの性質を自動的に検証する手法です。 このため、書き換え帰納法を用いた融合変換では、 与えられたプログラムの性質を自動的に証明しつつ、 プログラム変換を進めることが可能になります。 このため、従来より強力な変換が可能になります。
我々の研究室では、 書き換え帰納法を用いたプログラム融合変換を行うプロトタイプシステムの開発と実験を進めています。 以下は、本研究室で開発したプロトタイプシステムにより行ったプログラム融合変換の例とプログラム融合変換が書き換え帰納法により実行される様子です。
まで．