Document Open Access Logo

Combining Linear Logic and Size Types for Implicit Complexity

Authors Patrick Baillot, Alexis Ghyselen

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.9.pdf
  • Filesize: 0.57 MB
  • 21 pages

Document Identifiers

Author Details

Patrick Baillot
  • Univ Lyon, CNRS, ENS de Lyon, Université Claude-Bernard Lyon 1, LIP , F-69342, Lyon Cedex 07, France
Alexis Ghyselen
  • ENS Paris-Saclay, 94230 Cachan, France

Cite AsGet BibTex

Patrick Baillot and Alexis Ghyselen. Combining Linear Logic and Size Types for Implicit Complexity. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.9

Abstract

Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its !-modality controlling duplication. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. However both approaches suffer from limitations : either a limited intensional expressivity, or linearity restrictions. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. Our system is based on elementary linear logic combined with linear size types, called sEAL, and leads to characterizations of the complexity classes FPTIME and 2k-FEXPTIME, for k >= 0.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Linear logic
  • Theory of computation → Turing machines
  • Software and its engineering → Functional languages
Keywords
  • Implicit computational complexity
  • lambda-calculus
  • linear logic
  • type systems
  • polynomial time complexity
  • size types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Martin Avanzini and Ugo Dal Lago. Automating sized-type inference for complexity analysis. PACMPL, 1(ICFP):43:1-43:29, 2017. Google Scholar
  2. Patrick Baillot. On the expressivity of elementary linear logic: Characterizing ptime and an exponential time hierarchy. Information and Computation, 241:3-31, 2015. Google Scholar
  3. Patrick Baillot, Gilles Barthe, and Ugo Dal Lago. Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (long version). Research report, ENS Lyon, 2015. URL: https://hal.archives-ouvertes.fr/hal-01197456.
  4. Patrick Baillot and Ugo Dal Lago. Higher-order interpretations and program complexity. Information and Computation, 248:56-81, 2016. Google Scholar
  5. Patrick Baillot, Erika De Benedetti, and Simona Ronchi Della Rocca. Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. In IFIP International Conference on Theoretical Computer Science, pages 151-163. Springer, 2014. Google Scholar
  6. Patrick Baillot, Marco Gaboardi, and Virgile Mogbil. A polytime functional language from light linear logic. In European Symposium on Programming, pages 104-124. Springer, 2010. Google Scholar
  7. Patrick Baillot and Alexis Ghyselen. Combining linear logic and size types for implicit complexity (long version). hal-01687224, [Research Report], 2018. Google Scholar
  8. Patrick Baillot and Kazushige Terui. A feasible algorithm for typing in elementary affine logic. In TLCA, volume 5, pages 55-70. Springer, 2005. Google Scholar
  9. Stephen Bellantoni and Stephen Cook. A new recursion-theoretic characterization of the polytime functions. In Proceedings of the twenty-fourth annual ACM symposium on Theory of computing, pages 283-293. ACM, 1992. Google Scholar
  10. Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen. Quasi-interpretations a way to control resources. Theoretical Computer Science, 412(25):2776-2796, 2011. Google Scholar
  11. Ugo Dal Lago and Barbara Petit. The geometry of types. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'13, Proceedings, pages 167-178. ACM, 2013. Google Scholar
  12. Ugo Dal Lago and Barbara Petit. Linear dependent types in a call-by-value scenario. Science of Computer Programming, 84:77-100, 2014. Google Scholar
  13. Ugo Dal Lago and Paolo Parisen Toldin. A higher-order characterization of probabilistic polynomial time. In International Workshop on Foundational and Practical Aspects of Resource Analysis, pages 1-18. Springer, 2011. Google Scholar
  14. Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. Information and Computation, 183(1):123-137, 2003. Google Scholar
  15. Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175-204, 1998. Google Scholar
  16. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. In 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11, Proceedings. ACM, 2011. Google Scholar
  17. Jan Hoffmann and Martin Hofmann. Amortized resource analysis with polynomial potential. In 19th Euro. Symp. on Prog.(ESOP’10), pages 287-306. Springer, 2010. Google Scholar
  18. Martin Hofmann. A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion. In International Workshop on Computer Science Logic, pages 275-294. Springer, 1997. Google Scholar
  19. Martin Hofmann. Linear types and non-size-increasing polynomial time computation. Information and Computation, 183(1):57-85, 2003. Google Scholar
  20. Martin Hofmann and Steffen Jost. Static prediction of heap space usage for first-order functional programs. In 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11, Proceedings, pages 185-197. ACM, 2003. Google Scholar
  21. John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 410-423, 1996. Google Scholar
  22. Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. Static determination of quantitative resource usage for higher-order programs. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2010, pages 223-236, 2010. Google Scholar
  23. Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. Logical Methods in Computer Science, 8(4), 2011. Google Scholar
  24. Antoine Madet and Roberto M Amadio. An elementary affine λ-calculus with multithreading and side effects. In International Conference on Typed Lambda Calculi and Applications, pages 138-152. Springer, 2011. Google Scholar
  25. John Mitchell, Mark Mitchell, and Andre Scedrov. A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In Foundations of Computer Science, 1998. Proceedings. 39th Annual Symposium on, pages 725-733. IEEE, 1998. Google Scholar
  26. Kazushige Terui. Light affine lambda calculus and polytime strong normalization. In Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on, pages 209-220. IEEE, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact