プログラム開発の効率性やプログラムの保守性のためには、 人の理解しやすいアルゴリズムによるプログラムが望まれます。 しかしながら、人の理解しやすいプログラムが 必ずしも計算機上で効率よく動作するとはかぎりません。 そこで、 プログラムの開発や保守は人間の理解しやすいプログラムのまま行い、 計算機上での実行用のプログラムには、 プログラムの自動変換をもちいてアルゴリズムを効率化したものを用いる方法が考えられます。
近年の研究から、 プログラムの効率化にはいくつか決まったやり方もあることが分かってきました。 その決まったやり方を一般化することでパターンを作成し、 そのパターンを用いて効率的なプログラムへ自動的にプログラムを変換する手法が研究されています。
従来のパターンを用いたプログラム変換はラムダ式を用いてプログラムを定式化していたため、 プログラム変換の正当性の検証や解析が困難でした。 我々の研究室では、 定理自動証明で用いられる項書き換えシステムに基づいたパターンによるプログラム変換の形式化を行いました。 項書き換えシステムに基づく我々の形式化では定理自動証明に用いられる技術を応用することにより、 プログラム変換によるプログラムの意味の不変性を保証することが可能です。 我々は項書き換えシステムに基づくモデル化により、 より検証に適した、強力なプログラム変換の手法を提案することを目指しています。
以下は、本研究室で開発したプロトタイプシステムを用いてプログラム変換を行った例です。 このプロトタイプシステムによるプログラム変換では、 出力プログラムが入力プログラムと同じ計算を行うことが保証されています。
まで．