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

1996 Fiscal Year Annual Research Report

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

Research Abstract

高階書き換えシステムの基礎技術である停止性,合流性,計算戦略についての理論的解析を進めるとともに,高速書き替えシステムの実験を行い以下の知見を得た。
1.高階書き替えシステムの停止性を保証する新しい十分条件として,タイプ情報を重み付けに利用した改良再帰分解順序を提案し,その正当性を理論的に示した。
2.直和分解不可能な書き換えシステムのモジュラ解析は従来困難であった。このようなシステムのモジュラ解析をソ-ト情報にもとづいて行う新しい手法を開発した。
3.書き換えを効率的に行うためのリダクション戦略について検討し,従来知られていた正規化戦略の十分条件の拡張を行った。
4.高速書き換えシステムの実現法として,オ-マッチングオートマトンを組み込んだコンパイラを提案した。さらに、このコンパイラを実装し,従来の関改型プログラミング言語との速度比較を行い,本手法の有効性を明らかにした。

Research Products

• [Publications] M.Sakai: "Semantics and strong seguentiality of priority term rewriting systems" Lecture Notes in Comput. Sci.1103. 377-391 (1996)
• [Publications] 高橋宜孝: "条件付き項書き換え系の合流性について" 信学会論文誌. J79-D-1 No.11. 897-902 (1996)
• [Publications] 長谷崇: "重なりのある強遂次系のインデックス簡約について" 信学技報. COMP96-32. 39-48 (1996)
• [Publications] 青戸等人: "項書き換え系のパ-システント性の順序付ソ-トによる拡張" 信学技報. COMP96-31. 29-38 (1996)
• [Publications] 岩見宗弘: "高階項書換え系における改良再帰分解順序について" 信学技報. COMP96-73. 17-24 (1996)