Improving Context-Sensitive Dependency Pairs

Abstract Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a “ DP framework ” for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i. e. , we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

Authors

• Beatriz Alarcón
• Fabian Emmes
• Carsten Fuhs
• Jürgen Giesl
• Raúl Gutiérrez
• Salvador Lucas
• Peter Schneider-Kamp
• René Thiemann

Keywords

No keywords are indexed for this paper.