依存対に基づく高階項書換え系の停止性証明

スポンサーリンク

概要

論文の詳細を見る
一般に停止性問題は決定不可能であるため、停止性を保証する十分条件が研究されている。近年、項書換え系(Term Rewriting Systems, TRS)の停止性に関してArtsとGieslにより依存対を用いた停止性判定手法が提案された。しかし、この手法を高階項書換え系(Higher Order Rewriting System, HRS)に直接用いることはできない。なぜなら、高階項は一階項と違い、自由変数に関数を代入することできるため、β変換が起きて項が複雑に変化する可能性があるからである。本稿では、依存対を用いた手法をHRSに適用した場合の問題点を考察し、HRS上の依存対、依存対列を新たに定義する。また、HRSにおける依存対列と停止性の関係を明らかにし、HRSの停止性を判定する新しい手法を提案する。
社団法人電子情報通信学会の論文
1998-03-24

著者

関連論文

もっと見る

スポンサーリンク