| 研究概要 |
完備化に基づくプログラム融合変換が失敗した場合には,どのような条件を追加すれば変換が成功するかを調べた.さらに,より広いクラスのプログラムに対して変換が成功するように,完備化手続きの改良を行った.
具体的には、項書き換えシステムに基づいた融合変換手続きの形式化を行い、融合変換手続きの停止条件に焦点を絞った解析を行った.その結果,変換途中で生成される項のパターンが高々有限となるための条件と,融合変換手続きの停止条件は密接に関係していることが明らかになった.この成果に基づき,項の反復パターンを発見すると新しい関数として自動的に定義するメカニズムを,完備化手続きに組み込んだ.この拡張された完備化手続き上でプログラム融合変換の実験を計算機上で行ない,従来は完備化が発散して失敗して例に対しても,融合変換が可能となることを示した.
さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,帰納的定理の判定問題が決定可能となるための十分条件を解析し,融合変換に帰納的定理を自動適用する可能性を検討した.帰納的定理の判定問題を一般化し,抽象的なリダクションシステムの等価性判定問題としてとらえることにより,書き換え帰納法に基づく簡明で見通しの良い判定条件を与えることに成功した.この条件は,従来知られていた結果の拡張になっている.ここで与えられた決定可能条件は,Kapurら(2000,2001)の条件の一般化となっており,より広いクラスの決定問題に対して適用可能である.
|
