Proving Termination in the Context-Sensitive Dependency Pair Framework

Authors

Raúl Gutiérrez and Salvador Lucas.

Abstract

Termination of context-sensitive rewriting (CSR) is an interesting problem with several applications in the fields of term rewriting and in the analysis of programming languages like CafeOBJ, Haskell, Maude, OBJ, etc. The dependency pairs approach, one of the most powerful techniques for proving termination of rewriting, has been adapted to be used for proving termination of CSR. The corresponding notion of context-sensitive dependency pair (CS-DP) is different from the standard one in that collapsing 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 powerful framework 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 powerful context-sensitive dependency pairs framework which fulfills all practical and theoretical expectations.

Publication

In Peter Ölveczky, editor,
Proc. of the 8th International Workshop on Rewriting Logic and its Applications, WRLA 2010,
LNCS 6381:19-35, Springer-Verlag, Berlin, 2010.