Skip to main content
SpringerLink
Log in

The Derivational Complexity Induced by the Dependency Pair Method

  • Conference paper
Rewriting Techniques and Applications (RTA 2009)

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

Included in the following conference series:

Abstract

We study the derivational complexity induced by the (basic) dependency pair method. Suppose the derivational complexity induced by a termination method is closed under elementary functions. We show that the derivational complexity induced by the dependency pair method based on this termination technique is the same as for the direct technique. Therefore, the derivational complexity induced by the dependency pair method based on lexicographic path orders or multiset path orders is multiple recursive or primitive recursive, respectively. Moreover for the dependency pair method based on Knuth-Bendix orders, we obtain that the derivational complexity function is majorised by the Ackermann function. These characterisations are essentially optimal.

This research is partly supported by FWF (Austrian Science Fund) project P20133.

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

    Chapter  Google Scholar 

  2. Koprowski, A., Waldmann, J.: Arctic termination ...Below zero. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 202–216. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting based on matrix and context dependent interpretations. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2008. Dagstuhl Seminar Proceedings, vol. 08004, pp. 304–315 (2008)

    Google Scholar 

  4. Zantema, H.: Termination of term rewriting by semantic labelling. FI 24(1,2), 89–105 (1995)

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  6. Moser, G.: Derivational complexity of Knuth Bendix orders revisited. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 75–89. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 364–379. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Hirokawa, N., Moser, G.: Complexity, graphs, and the dependency pair method. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 652–666. Springer, Heidelberg (2008)

    Google Scholar 

  9. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. IC 199(1,2), 172–199 (2005)

    MathSciNet  MATH  Google Scholar 

  10. Dershowitz, N.: Termination dependencies. In: Rubio, A. (ed.) WST 2003. Technical Report DSIC-II/15/03, Universidad Politecnica de Valencia, pp. 27–30 (2003)

    Google Scholar 

  11. Weiermann, A.: Termination proofs for term rewriting systems with lexicographic path orderings imply multiply recursive derivation lengths. TCS 139(1,2), 355–362 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  12. Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. TCS 105(1), 129–140 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  13. Lepper, I.: Derivation lengths and order types of Knuth-Bendix orders. TCS 269(1,2), 433–450 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  14. Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD thesis, University of Aachen (2007)

    Google Scholar 

  15. Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. IC 205, 474–511 (2007)

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Book  MATH  Google Scholar 

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

    Google Scholar 

  19. Geser, A.: Relative Termination. PhD thesis, Universität Passau (1990)

    Google Scholar 

  20. Moser, G., Schnabl, A.: The derivational complexity induced by the dependency pair method. CoRR abs/0904.0570 (2009)

    Google Scholar 

  21. Hofbauer, D.: Termination Proofs and Derivation Lengths in Term Rewriting Systems. PhD thesis, Technische Universität Berlin (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Georg Moser & Andreas Schnabl

Authors
  1. Georg Moser
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andreas Schnabl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire PPS, Université Paris Diderot - Paris 7, CNRS, Paris, France

    Ralf Treinen

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Moser, G., Schnabl, A. (2009). The Derivational Complexity Induced by the Dependency Pair Method . In: Treinen, R. (eds) Rewriting Techniques and Applications. RTA 2009. Lecture Notes in Computer Science, vol 5595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02348-4_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02348-4_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02347-7

  • Online ISBN: 978-3-642-02348-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation