Raúl Gutiérrez

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

[download] 

Download in PDF format.

[BibTeX entry] 

@inproceedings{gl09b,
    author = {Guti\'errez, R. and Lucas, S.},
    title = {{Mechanizing Proofs of Termination 
              in the Context-Sensitive Dependency 
              Pair Framework}},
    booktitle = {Proc.\ of the 9th Spanish 
                 Conference on Programming and 
                 Languages, PROLE'09},
    editor = {Lucio, P. and Moreno, G. and 
              Pe\~na, R.},
    pages = {265--274},
    year = {2009}
 }