Skip to main content
SpringerLink
Log in

A New Order-Theoretic Characterisation of the Polytime Computable Functions

  • Conference paper
Programming Languages and Systems (APLAS 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7705))

Included in the following conference series:

Abstract

We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define the small polynomial path order (sPOP * for short). This termination order entails a new syntactic method to analyse the innermost runtime complexity of term rewrite systems fully automatically: for any rewrite system compatible with sPOP* that employs recursion upto depth d, the (innermost) runtime complexity is polynomially bounded of degree d. This bound is tight.

This work is partially supported by FWF (Austrian Science Fund) project I-608-N18 and by a grant of the University of Innsbruck. The second author is supported by a grant from the John Templeton Foundation for the project “Philosophical Frontiers in Reverse Mathematics”.

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. Bellantoni, S., Cook, S.: A new Recursion-Theoretic Characterization of the Polytime Functions. CC 2(2), 97–110 (1992)

    MathSciNet  MATH  Google Scholar 

  2. Baillot, P., Marion, J.Y., Rocca, S.R.D.: Guest Editorial: Special Issue on Implicit Computational Complexity. TOCL 10(4) (2009)

    Google Scholar 

  3. Marion, J.Y.: Analysing the Implicit Complexity of Programs. IC 183, 2–18 (2003)

    MathSciNet  MATH  Google Scholar 

  4. Arai, T., Moser, G.: Proofs of Termination of Rewrite Systems for Polytime Functions. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 529–540. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Avanzini, M., Moser, G.: Complexity Analysis by Rewriting. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 130–146. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Avanzini, M., Moser, G.: Polynomial Path Orders: A Maximal Model. CoRR cs/CC/1209.3793 (2012), http://www.arxiv.org/

  7. Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with Polynomial Interpretation Termination Proof. JFP 11(1), 33–53 (2001)

    MathSciNet  MATH  Google Scholar 

  8. Marion, J.Y.: On Tiered Small Jump Operators. LMCS 5(1) (2009)

    Google Scholar 

  9. Moser, G., Schnabl, A.: Proving Quadratic Derivational Complexities Using Context Dependent Interpretations. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 276–290. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Hirokawa, N., Moser, G.: Automated Complexity Analysis Based on the Dependency Pair Method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Zankl, H., Korp, M.: Modular Complexity Analysis via Relative Complexity. In: Proc. of 21st RTA. LIPIcs, vol. 6, pp. 385–400 (2010)

    Google Scholar 

  12. Noschinski, L., Emmes, F., Giesl, J.: A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 422–438. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Hirokawa, N., Moser, G.: Automated Complexity Analysis Based on the Dependency Pair Method. CoRR abs/1102.3129 (2011) (submitted)

    Google Scholar 

  14. Middeldorp, A., Moser, G., Neurauter, F., Waldmann, J., Zankl, H.: Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems. In: Winkler, F. (ed.) CAI 2011. LNCS, vol. 6742, pp. 1–20. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  15. Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis. In: Proc. of 38th POPL, pp. 357–370. ACM (2011)

    Google Scholar 

  16. Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G., Ramírez, D., Román, G., Zanardini, D.: Termination and Cost Analysis with COSTA and its User Interfaces. ENTCS 258(1), 109–121 (2009)

    Google Scholar 

  17. Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117–133. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Gulwani, S., Mehra, K., Chilimbi, T.: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In: Proc. of 36th POPL, pp. 127–139. ACM (2009)

    Google Scholar 

  19. Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound Analysis of Imperative Programs with the Size-Change Abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Simmons, H.: The Realm of Primitive Recursion. AML 27, 177–188 (1988)

    MathSciNet  MATH  Google Scholar 

  21. Leivant, D.: A Foundational Delineation of Computational Feasiblity. In: Proc. of 6th LICS, pp. 2–11. IEEE Computer Society (1991)

    Google Scholar 

  22. Handley, W.G., Wainer, S.S.: Complexity of Primitive Recursion. In: Computational Logic. NATO ASI Series F: Computer and Systems Science, vol. 165, pp. 273–300 (1999)

    Google Scholar 

  23. Avanzini, M., Eguchi, N., Moser, G.: A New Order-theoretic Characterisation of the Polytime Computable Functions. CoRR cs/CC/1201.2553 (2012), http://www.arxiv.org/

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

    Google Scholar 

  25. Dal Lago, U., Martini, S.: On Constructor Rewrite Systems and the Lambda-Calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 163–174. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Avanzini, M., Moser, G.: Closing the Gap Between Runtime Complexity and Polytime Computability. In: Proc. of 21st RTA. LIPIcs, vol. 6, pp. 33–48 (2010)

    Google Scholar 

  27. Avanzini, M., Eguchi, N., Moser, G.: On a Correspondence between Predicative Recursion and Register Machines. In: Proc. of 12th WST, pp. 15–19 (2012), http://cl-informatik.uibk.ac.at/users/georg/events/wst2012/

  28. Hoffmann, J., Aehlig, K., Hofmann, M.: Resource Aware ML. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 781–786. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Martin Avanzini & Georg Moser

  2. Mathematical Institute, Tohoku University, Japan

    Naohi Eguchi

Authors
  1. Martin Avanzini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Naohi Eguchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Georg Moser
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of California, San Diego, 9500 Gilman Drive, 92092-6237, La Jolla, CA, USA

    Ranjit Jhala

  2. Graduate School of Informatics, Kyoto University, Yoshida-Honmachi, 606-8501, Sakyo-ku, Kyoto, Japan

    Atsushi Igarashi

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Avanzini, M., Eguchi, N., Moser, G. (2012). A New Order-Theoretic Characterisation of the Polytime Computable Functions. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-35182-2_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-35181-5

  • Online ISBN: 978-3-642-35182-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation