Abstract
We propose two transformations on term rewrite systems (TRSs) based on reducing right-hand sides: one related to the transformation order and a variant of dummy elimination. Under mild conditions we prove that the transformed system is terminating if and only if the original one is terminating. Both transformations are very easy to implement, and make it much easier to prove termination of some TRSs automatically.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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 University Press, Cambridge (1998)
Bellegarde, F., Lescanne, P.: Termination by completion. Applicable Algebra in Engineering, Communication and Computing 1(2), 79–96 (1990)
Ben-Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming 9, 137–159 (1987)
Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17, 279–301 (1982)
Giesl, J., et al.: AProVE: Automated program verification environment., http://aprove.informatik.rwth-aachen.de/
Ferreira, M.: Termination of Term Rewriting – Well-Foundedness, Totality, and Transformations. PhD thesis, University of Utrecht (1995)
Ferreira, M., Zantema, H.: Dummy elimination: Making termination easier. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 243–252. Springer, Heidelberg (1995)
Ferreira, M.C.F.: Dummy elimination in equational rewriting. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 63–77. Springer, Heidelberg (1996)
Giesl, J., Middeldorp, A.: Eliminating dummy elimination. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 309–323. Springer, Heidelberg (2000)
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, vol. 3452, pp. 301–331. Springer, Heidelberg (2005)
Gramlich, B.: Simplifying termination proofs for rewrite systems by preprocessing. In: Gabrielli, M., Pfenning, F. (eds.) Proceedings of the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP), Montreal, Canada, September 2000, pp. 139–150. ACM Press, New York (2000)
Hirokawa, N., Middeldorp, A.: TTT: Tyrolean termination tool, http://cl2-informatik.uibk.ac.at/ttt/
Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004)
Koprowski, A.: TPA: Termination proved automatically, http://www.win.tue.nl/tpa
Middeldorp, A., Ohsaki, H., Zantema, H.: Transforming termination by self-labelling. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 373–386. Springer, Heidelberg (1996)
Steinbach, J.: Automatic termination proofs with transformation orderings. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 11–25. Springer, Heidelberg (1995)
Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)
Thiemann, R., Zantema, H., Giesl, J., Schneider-Kamp, P.: Adding constants to string rewriting. Technical report, RWTH Aachen (2005), To appear, available via, http://www-i2.informatik.rwth-aachen.de/AProVE/ConstantsSRS.pdf
TPDB. Termination problem data base, http://www.lri.fr/~marche/tpdb/
Zantema, H.: TORPA: Termination of rewriting proved automatically, http://www.win.tue.nl/~hzantema/torpa.html
Zantema, H.: Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation 17, 23–50 (1994)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)
Zantema, H.: Termination. In: Term Rewriting Systems, by Terese, pp. 181–259. Cambridge University Press, Cambridge (2003)
Zantema, H.: Termination of string rewriting proved automatically. Technical Report CS-report 03-14, Eindhoven University of Technology (2003), Available via, http://www.win.tue.nl/inf/onderzoek/en_index.html
Zantema, H.: TORPA: termination of rewriting proved automatically. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 95–104. Springer, Heidelberg (2004)
Zantema, H.: Termination of string rewriting proved automatically. Journal of Automated Reasoning (2005) (Accepted for publication)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Zantema, H. (2005). Reducing Right-Hand Sides for Termination. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds) Processes, Terms and Cycles: Steps on the Road to Infinity. Lecture Notes in Computer Science, vol 3838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11601548_12
Download citation
DOI: https://doi.org/10.1007/11601548_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30911-6
Online ISBN: 978-3-540-32425-6
eBook Packages: Computer ScienceComputer Science (R0)