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

2001 Fiscal Year Annual Research Report

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

Research Abstract

関数型言語MLによるプログラムを対象として、完備化に基づくプログラム融合変換の実験を計算機上で行ない、その動作確認を行うとともに、その変換能力の拡張を試みた。また、融合変換を書き換えシステムの等価変換手続きとしてモデル化し、その動作原理の理論的な解明を進めた。
(1)完備化による変換例の収集
完備化による融合変換能力を調査するための基礎データとして、計算機上の実験による融合変換の成功例・失敗例の収集を進めた。実験方法は次の通りである。
(i)MLプログラムPからP'への融合変換例を文献等から収集
(ii)Pに対応する項書き換えシステムRを構成
(iii)Rに対して完備化手続きを適用して完備な項書き換えシステムR'に自動変換
(iv)得られたR'とP'を比較して完備化による融合変換が成功か否かを判定
さらに、変換が失敗した場合には、どのような補題を追加すれば変換が成功するかの実験も合わせて行った。なお、実験対象としたプログラムは、自然数上の関数、リスト処理関数、ブール関数などである。以上の実験を通して当初予定していた基礎データを収集することができた。
(2)融合変換の成功条件の解析
関数型プログラムの融合変換手続きが必ず成功するための条件に関しては、Wadler(1988)、Chin(1994)、Seidl(1994)、Seidl-Sorensen(1998)らの研究が知られている。しかし、評価メカニズムの違いから、これらの成功条件をそのまま項書き換えシステムに適用することは困難である。そこで、項書き換えシステムに基づいた融合変換手続きの形式的モデルを作成し、融合変換手続きの停止条件に焦点を絞った解析を進めた。その結果、変換途中で生成される項の正規形の個数が高々有限となるための条件と、融合変換手続きの停止条件は密接に関係していることが明らかになった。

Research Products

• [Publications] Yoshihito Toyama: "Equational proofs by Completion"Journal of Japanese Society for Artificial Intelligence. 16・5. 668-674 (2001)
• [Publications] Keiichirou Kusakari: "On Proving Termination of Term Rewriting Systems with Higher-Order Variables"IPSJ Transactions on Programming. 42・SIG7. 35-45 (2001)
• [Publications] Keiichirou Kusakari: "On Proving AC-Dependency Paris"IEICE Transactions on Information and systems. E84D・5. 604-612 (2001)
• [Publications] Yoshihito Toyama: "Church-Rosser Property and Unique Normal Form Property of Non-Duplicating Term Rewriting Systems"IEICE Transactions on Information and systems. E84-D・4. 439-447 (2001)