Skip to main content
SpringerLink
Log in

Proofs of Termination of Rewrite Systems for Polytime Functions

  • Conference paper
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005)

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

Abstract

We define a new path order \({\prec_{\textsc{pop}}}\) so that for a finite rewrite system R compatible with \({\prec_{\textsc{pop}}}\), the complexity or derivation length function Dl\(_{R}^{f}\) for each function symbol f is guaranteed to be bounded by a polynomial in the length of the inputs. Our results yield a simplification and clarification of the results obtained by Beckmann and Weiermann (Archive for Mathematical Logic, 36:11–30, 1996).

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Beckmann, A., Weiermann, A.: A term rewriting characterization of the polytime functions and related complexity classes. Archive for Mathematical Logic 36, 11–30 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  2. Cichon, E.A., Weiermann, A.: Term rewriting theory for the primitive recursive functions. Annals of Pure and Applied Logic 83, 199–223 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  3. Oitavem, I.: A term rewriting characterization of the functions computable in polynomal space. Archive for Mathematical Logic 41, 35–47 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-intepretations and small space bounds. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 150–164. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge Univeristy Press, New York (1998)

    Google Scholar 

  6. Cobham, A.: The intrinsic computational difficulty of functions. In: Bar-Hillel, Y. (ed.) Logic, Methodology and Philosophy of Science, proceedings of the second International Congress, p. 1964. North-Holland, Amsterdam (1965)

    Google Scholar 

  7. Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions. Comput. Complexity 2, 97–110 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  8. Arai, T., Moser, G.: A note on a term rewriting characterization of PTIME. In: Proc. of WST 2004, pp. 10–13 (2004) (extended abstract)

    Google Scholar 

  9. Buchholz, W.: Proof-theoretical analysis of termination proofs. Annals of Pure and Applied Logic 75, 57–65 (1995)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  11. Marion, J.: Analysing the implicit complexity of programs. Information and Computation 183, 2–18 (2003)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Graduate School of Science and Technology, Kobe University,  

    Toshiyasu Arai

  2. Computational Logic, University of Innsbruck,  

    Georg Moser

Authors
  1. Toshiyasu Arai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Georg Moser
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National Institute of Advanced Studies, Indian Institute of Science Campus, 560012, Bangalore, India

    Sundar Sarukkai

  2. Department of Comp. Sc. & Engg., Indian Institute of Technology Delhi, 110016, New Delhi, India

    Sandeep Sen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arai, T., Moser, G. (2005). Proofs of Termination of Rewrite Systems for Polytime Functions. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_43

Download citation

  • DOI: https://doi.org/10.1007/11590156_43

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30495-1

  • Online ISBN: 978-3-540-32419-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation