Improving the context-sensitive dependency graph
Authors
Beatriz Alarcón, Raúl Gutiérrez, and Salvador Lucas
Abstract
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.
Keywords
Dependency pairs, term rewriting,
program analysis, termination.