Sciweavers

Share
FROCOS
2007
Springer

Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs

8 years 9 months ago
Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
Abstract. Innermost context-sensitive rewriting has been proved useful for modeling computations of programs of algebraic languages like Maude, OBJ, etc. Furthermore, innermost termination of rewriting is often easier to prove than termination. Thus, under appropriate conditions, a useful strategy for proving termination of rewriting is trying to prove termination of innermost rewriting. This phenomenon has also been investigated for context-sensitive rewriting (CSR). Up to now, only few transformations have been proposed and used to prove termination of innermost CSR. In this paper, we investigate direct methods for proving termination of innermost CSR. We adapt the recently introduced context-sensitive dependency pairs approach to innermost CSR and show that they can be advantageously used for proving termination of innermost CSR. We have implemented them as part of the termination tool mu-term.
Beatriz Alarcón, Salvador Lucas
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FROCOS
Authors Beatriz Alarcón, Salvador Lucas
Comments (0)
books