高階書き換えシステムをもちいたプログラム検証法の研究

1997 Fiscal Year Annual Research Report

• Project/Area Number: 07680347
• Research Institution: Japan Advanced Institute of Science and Technology, Hokuriku
• Principal Investigator: 外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
• Co-Investigator(Kenkyū-buntansha): 酒井 正彦 名古屋大学, 大学院・工学研究科, 助教授 (50215597)
• Keywords: 項書き換えシステム / 高階書き換えシステム / 合流性 / 停止性 / リダクション

Research Abstract

高階書き換えシステムの基礎技術である停止性,合流性,計算戦略についての理論的解析を進めるとともに,プログラムの等価変換法と書き換えシステムによる自動証明法の実験を行ない,以下の成果を得た。
1。高階書き換えシステムの停止性を保証する条件として,改良再帰分解順序を解析し,適用可能な条件を明らかにした。これは従来の停止条件の拡張となっている。
2。型情報を利用した停止性,合流性の判定手法として永続性にもとづく解析手法を開発した。この手法はモジュラ解析が困難なシステムにも適用可能である。
3。書き換え規則に重なりがある場合の計算機戦略について解析し,効率的な書き換え方法について提案した。また,この方法が決定可能であることを明らかにした。
4。プログラムの新しい等価変換手法を提案し,計算機上で変換システムの実験を行い,その有効性を確認した。
5。書き換え手法にもとづく帰納的定理証明法として,書き換え帰納法の解析を行うとともに,潜在帰納法との比較評価を行った。
6。依存対を利用した停止性の証明手法の実装を行い,実験を通して有効性を確認した。また、結合律・可換律を含むシステムの停止性の証明も可能となるように拡張を行った。

Research Products

• [Publications] T.Aoto: "On Composable properties of term rewriting systems" Lecture Notes in Comput.Sci.1298. 114-128 (1997)
• [Publications] T.Aoto: "Persistency of Confluence" Journal of Universal Comput.Sci.3.11. 1134-1148 (1997)
• [Publications] T.Aoto: "Tree lifting orderings for termimation trans formation of term rewriting systems" Proc.of LA symposium(1997-07). 109-114 (1997)
• [Publications] 岩見宗弘: "項書換え系の停止性の順序ソ-トに関する永続性について" ソフトウエア科学会第14回大会論文集. 357-360 (1997)
• [Publications] 草刈圭一郎: "項書換え系の停止性自動証明法の提案" ソフトウエア科学会第14回大会論文集. 361-364 (1997)
• [Publications] 佐賀正芳: "リスト生成法に基づくプログラム変換" 電気関係学会北陸支部連合大会予稿集(1997). 287-287 (1997)