Document Open Access Logo

Polynomial Time in the Parametric Lambda Calculus

Author Brian F. Redmond

PDF

File

Thumbnail PDF
PDF
LIPIcs.TLCA.2015.288.pdf
  • Filesize: 474 kB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • Parametric Lambda Calculus
  • Polynomial Time Complexity
  • Combinators
  • Nondeterminism and Explicit Products
  • Implicit Computational Complexity

Metrics

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

Abstract

In this paper we investigate Implicit Computational Complexity via the parametric lambda calculus of Ronchi Della Rocca and Paolini. We show that a particular instantiation of the set of input values leads to a characterization of polynomial time computations in a similar way to Lafont’s Soft Linear Logic. This characterization is manifestly type-free and does not require any ad hoc extensions to the pure lambda calculus. Moreover, there is a natural extension to nondeterminism with the addition of explicit products.

Cite As Get BibTex

Brian F. Redmond. Polynomial Time in the Parametric Lambda Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 288-301, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.288

Author Details

Brian F. Redmond

References

  1. Beniamino Accattoli and Ugo Dal Lago. Beta reduction is invariant, indeed. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS'14, Vienna, Austria, July 14-18, 2014, page 8. ACM, 2014. Google Scholar
  2. Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda-calculus. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 266-275. IEEE Computer Society, 2004. Google Scholar
  3. Hendrik Pieter Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, New-York, Oxford, 1981. Google Scholar
  4. J. Chrząszcz and A. Schubert. The role of polymorphism in the characterisation of complexity by soft types. (To appear). Google Scholar
  5. Marco Gaboardi and Simona Ronchi Della Rocca. A soft type assignment system for lambda-calculus. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 253-267. Springer, 2007. Google Scholar
  6. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse d'état, Université Paris 7, June 1972. Google Scholar
  7. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Number 7 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. Google Scholar
  8. J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, New York, NY, USA, 2 edition, 2008. Google Scholar
  9. Yves Lafont. Soft linear logic and polynomial time. Theor. Comput. Sci., 318(1-2):163-180, 2004. Google Scholar
  10. Daniel Leivant. Finitely stratified polymorphism. Inf. Comput., 93(1):93-113, 1991. Google Scholar
  11. Harry G. Mairson and Kazushige Terui. On the computational complexity of cut-elimination in linear logic. In Carlo Blundo and Cosimo Laneve, editors, Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings, volume 2841 of Lecture Notes in Computer Science, pages 23-36. Springer, 2003. Google Scholar
  12. B. Redmond. Bounded combinatory logic and lower complexity. (To appear). Google Scholar
  13. Simona Ronchi Della Rocca and Luca Paolini. The parametric lambda calculus: a meta-model for computation. Texts in theoretical computer science. Springer-Verlag, New York, 2004. Google Scholar
  14. Aleksy Schubert. The complexity of beta-reduction in low orders. In TLCA, pages 400-414, 2001. Google Scholar
  15. H. Schwichtenberg. Definierbare Funktionen im λ-Kalkül mit Typen. Arkhiv für mathematische Logik und Grundlagenforschung, 17:113-114, 1976. Google Scholar
  16. R. Statman. The typed lambda calculus is not elementary recursive. Theoretical Computer Science, 9:73-82, 1979. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact