Abstract
Restrictions of rewriting can eventually achieve termination by pruning all infinite rewrite sequences issued from every term. Context-sensitive rewriting (CSR) is an example of such a restriction. In CSR, the replacements in some arguments of the function symbols are permanently forbidden. This paper describes mu-term, a tool which can be used to automatically prove termination of CSR. The tool implements the generation of the appropriate orderings for proving termination of CSR by means of polynomial interpretations over the rational numbers. In fact, mu-term is the first termination tool which generates term orderings based on such polynomial interpretations. These orderings can also be used, in a number of different ways, for proving termination of ordinary rewriting. Proofs of termination of CSR are also possible via existing transformations to TRSs (without any replacement restriction) which are also implemented in mu-term.
Work partially supported by MCYT project STREAM TIC2001-2705-C03-01, MCyT Acción Integrada HU 2003-0003 and Agencia Valenciana de Ciencia y Tecnología GR03/025.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
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)
Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical report, AIB-2001-09, RWTH Aachen, Germany (2001)
Borralleras, C., Lucas, S., Rubio, A.: Recursive Path Orderings can be Context- Sensitive. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 314–331. Springer, Heidelberg (2002)
Borralleras, C.: Ordering-based methods for proving termination automatically. PhD Thesis, Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya (May 2003)
Ferreira, M.C.F., Ribeiro, A.L.: Context-sensitive AC-rewriting. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 286–300. Springer, Heidelberg (1999)
Gramlich, B., Lucas, S.: Modular termination of context-sensitive rewriting. In: Proc. of PPDP 2002, pp. 50–61. ACM Press, New York (2002)
Gramlich, B., Lucas, S.: Simple termination of context-sensitive rewriting. In: Proc. of RULE 2002, pp. 29–41. ACM Press, New York (2002)
Giesl, J., Middeldorp, A.: Termination of Innermost Context-Sensitive Rewriting. In: Ito, M., Toyama, M. (eds.) DLT 2002. LNCS, vol. 2450, pp. 231–244. Springer, Heidelberg (2003)
Giesl, J., Middeldorp, A.: Transformation Techniques for Context-Sensitive Rewrite Systems. In: Journal of Functional Programming (2004) (to appear)
Lucas, S.: Termination of context-sensitive rewriting by rewriting. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 122–133. Springer, Heidelberg (1996)
Lucas, S.: Termination of Rewriting With Strategy Annotations. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 669–684. Springer, Heidelberg (2001)
Lucas, S.: Context-sensitive rewriting strategies. Information and Computation 178(1), 293–343 (2002)
Lucas, S.: Lazy Rewriting and Context-Sensitive Rewriting. Electronic Notes in Theoretical Computer Science, vol. 64. Elsevier Sciences, Amsterdam (2002)
Lucas, S.: Polynomials for proving termination of context-sensitive rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 318–332. Springer, Heidelberg (2004)
Steinbach, J.: Generating Polynomial Orderings. Information Processing Letters 49, 85–93 (1994)
Zantema, H.: Termination of Context-Sensitive Rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 172–186. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lucas, S. (2004). mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive