Skip to main content
SpringerLink
Log in

Complexity Invariance of Real Interpretations

  • Conference paper
Theory and Applications of Models of Computation (TAMC 2010)

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

Abstract

In the field of implicit computational complexity, we are considering in this paper the fruitful branch of interpretation methods. In this area, the synthesis problem is solved by Tarski’s decision procedure, and consequently interpretations are usually chosen over the reals rather than over the integers. Doing so, one cannot use anymore the (good) properties of the natural (well-) ordering of N employed to bound the complexity of programs. We show that, actually, polynomials over the reals benefit from some properties that allow their safe use for complexity. We illustrate this by two characterizations, one of PTIME and one of PSPACE.

Work partially supported by project ANR-08-BLANC-0211-01 (COMPLICE).

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. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

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

  3. Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry. Springer, Heidelberg (2003)

    MATH  Google Scholar 

  4. Bonfante, G., Cichon, A., Marion, J.-Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. Journal of Functional Programming 11(1), 33–53 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bonfante, G., Deloup, F.: Complexity invariance of real interpretations. Technical report, LORIA (2010), http://www.loria.fr/~bonfante/ciri.pdf

  6. Coste, M., Lombardi, H., Roy, M.-F.: Dynamical method in algebra: Effective nullstellensätze. Annals of Pure and Applied Logic 111, 203–256 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  7. dal Lago, U., Martini, S.: Derivational complexity is an invariant cost model. In: Foundational and Practical Aspects of Resource Analysis, FOPARA 2009 (2009)

    Google Scholar 

  8. Dershowitz, N.: A note on simplification orderings. Information Processing Letters, 212–215 (1979)

    Google Scholar 

  9. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol. B, pp. 243–320 (1990)

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

    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.: Proving termination with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 50–65. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27(4), 797–821 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  15. Huet, G., Oppen, D.: Equations and rewrite rules: A survey. In: Book, R.V. (ed.) Formal Language Theory: Perspectives and Open Problems, pp. 349–405. AP (1980)

    Google Scholar 

  16. Lankford, D.S.: On proving term rewriting systems are noetherien. Technical report (1979)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  18. Lucas, S.: Practical use of polynomials over the reals in proofs of termination. In: PPDP 2007: Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, pp. 39–50. ACM, New York (2007)

    Google Scholar 

  19. Lucas, S., Peña, R.: Rewriting techniques for analysing termination and complexity bounds of safe programs. In: Hanus, M. (ed.) LOPSTR 2008. LNCS, vol. 5438, pp. 43–57. Springer, Heidelberg (2009)

    Google Scholar 

  20. Marion, J.-Y., Péchoux, R.: Resource analysis by sup-interpretation. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 163–176. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Marion, J.-Y., Péchoux, R.: Characterizations of polynomial complexity classes with a better intensionality. In: Antoy, S., Albert, E. (eds.) PPDP, pp. 79–88. ACM, New York (2008)

    Chapter  Google Scholar 

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

  23. Rosen, B.: Tree-manipulating systems and church-rosser theorems. Journal of the ACM 20(1), 160–187 (1973)

    Article  MATH  Google Scholar 

  24. Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Mathematische Annalen 207(2), 87–97 (1973)

    Article  MATH  MathSciNet  Google Scholar 

  25. Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, California (1951)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LORIA, Université de Nancy, Nancy, France

    Guillaume Bonfante

  2. Toulouse - IMT, Université Paul Sabatier, France

    Florian Deloup

Authors
  1. Guillaume Bonfante
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Florian Deloup
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Charles University, Malostranske nam 25, 11800, Praha 1, Czech Republic

    Jan Kratochvíl , Jiří Fiala  & Petr Kolman ,  & 

  2. State Key Lab. of Computer Science, Institute of Software,, Chinese Academy of Sciences, 100190, Beijing, P.R. China

    Angsheng Li

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bonfante, G., Deloup, F. (2010). Complexity Invariance of Real Interpretations. In: Kratochvíl, J., Li, A., Fiala, J., Kolman, P. (eds) Theory and Applications of Models of Computation. TAMC 2010. Lecture Notes in Computer Science, vol 6108. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13562-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13562-0_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13561-3

  • Online ISBN: 978-3-642-13562-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation