Skip to main content
SpringerLink
Log in

On the Domain and Dimension Hierarchy of Matrix Interpretations

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7180))

Abstract

Matrix interpretations are a powerful technique for proving termination of term rewrite systems. Depending on the underlying domain of interpretation, one distinguishes between matrix interpretations over the real, rational and natural numbers. In this paper we clarify the relationship between all three variants, showing that matrix interpretations over the reals are more powerful than matrix interpretations over the rationals, which are in turn more powerful than matrix interpretations over the natural numbers. We also clarify the ramifications of matrix dimension on termination proving power. To this end, we establish a hierarchy of matrix interpretations with respect to matrix dimension and show it to be infinite, with each level properly subsuming its predecessor.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alarcón, B., Lucas, S., Navarro-Marset, R.: Proving termination with matrix interpretations over the reals. In: WST 2009, pp. 12–15 (2009)

    Google Scholar 

  2. Amitsur, A., Levitzki, J.: Minimal identities for algebras. Proceedings of the American Mathematical Society 1(4), 449–463 (1950)

    Article  MathSciNet  MATH  Google Scholar 

  3. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. TCS 236(1-2), 133–178 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  4. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

    Google Scholar 

  5. Courtieu, P., Gbedo, G., Pons, O.: Improved Matrix Interpretation. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol. 5901, pp. 283–295. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(2–3), 195–220 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  7. Gebhardt, A., Hofbauer, D., Waldmann, J.: Matrix evolutions. In: WST 2007, pp. 4–8 (2007)

    Google Scholar 

  8. Gebhardt, A., Waldmann, J.: Weighted automata define a hierarchy of terminating string rewriting systems. Acta Cybernetica 19(2), 295–312 (2009)

    MathSciNet  MATH  Google Scholar 

  9. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR-11 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. JAR 37(3), 155–203 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  11. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. I&C 199(1-2), 172–199 (2005)

    MathSciNet  MATH  Google Scholar 

  12. Hofbauer, D.: Termination Proofs by Context-Dependent Interpretations. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 108–121. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Horn, R., Johnson, C.: Matrix Analysis. Cambridge University Press (1990)

    Google Scholar 

  16. Lucas, S.: On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. AAECC 17(1), 49–73 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  17. Lucas, S.: From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 116–131. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Neurauter, F., Middeldorp, A.: Polynomial interpretations over the reals do not subsume polynomial interpretations over the integers. In: RTA 2010. LIPIcs, vol. 6, pp. 243–258 (2010)

    Google Scholar 

  19. Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: RTA 2011. LIPIcs, vol. 10, pp. 251–266 (2011)

    Google Scholar 

  20. Neurauter, F., Zankl, H., Middeldorp, A.: Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17 2010. LNCS, vol. 6397, pp. 550–564. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Rose, H.E.: Linear Algebra: A Pure Mathematical Approach. Birkhäuser (2002)

    Google Scholar 

  22. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)

    Google Scholar 

  23. Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD thesis, RWTH Aachen, available as Technical Report AIB-2007-17 (2007)

    Google Scholar 

  24. Zankl, H., Middeldorp, A.: Satisfiability of Non-linear (Ir)rational Arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 481–500. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Friedrich Neurauter & Aart Middeldorp

Authors
  1. Friedrich Neurauter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Nikolaj Bjørner

  2. School of computer Science, University of Manchester, Kilburn Building, Oxford Road, MP13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Neurauter, F., Middeldorp, A. (2012). On the Domain and Dimension Hierarchy of Matrix Interpretations. In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28717-6_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-28716-9

  • Online ISBN: 978-3-642-28717-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation