Improving the Context-sensitive Dependency Graph

9 years 10 months ago
Improving the Context-sensitive Dependency Graph
The dependency pairs method is one of the most powerful technique for proving termination of rewriting and it is currently central in most automatic termination provers. Recently, it has been adapted to be used in proofs of termination of context-sensitive rewriting. The use of collapsing dependency pairs i.e., having a single variable in the right-hand side is a novel and essential feature to obtain a correct framework in this setting. Unfortunately, dependency pairs behave as a kind of glue in the context-sensitive dependency graph which makes the cycles bigger, thus making some proofs of termination harder. In this paper we show that this effect can be safely mitigated by removing some arcs from the graph, thus leading to faster and easier proofs. Narrowing dependency pairs is also introduced and used here to eventually simplify the treatment of the context-sensitive dependency graph. We show the practicality of the new techniques with some benchmarks.
Beatriz Alarcón, Raúl Gutiérr
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Beatriz Alarcón, Raúl Gutiérrez, Salvador Lucas
Comments (0)