Improving the Context-Sensitive Dependency Graph

Abstract

[EN] 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.