Article ID Journal Published Year Pages File Type
426696 Information and Computation 2007 23 Pages PDF
Abstract

We present a new method for automatically proving termination of left-linear term rewriting systems on a given regular language of terms. It is a generalization of the match bound method for string rewriting. To prove that a term rewriting system terminates we first construct an enriched system over a new signature that simulates the original derivations. The enriched system is an infinite system over an infinite signature, but it is locally terminating: every restriction of the enriched system to a finite signature is terminating. We then construct iteratively a finite tree automaton that accepts the enriched given regular language and is closed under rewriting modulo the enriched system. If this procedure stops, then the enriched system is compact: every enriched derivation involves only a finite signature. Therefore, the original system terminates. We present two methods to construct the enrichment: roof heights for left-linear systems, and match heights for linear systems. For linear systems, the method is strengthened further by a forward closure construction. Using these methods, we give examples for automated termination proofs that cannot be obtained by standard methods.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics