Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Foundational and Practical Aspects of Resource Analysis

FOPARA 2013: Foundational and Practical Aspects of Resource Analysis pp 127–142Cite as

On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets

  • Conference paper
  • First Online:

  • 280 Accesses

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

Abstract

Several variants of linear logic have been proposed to characterize complexity classes in the proofs-as-programs correspondence. Light linear logic (\(LLL\)) ensures a polynomial bound on reduction time, and characterizes in this way the class \(Ptime\). In this paper we study the complexity of linear logic proof-nets and propose two sufficient criteria, one for elementary time soundness and the other one for \(Ptime\) soundness, based on the study of paths inside the proof-net. These criteria offer several benefits: they provide a bound for any reduction sequence and they can be used to prove the complexity soundness of several variants of linear logic. As an example we show with our criteria a strong polytime bound for the system \(L^4\) (light linear logic by levels).

This is a preview of subscription content, 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   34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   44.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

Learn about institutional subscriptions

Notes

  1. 1.

    In fact, a proof of a strong bound is claimed in [13], but it contains flaws which do not seem to be easily patchable. See Appendix B of [12] for more details.

  2. 2.

    The pairs are here represented by using the connective \(\otimes \).

References

  1. Baillot, P., Mazza, D.: Linear logic by levels and bounded time complexity. Theor. Comput. Sci. 411(2), 470–503 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  2. Baillot, P., Pedicini, M.: Elementary complexity and geometry of interaction. Fundamenta Informaticae 45(1–2), 1–31 (2001)

    MathSciNet  MATH  Google Scholar 

  3. Baillot, P., Terui, K.: Light types for polynomial time computation in lambda calculus. Inf. Comput. 207(1), 41–62 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  4. Dal Lago, U.: Context semantics, linear logic, and computational complexity. ACM Trans. Comput. Logic 10(4), 1–32 (2009)

    Article  Google Scholar 

  5. Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: Logic in Computer Science. IEEE (2011)

    Google Scholar 

  6. Danos, V., Joinet, J.B.: Linear logic and elementary time. Inf. Comput. 183(1), 123–137 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  7. Danos, V., Regnier, L.: Proof-nets and the Hilbert space. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge (1995)

    Google Scholar 

  8. Girard, J.Y.: Une extension de l’interpretation de gödel a l’analyse, et son application a l’elimination des coupures dans l’analyse et la theorie des types. In: Fenstad, J.E. (ed.) Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63–92. North Holland, Amsterdam (1971)

    Google Scholar 

  9. Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–102 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  10. Girard, J.Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  11. Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(1–2), 163–180 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  12. Perrinel, M.: On paths-based criteria for polynomial time complexity in proof-nets (long version) (2013). http://arxiv.org/abs/1201.2956

  13. Vercelli, L.: On the Complexity of Stratified Logics. Ph.D. thesis, Scuola di Dottorato in Scienze e Alta Tecnologia, Università degli Studi di Torino - Italy (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ENS de Lyon, CNRS, Inria, UCBL, Université de Lyon. Laboratoire LIP, Lyon, France

    Matthieu Perrinel

Authors
  1. Matthieu Perrinel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthieu Perrinel .

Editor information

Editors and Affiliations

  1. Università di Bologna, Bologna, Italy

    Ugo Dal Lago

  2. Universidad Complutense de Madrid, Madrid, Spain

    Ricardo Peña

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Perrinel, M. (2014). On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets. In: Dal Lago, U., Peña, R. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2013. Lecture Notes in Computer Science(), vol 8552. Springer, Cham. https://doi.org/10.1007/978-3-319-12466-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12466-7_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12465-0

  • Online ISBN: 978-3-319-12466-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation