プログラムの合成・変換・検証に関する知識の説明に基づく学習とリフォーメーション

1994 Fiscal Year Annual Research Report

• Project/Area Number: 04650298
• Research Institution: Hokkaido University
• Principal Investigator: 栗原 正仁 北海道大学, 工学部, 助教授 (50133707)
• Keywords: 項書き換え系 / 完備化 / プログラム合成 / 変換 / リフォーメーション

Research Abstract

本研究は人工知能の分野で開発された「知識の説明に基づく学習」(EBL)の考え方を,ソフトウェア工学の問題領域である「プログラムの合成・変換・検証」に応用することを目的としている。過去2年間において検証と合成の部分について成果を上げてきている。本年度は本研究の最終年度であり,合成の部分の成果をさらに洗練化させるとともに,変換の部分に重点を置いて研究を進めた。その成果の概略を項目ごとに示す。
1.プログラムの合成に関してEBLの考え方を導入し,効率のよいシステムを構築した。本研究の枠組みである等式言語あるいは等式論理においては,プログラム合成は等式理論の完備化と呼ばれている。すなわち,完備化は等式で仕様記述された理論を入力されると,その理論を実現するプログラムを完備な項書換え系の形式で出力する。この研究においては,探索の過程でシステムが学習した知識を真偽維持システムで管理することにより,効率の良い完備化手続きを開発することができた。特に,本年度はこのシステムを推論規則として形式化し,通常のシステムとの関連のもとで,その健全性と完全性を証明した。
2.停止性を保存するプログラム変換を考察の対称として,EBLの考え方を利用した。与えられた項書換え系の停止性の証明が困難なとき,その停止性を保存したまま適切な系に変換することにより、もとの系の停止性を示そうというのがその動機である。本研究では合成可能(composable)な系の停止性について、混合系の非停止性を示す無限簡約列を純粋系の無限簡約列に変換する手法の一般化においてEBLの考え方が利用された。
3.3年間にわたる本研究成果の全体を総括し、知識のリフォーメーションという観点から、その発展の方向を検討した。

Research Products

• [Publications] 近藤 久: "複数の簡約順序のもとでの項書換えシステム完備化手続き" 電子情報通信学会論文誌. J78-D-I. 1-10 (1995)
• [Publications] 能登 正人: "Expert system for proving termination of rewrite rule programs by path orderings with extended status," Proc.IEEE Symposium on Emerging Technologies & Factory Automation. 142-147 (1994)
• [Publications] 栗原 正仁: "Termination of combination of composable term rewriting systems" Proc.7th Australian Joint Conference on Artificial Intelligence. 227-234 (1994)
• [Publications] 栗原 正仁: "Decomposable termination of composable term rewriting systems" IEICE Transactions on Information and Systems. E78-D(発表予定). (1995)
• [Publications] 栗原 正仁: "Completion for multiple reduction orderings" Proc.6th International Conference on Rewriting Techniques and Applications. (発表予定). (1995)
• [Publications] 栗原 正仁: "Modularity in noncopying term rewriting" Theoretical Computer Science. (発表予定). (1995)