Heuristics for Proving Non-termination of Term Rewriting Systems

概要

論文の詳細を見る
A term rewriting system R is a program expressed as a finite set of rewrite rules, each of the form l→r, where l and r are terms constructed from function symbols and variables. The program is executed by rewriting ; that is, by repeatedly applying rewrite rules to some given initial term, using single-directional pattern matching and subterm replacement. We write s⇒t to indicate that the term s is rewritten to the term t by a single application of some rule in R. A derivation is a sequence of rewrites. A term rewriting system is terminating if there is no infinite derivation t_1⇒t_2⇒…. Otherwise, the system is non-terminating. Several methods of proving termination have been proposed. However, there are few that are useful for proving non-termination. It is known that the termination and the non-termination are undecidable properties. Therefore, the failure to prove termination does not imply the success in proving non-termination. The difficulty of proving non-termination is two-fold : 1. How can we effectively generate an infinite derivation? 2. How can we recognize the infiniteness of the derivation (from a finite part of it)? In this paper, we present some heuristics along these two lines.
一般社団法人情報処理学会の論文
1990-03-14