等価変換ルールの生成方法の理論的基礎

概要

論文の詳細を見る
本発表では仕様からプログラムを合成する方法を提案し, その正当性を保証する理論を開発する.基礎となるのは「等価変換モデル」と呼ばれる新しい計算モデルである.等価変換モデルでは仕様は(拡張された)確定節の集合で表現され, プログラム合成の主要部分は仕様からの新しい等価変換ルールの生成である.等価変換モデルでは新しいルールを採用するごとにプログラムを改善でき, 最終的に効率の良いプログラムを得る可能性がある.Prologのプログラム変換では, 確定節(仕様)が確定節(プログラム)に変換されるが, ルール生成はそれとは異なる. ルールを生成するためにメタ記述を用いる.メタ記述は具体化によって得られる(無限の)記述を代表している.メタ記述が等価変換されるとは, それが代表するすべての記述が等価変換されることである.メタ記述の対から等価変換ルールが得られる. メタ記述はメタルールによって変換する.アンフォールド変換, フォールド変換, その他の変換などに対応するメタルールを使えるので, 提案する方法は論理プログラミングのアンフォールド/フォールド変換に劣らない効率化を達成することができる.本方法の最も重要な特徴の1つはモジュラー性である.すなわち, 個々のメタルールは他のメタルールとはまったく無関係に正当性を判定できる.メタルールは任意の順序で適用できるが, 論理プログラミングのプログラム変換ルールはそうではない.正しいメタルールの繰り返し適用によって等価な2つのメタ記述が得られ, それらから正当な等価変換ルールが得られることを証明する.
一般社団法人情報処理学会の論文
1999-08-15

等価変換ルールの生成方法の理論的基礎

スポンサーリンク

概要

著者

関連論文

スポンサーリンク