Polynomials for proving termination of context-sensitive rewriting

Abstract

We show how to generate well-founded and stable term orderings based on polynomial interpretations over the real numbers. Monotonicity (another usual requirement in termination proofs) can, then, be gradually introduced in the interpretations to deal with different applications. For instance, the dependency pairs method for proving termination of rewriting, and some restrictions of the rewrite relation which are not monotonie in all arguments of the function symbols, can benefit from this approach. The latter is the case for context-sensitive rewriting (CSR), a simple restriction of rewriting which has been proved useful for describing the semantics of several programming languages (e.g., Maude) and analyzing the properties of the corresponding programs. We show how to automatically generate polynomial interpretations over the real numbers for proving termination of CSR. Keywords: Programming languages, rewriting, termination. © Springer-Verlag 2004.