Abstract
We present the first method to disprove innermost termination of term rewrite systems automatically. To this end, we first develop a suitable notion of an innermost loop. Second, we show how to detect innermost loops: One can start with any technique amenable to find loops. Then our novel procedure can be applied to decide whether a given loop is an innermost loop. We implemented and successfully evaluated our method in the termination prover AProVE.
Supported by the Deutsche Forschungsgemeinschaft (DFG) under grant GI 274/5-2.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge (1998)
Dershowitz, N.: Termination of rewriting. J. Symb. Comp. 3, 69–116 (1987)
Diekert, V.: Makanin’s algorithm. In: Lothaire, M. (ed.) Combinatorics on Words, pp. 387–442. Cambridge University Press, Cambridge (2002)
Endrullis, J.: Jambox, http://joerg.endrullis.de
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)
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 (LNAI), 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)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)
Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae 24, 3–23 (1995)
Guttag, J., Kapur, D., Musser, D.: On proving uniform termination and restricted termination of rewriting systems. SIAM J. Computation 12, 189–214 (1983)
Hermann, M., Galbavý, R.: Unification of infinite sets of terms schematized by primal grammars. Theoretical Computer Science 176(1-2), 111–158 (1997)
Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)
Kruskal, J.B.: Well-quasi-orderings, the Tree Theorem, and Vazsonyi’s conjecture. Transactions of the American Mathematical Society 95, 210–223 (1960)
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)
Marché, C., Zantema, H.: The termination competition. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 303–313. Springer, Heidelberg (2007)
Payet, É.: Detecting non-termination of term rewriting systems using an unfolding operator. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 194–209. Springer, Heidelberg (2007)
Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD thesis, RWTH Aachen University. Technical Report AIB-2007-17 (2007), http://aib.informatik.rwth-aachen.de/2007/2007-17.pdf
Vroon, D.: Personal communication (2007)
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)
Zhang, X.: Overlap closures do not suffice for termination of general term rewriting systems. Information Processing Letters 37(1), 9–11 (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thiemann, R., Giesl, J., Schneider-Kamp, P. (2008). Deciding Innermost Loops. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)