On Proving Uniform Termination and Restricted Termination of Rewriting Systems
John V. Guttag, Deepak Kapur, David R. Musser · SIAM Journal on Computing · 1983
In mechanical theorem proving, particularly in proving properties of algebraically specified data types, we frequently need a decision procedure for the theory of a given finite set of equations (axioms). A general approach to this problem is to try to derive from the axioms a set of rewrite rules that are “canonical,” i.e., they rewrite to a canonical form all terms that are equal (according the axioms and the equivalence and substitution properties of equality). Rewrite rules are canonical if and only if they determine a relation that is both confluent and uniformly terminating. The difficulty of proving uniform termination has been the major drawback of the rewrite rule approach to deciding equations. A new method of proving uniform termination is proposed. Assuming that the rewriting relation is globally finite (for any term there are only finitely many terms to which it can be rewritten), nontermination can occur only if there are cycles. Uniform termination is proved by showing that no cycles can occur. A method related to the Knuth and Bendix method of proving confluence is developed and used as the basis of such proof. In most cases, the proposed method will only prove termination for terms up to a certain size; this kind of “restricted termination” has a number of applications.