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

1995 Fiscal Year Annual Research Report

• Project/Area Number: 07680347
• Research Category: Grant-in-Aid for General 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.高階書き換えシステムの計算結果の存在保証を行うために,従来知られていた再帰経路順序よりも強力な再帰分解順序による停止条件を明らかにできた。

Research Products

• [Publications] 酒井正彦,外山芳人: "優先順位付き項書き換え系の意味論とその強逐次性" 信学技報. SS95-40. 31-38 (1996)
• [Publications] 草刈圭一朗,酒井正彦,外山芳人: "非線形項書き換え系の合流性について" 信学技報. COMP95‐86. 123-129 (1996)
• [Publications] 岩見宗弘,酒井正彦,外山芳人: "高階項書き換え系の停止性について" 信学技報. COMP95‐85. 113-121 (1996)
• [Publications] T.Nagaya,M.Sakai,Y.Toyama: "NVNF‐sequentiality of Left‐linear Term Rewriting Systems" 数理解析研究所講究録. 918. 109-117 (1995)
• [Publications] Y.Toyama,M.Oyamaguchi: "Church‐Rosser Property and Unique Normal Form Property of Non‐Duplicating Term Rewriting Systems" 数理解析研究所講究録. 918. 139-149 (1995)