Abstract
We introduce the arctic matrix method for automatically proving termination of term rewriting. We use vectors and matrices over the arctic semi-ring: natural numbers extended with -∞,with the operations ”max” and ”plus”. This extends the matrix method for term rewriting and the arctic matrix method for string rewriting. In combination with the Dependency Pairs transformation, this allows for some conceptually simple termination proofs in cases where only much more involved proofs were known before. We further generalize to arctic numbers ”below zero”: integers extended with -∞.This allows to treat some termination problems with symbols that require a predecessor semantics. The contents of the paper has been formally verified in the Coq proof assistant and the formalization has been contributed to the CoLoR library of certified termination techniques. This allows formal verification of termination proofs using the arctic matrix method. We also report on experiments with an implementation of this method which, compared to results from 2007, outperforms TPA (winner of the certified termination competition for term rewriting), and in the string rewriting category is as powerful as Matchbox was but now all of the proofs are certified.
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
Amadio, R.M.: Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae 65(1-2), 29–60 (2005)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. TCS 236(1-2), 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Blanqui, F., Delobel, W., Coupet-Grimal, S., Hinderer, S., Koprowski, A.: CoLoR, a Coq library on rewriting and termination. In: WST (2006), http://color.loria.fr
Eén, N., Sörensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Endrullis, J.: Jambox, http://joerg.endrullis.de
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning (to appear, 2007)
Fuchs, L.: Partially Ordered Algebraic Systems. Addison-Wesley, Reading (1962)
Gaubert, S., Plus, M.: Methods and applications of (max, +) linear algebra. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 261–282. Springer, Heidelberg (1997)
Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation 34(1), 21–58 (2002)
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)
Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 443–459. Springer, Heidelberg (2007)
Golan, J.S.: Semirings and their Applications. Kluwer, Dordrecht (1999)
Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 185–198. Springer, Heidelberg (2004)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)
Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 167–177. Springer, Heidelberg (1989)
Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 328–342. Springer, Heidelberg (2006)
Koprowski, A.: TPA: Termination proved automatically. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 257–266. Springer, Heidelberg (2006), http://www.win.tue.nl/tpa
Koprowski, A., Zantema, H.: Certification of proving termination of term rewriting by matrix interpretations. In: SOFSEM. LNCS, vol. 4910, pp. 328–339 (2008)
Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 101–112. Springer, Heidelberg (1992)
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), http://dfa.imn.htwk-leipzig.de/matchbox
Waldmann, J.: Arctic termination. In: WST (2007)
Waldmann, J.: Weighted automata for proving termination of string rewriting. Journal of Automata, Languages and Combinatorics (to appear, 2007)
Zantema, H., Waldmann, J.: Termination by quasi-periodic interpretations. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 404–418. Springer, Heidelberg (2007)
The Coq proof assistant, http://coq.inria.fr
Termination competition, http://www.lri.fr/~marche/termination-competition
Termination problems data base, http://www.lri.fr/~marche/tpdb
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Koprowski, A., Waldmann, J. (2008). Arctic Termination ...Below Zero. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)