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 \({\textsf{T\kern-0.2em\raisebox{-0.3em}T\kern-0.2emT\kern-0.2em\raisebox{-0.3em}2}}\).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Endrullis, J.: Jambox, http://joerg.endrullis.de
Giesl, J., Middeldorp, A.: Transformation techniques for context-sensitive rewrite systems. Journal of Functional Programming 14(4), 379–427 (2004)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the DP framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated termination analysis for Haskell: From term rewriting to programming languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 297–312. Springer, Heidelberg (2006)
Guttag, J., Kapur, D., Musser, D.: On proving uniform termination and restricted termination of rewriting systems. SIAM J. Computation 12, 189–214 (1983)
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. springer, Heidelberg (2009)
Kurth, W.: Termination und Konfluenz von Semi-Thue-Systemen mit nur einer Regel. PhD thesis, Technische Universität Clausthal, Germany (1990)
Lankford, D., Musser, D.: A finite termination criterion. Unpublished Draft. USC Information Sciences Institute (1978)
Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming 1, 1–61 (1998)
Payet, É.: Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science 403(2-3), 307–327 (2008)
Raffelsieper, M., Zantema, H.: A transformational approach to prove outermost termination automatically. In: Proc. WRS 2008. ENTCS 237, pp. 3–21 (2009)
Thiemann, R.: From outermost termination to innermost termination. In: Nielsen, M., et al. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 533–545. Springer, Heidelberg (2009)
Thiemann, R., Giesl, J., Schneider-Kamp, P.: Deciding innermost loops. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 366–380. Springer, Heidelberg (2008)
Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004)
Zantema, H.: Termination of string rewriting proved automatically. Journal of Automated Reasoning 34, 105–139 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thiemann, R., Sternagel, C. (2009). Loops under Strategies. In: Treinen, R. (eds) Rewriting Techniques and Applications. RTA 2009. Lecture Notes in Computer Science, vol 5595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02348-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-02348-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02347-7
Online ISBN: 978-3-642-02348-4
eBook Packages: Computer ScienceComputer Science (R0)