Mechanizing Proofs of Termination in the Context-Sensitive Dependency Pairs Framework
Authors
Raúl Gutiérrez and Salvador Lucas
Abstract
The dependency pairs approach, one of the most powerful techniques
for proving termination of rewriting, has been recently adapted to
be used for proving termination of context-sensitive rewriting
(CSR). The notion of context-sensitive dependency pair (CS-DP) is
different from the standard one in that collapsing dependency pairs
(i.e., rules whose right-hand side is a variable) are
considered. Although the implementation and practical use of CS-DPs
leads to a very powerful framework which improves the current
state-of-the-art of methods for proving termination of CSR,
handling collapsing pairs is not easy and often leads to impose
heavy requirements over the base orderings which are used to achieve
the proofs. A recent proposal removes collapsing pairs by
transforming them into sets of new (standard) pairs. In this way,
though, the complexity of the obtained dependency graph is heavily
increased and the role of collapsing pairs for modeling
context-sensitive computations gets lost. This leads to a less
intuitive and accurate description of the termination behavior of
the system.
In this paper, we show how to get the best of the two approaches,
thus obtaining a more powerful dependency pair framework which
hopefully fulfills all practical and theoretical expectations.
Keywords
Context-sensitive rewriting, termination, dependency pairs.