Abstract
The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. We extend their work to non-left-linear rewrite systems. The key to this extension is the introduction of so-called raise rules and the use of tree automata that are not quite deterministic. Furthermore, we present negative solutions to two open problems related to string rewrite systems.
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.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2002), Available at, www.grappa.univ-lille3.fr/tata
Dershowitz, N.: Termination of linear rewriting systems (preliminary version). In: Even, S., Kariv, O. (eds.) Automata, Languages and Programming. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981)
Endrullis, J.: Jambox: Automated termination proofs for string/term rewriting (2006), Available from http://joerg.endrullis.de/
Endrullis, J., Hofbauer, D., Waldmann, J.: Decomposing terminating rewrite relations. In: Proc. 8th WST, pp. 39–43 (2006)
Genet, T.: Decidable approximations of sets of descendants and sets of normal forms. In: Nipkow, T. (ed.) Proc. 9th RTA. LNCS, vol. 1379, pp. 151–165. Springer, Heidelberg (1998)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. AAECC 15(3-4), 149–171 (2004)
Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. JAR 34(4), 365–385 (2005)
Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: Finding finite automata that certify termination of string rewriting systems. IJFCS 16(3), 471–486 (2005)
Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: On tree automata that certify termination of left-linear term rewriting systems. I&C 205(4), 512–534 (2007)
Geupel, O.: Overlap closures and termination of term rewriting systems. Report MIP-8922, Universität Passau (1989)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Huet, G., Lankford, D.S.: On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA (1978)
Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 593–610. Springer, Heidelberg (2001)
Nagaya, T., Toyama, Y.: Decidability for left-linear growing term rewriting systems. I&C 178(2), 499–514 (2002)
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 rewriting proved automatically. JAR 34, 105–139 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Korp, M., Middeldorp, A. (2007). Proving Termination of Rewrite Systems Using Bounds. In: Baader, F. (eds) Term Rewriting and Applications. RTA 2007. Lecture Notes in Computer Science, vol 4533. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73449-9_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-73449-9_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73447-5
Online ISBN: 978-3-540-73449-9
eBook Packages: Computer ScienceComputer Science (R0)