×
Zantema, H.

Termination of string rewriting proved automatically. (English) Zbl 1102.68649

J. Autom. Reasoning 34, No. 2, 105-139 (2005).
Summary: This paper describes how a combination of polynomial interpretations, recursive path order, RFC match-bounds, the dependency pair method, and semantic labelling can be used for automatically proving termination of an extensive class of String Rewriting Systems (SRSs). The tool implementing this combination of techniques is called TORPA: Termination of Rewriting Proved Automatically. All termination proofs generated by TORPA are easy to read and check; but for many of the SRSs involved, finding a termination proof would be a hard job for a human. This paper contains all underlying theory, describes how the search for a termination proof is implemented, and includes many examples.

Cited in 16 Documents

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q42 Grammars and rewriting systems

Keywords:

string rewriting; termination; semantic labelling; relative termination; match-bounds

Software:

TORPA; Matchbox; CiME; Tsukuba; AProVE; REVE
Cite Review PDF
Full Text: DOI

References:

[1] Arts, T. and Giesl, J.: Termination of term rewriting using dependency pairs, Theoret. Comput. Sci. 236 (2000), 133–178. · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8
[2] Ben-Cherifa, A. and Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation, Sci. Comput. Programming 9 (1987), 137–159. · Zbl 0625.68036 · doi:10.1016/0167-6423(87)90030-X
[3] Contejean, E., Marché, C., Monate, B. and Urbain, X.: The CiME rewrite tool, available at http://cime.lri.fr/.
[4] Dershowitz, N.: Termination of linear rewriting systems, in S. Even and O. Kariv (eds.), Proc. of the 8th Internat. Coll. on Automata, Languages and Programming (ICALP-81), Lecture Notes in Comput. Sci. 115, Springer, Berlin, 1981, pp. 448–458. · Zbl 0465.68009
[5] Dershowitz, N.: Orderings for term-rewriting systems, Theoret. Comput. Sci. 17 (1982), 279–301. · Zbl 0525.68054 · doi:10.1016/0304-3975(82)90026-3
[6] Geser, A.: Relative termination, PhD Thesis, Universität Passau, Germany, 1990.
[7] Geser, A., Hofbauer, D. and Waldmann, J.: Match-bounded string rewriting systems, in B. Rovan and P. Vojtas (eds.), Proc. of the 28th Internat. Symp. on Mathematical Foundations of Computer Science (MFCS-03), Lecture Notes in Comput. Sci. 2747, Springer, Berlin, 2003, pp. 449–459. Extended version accepted for publication in Appl. Algebra Engrg. Comm. Comput. · Zbl 1124.68378
[8] Geser, A., Hofbauer, D. and Waldmann, J.: Deciding termination for ancestor match-bounded string rewriting systems, Nia Technical Report, National Institute of Aerospace, Hampton, VA, 2004; available at research.nianet.org/\(\sim\)geser/papers/nia-ancestors.html. · Zbl 1101.68048
[9] Geser, A., Hofbauer, D., Waldmann, J. and Zantema, H.: Finding finite automata that certify termination of string rewriting, in K. Salomaa and S. Yu (eds.), Proc. of Ninth Internat. Conf. on Implementation and Application of Automata (CIAA04), Lecture Notes in Comput. Sci., Springer, Berlin, 2004. · Zbl 1115.68433
[10] Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S.: Automated termination proofs with AProVE, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 210–220; tool available at http://www-i2.informatik.rwth-aachen.de/AProVE/.
[11] Giesl, J. and Zantema, H.: Liveness in rewriting, in R. Nieuwenhuis (ed.), Proc. of the 14th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 2706, Springer, Berlin, 2003, pp. 321–336. · Zbl 1038.68067
[12] Hirokawa, N. and Middeldorp, A.: Tsukuba termination tool, in R. Nieuwenhuis (ed.), Proc. of the 14th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 2706, Springer, Berlin, 2003, pp. 311–320. · Zbl 1038.68561
[13] Hirokawa, N. and Middeldorp, A.: Dependency pairs revisited, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 249–268. · Zbl 1187.68275
[14] Krishnamoorthy, M. S. and Narendran, P.: On recursive path ordering, Theoret. Comput. Sci. 40 (1985), 323–328. · Zbl 0602.68031 · doi:10.1016/0304-3975(85)90175-6
[15] Kurth, W.: Termination und Konfluenz von Semi-Thue-Systemen mit nur einer Regel, PhD Thesis, Technische Universität Clausthal, Germany, 1990. · Zbl 0719.03019
[16] Lagarias, J. C.: The 3n+1 problem and its generalizations, Amer. Math. Monthly 92 (1985), 3–23. · Zbl 0566.10007 · doi:10.2307/2322189
[17] Lankford, D. S.: On proving term rewriting systems are noetherian, Technical Report MTP 3, Louisiana Technical University, 1979.
[18] Manna, Z. and Ness, S.: On the termination of Markov algorithms, in Proc. of the Third Hawaii Internat. Conf. on System Science, Honolulu, HI, 1970, pp. 789–792.
[19] Vardi, I.: Computational Recreations in Mathematica, Addison-Wesley, Reading, MA, 1991. · Zbl 0786.11002
[20] Waldmann, J.: Matchbox: A tool for match-bounded string rewriting, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 85–94.
[21] Zantema, H.: Termination of term rewriting: Interpretation and type elimination, J. Symbolic Comput. 17 (1994), 23–50. · Zbl 0810.68087 · doi:10.1006/jsco.1994.1003
[22] Zantema, H.: Termination of term rewriting by semantic labelling, Fundamenta Informaticae 24 (1995), 89–105. · Zbl 0839.68050
[23] Zantema, H.: Termination, in: Term Rewriting Systems, by Terese, Cambridge Univ. Press, Cambridge, 2003, pp. 181–259.
[24] 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. · Zbl 1102.68649
[25] Zantema, H.: TORPA: Termination of rewriting proved automatically, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 95–104.
[26] Zantema, H. and Geser, A.: Non-looping string rewriting, Theoret. Informatics Appl. 33 (1999), 279–301. · Zbl 0951.68054 · doi:10.1051/ita:1999118
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.