Movatterモバイル変換

[0]ホーム
URL:

Skip to main content
Springer Nature Link
Log in

Matrix Interpretations for Proving Termination of Term Rewriting

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows us to prove termination and relative termination. A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.

This is a preview of subscription content,log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+
from ¥17,985 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

References

  1. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comp. Sci.236, 133–178 (2000)

    Article MATH MathSciNet  Google Scholar 

  2. Termination problems data base.http://www.lri.fr/~marche/tpdb/

  3. Termination competition.http://www.lri.fr/~marche/termination-competition/

  4. Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) Proc. 8th Int. Coll. on Automata, Languages and Programming (ICALP-81). Lecture Notes in Computer Science, vol. 115, pp. 448–458. Springer (1981)

  5. Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) Proc. 8th Int. Conf. Theory and Applications of Satisfiability Testing SAT 2005. Lecture Notes in Computer Science, vol. 3569, pp. 61–75. Springer (2005). Tool:http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

  6. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR ’06). Lecture Notes in Computer Science, vol. 4130, pp. 574–588. Springer (2006)

  7. Giesl, J., Schneider-Kamp, P., Thiemann, R.: Aprove 1.2: automatic termination proofs in the dependency pair framework. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR ’06). Lecture Notes in Computer Science, vol. 4130, pp. 281– 286. Springer (2006)

  8. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004). Lecture Notes in Computer Science, vol. 3452, pp. 301–331. Springer (2005)

  9. Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) Proceedings of the 15th Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, vol. 3091, pp. 249–268. Springer (2004)

  10. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Inf. Comput.199, 172–199 (2005)

    Article MATH MathSciNet  Google Scholar 

  11. Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Giesl, J. (ed.) Proceedings of the 16th Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, vol. 3467, pp. 175–184. Springer (2005)

  12. Hirokawa, N., Middeldorp, A.: Uncurrying for termination. In: Proceedings of 3rd International Workshop on Higher-Order Rewriting (HOR), pp. 19–24. (2006)

  13. Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations (preliminary version). In: Dershowitz, N. (ed.) Proceedings of the 3rd Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, vol. 355, pp, 167–177. Springer (1989)

  14. Hofbauer, D., Waldmann, J.: Proving termination with matrix interpretations. In: Pfenning, F. (ed.) Proceedings of the 17th Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, vol. 4098, pp. 328–342. Springer (2006)

  15. Hofbauer, D., Waldmann, J.: Termination of {aa→bc,bb→ac,cc→ab}. Inf. Process. Lett.98(4), 156–158 (2006)

    Article MathSciNet  Google Scholar 

  16. The RTA list of open problems.http://www.lsv.ens-cachan.fr/rtaloop/

  17. Full results of Jambox.http://joerg.endrullis.de/jar07/

  18. Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput.17, 23–50 (1994)

    Article MATH MathSciNet  Google Scholar 

  19. Zantema, H.: Termination. In: Term Rewriting Systems, by Terese, pp. 181–259. Cambridge University Press (2003)

  20. Zantema, H.: 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: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 3838, pp. 173–197. Springer (2005)

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Vrije Universiteit Amsterdam, De Boelelaan 1081, 1081 HV, Amsterdam, The Netherlands

    Jörg Endrullis

  2. Hochschule für Technik, Wirtschaft und Kultur (FH) Leipzig, Fb IMN, PF 30 11 66, 04251, Leipzig, Germany

    Johannes Waldmann

  3. Department of Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Hans Zantema

Authors
  1. Jörg Endrullis
  2. Johannes Waldmann
  3. Hans Zantema

Corresponding author

Correspondence toHans Zantema.

Rights and permissions

About this article

Cite this article

Endrullis, J., Waldmann, J. & Zantema, H. Matrix Interpretations for Proving Termination of Term Rewriting.J Autom Reasoning40, 195–220 (2008). https://doi.org/10.1007/s10817-007-9087-9

Download citation

Keywords

Access this article

Subscribe and save

Springer+
from ¥17,985 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Advertisement

[8]ページ先頭
©2009-2025 Movatter.jp