完備化に基づくプログラム自動変換の研究

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14019003
• Research Institution: Tohoku University
• Principal Investigator: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• Co-Investigator(Kenkyū-buntansha): 草刈 圭一朗 東北大学, 電気通信研究所, 助手 (90323112)
• Keywords: プログラム変換 / 完備化 / 融合変換 / 自動証明

Research Abstract

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

Research Products

• [Publications] Yoshihito Toyama: "Decidability for left-linear growing term rewriting systems"Information and Computation. 178. 499-514 (2002)
• [Publications] Keiichirou Kusakari: "On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique"The First International Workshop on Higher-Order Rewriting. HOR'02. 25 (2002)
• [Publications] Yoshihito Toyama: "Decision procedure for inductive theorems by rewriting induction,"Technical Report of IEICE COMP. 2002-45. 41-45 (2002)
• [Publications] 外山 芳人: "書き換え帰納法による帰納的定理の決定手続き"日本ソフトウェア科学会第19回大会論文集. 2002-9. 3A-2 (2002)
• [Publications] 鶴川敏孝: "変換パターンに基づく高階プログラム変換"信学技報COMP. 2002-83. 61-68 (2002)
• [Publications] 伊藤芳浩: "完備化手続きによるプログラム融合変換の停止条件"信学技報COMP. 2002-84. 69-76 (2002)