Sciweavers

Share
FOSSACS
2004
Springer

Polynomials for Proving Termination of Context-Sensitive Rewriting

10 years 2 months ago
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 monotonic 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.
Salvador Lucas
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where FOSSACS
Authors Salvador Lucas
Comments (0)
books