cl-banner

Loops under Strategies

René Thiemann and Christian Sternagel

Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 17 – 31, 2009.

Abstract

Most techniques to automatically disprove termination of term rewrite systems search for a loop. Whereas a loop implies non-termination for full rewriting, this is not necessarily the case if one considers rewriting under strategies. Therefore, in this paper we first generalize the notion of a loop to a loop under a given strategy. In a second step we present two novel decision procedures to check whether a given loop is a context-sensitive or an outermost loop. We implemented and successfully evaluated our method in the termination prover TTT2.

 

  PDF |    doi:10.1007/978-3-642-02348-4_2  |  © Springer

BibTeX 

@inproceedings{RTCS-RTA09,
author = "Ren{\'e} Thiemann and Christian Sternagel",
title = "Loops under Strategies",
booktitle = "Proceedings of the 20th International Conference on Rewriting
Techniques and Applications",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
volume = 5595,
pages = "17--31",
year = 2009
}
Nach oben scrollen