Abstract
In this paper, we present an approach to non-termination of term rewriting systems inspired by a technique that was designed in the context of logic programming. Our method is based on a classical unfolding operation together with semi-unification and is independent of a particular reduction strategy. We also describe a technique to reduce the explosion of rules caused by the unfolding process. The analyser that we have implemented is able to solve most of the non-terminating examples in the Termination Problem Data Base.
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
Alpuente, M., Falaschi, M., Manzo, F.: Analyses of unsatisfiability for equational logic programming. Journal of Logic Programming 311(1–3), 479–525 (1995)
Alpuente, M., Falaschi, M., Moreno, G., Vidal, G.: Safe folding/unfolding with conditional narrowing. In: Proc. of ALP/HOA 97, pp. 1–15 (1997)
Alpuente, M., Falaschi, M., Moreno, G., Vidal, G.: Rules + strategies for transforming lazy functional logic programs. Theoretical Computer Science 311(1–3), 479–525 (2004)
Alpuente, M., Falaschi, M., Ramis, M.J., Vidal, G.: Narrowing approximations as an optimization for equational logic programs. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714, pp. 391–409. Springer, Heidelberg (1993)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
F. Baader and T. Nipkow. Term rewriting and all that. Cambridge, 1998.
Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)
Chabin, J., Réty, P.: Narrowing directed by a graph of terms. In: Book, R.V. (ed.) Rewriting Techniques and Applications. LNCS, vol. 488, pp. 112–123. Springer, Heidelberg (1991)
Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41(1), 103–123 (1999)
Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation 3(1-2), 69–116 (1987)
Drosten, K.: Termersetzungssysteme: Grundlagen der Prototyp-Generierung algebraischer Spezifikationen. Springer, Berlin (1989)
Gabbrielli, M., Giacobazzi, R.: Goal independency and call patterns in the analysis of logic programs. In: Proc. of SAC’94, pp. 394–399. ACM Press, New York (1994)
Genaim, S., Codish, M.: Inferring termination conditions for logic programs using backwards analysis. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 685–694. Springer, Heidelberg (2001)
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.) Frontiers of Combining Systems. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)
Kapur, D., Musser, D., Narendran, P., Stillman, J.: Semi-unification. Theoretical Computer Science 81, 169–187 (1991)
Lankford, D.S., Musser, D.R.: A finite termination criterion. Unpublished Draft, USC Information Sciences Institute, Marina Del Rey, CA (1978)
Mesnard, F., Bagnara, R.: cTI: a constraint-based termination inference tool for iso-prolog. Theory and Practice of Logic Programming 5(1–2), 243–257 (2005)
Payet, É., Mesnard, F.: Non-termination inference for constraint logic programs. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 377–392. Springer, Heidelberg (2004)
Payet, E., Mesnard, F.: Non-termination inference of logic programs. ACM Transactions on Programming Languages and Systems 28(Issue 2), 256–289 (2006)
Pettorossi, A., Proietti, M.: Rules and strategies for transforming functional and logic programs. ACM Comput. Surv. 28(2), 360–414 (1996)
Steinbach, J.: Simplification orderings: history of results. Fundamenta Informaticae 24, 47–87 (1995)
Toyama, Y.: Counterexamples to the termination for the direct sum of term rewriting systems. Information Processing Letters 25(3), 141–143 (1987)
Termination Problem Data Base. http://www.lri.fr/~marche/termination-competition
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Payet, É. (2007). Detecting Non-termination of Term Rewriting Systems Using an Unfolding Operator. In: Puebla, G. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2006. Lecture Notes in Computer Science, vol 4407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71410-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-71410-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71409-5
Online ISBN: 978-3-540-71410-1
eBook Packages: Computer ScienceComputer Science (R0)