Polynomial Time and Dependent Types
Article No.: 76, Pages 2288 - 2317
Abstract
We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann.
Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory.
References
[1]
Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. 2005. Containers: Constructing strictly positive types. Theor. Comput. Sci., 342, 1 (2005), 3–27. https://doi.org/10.1016/j.tcs.2005.06.002
[2]
Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson. 2023. A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. Proc. ACM Program. Lang., 7, ICFP (2023), Article 220, aug, 35 pages. https://doi.org/10.1145/3607862
[3]
Klaus Aehlig and Helmut Schwichtenberg. 2002. A syntactical analysis of non-size-increasing polynomial time computation. ACM Trans. Comput. Log., 3, 3 (2002), 383–401. https://doi.org/10.1145/507382.507386
[4]
Sanjeev Arora and Boaz Barak. 2009. Computational Complexity - A Modern Approach. Cambridge University Press. isbn:978-0-521-42426-4 http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264
[5]
Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 56–65. https://doi.org/10.1145/3209108.3209189
[6]
Robert Atkey. 2023. Agda formalisation of Polynomial Time and Dependent Types. https://doi.org/10.5281/zenodo.8425923
[7]
Robert Atkey. 2023. Polynomial Time and Dependent Types - Extended Version. https://doi.org/10.48550/arXiv.2307.09145 arXiv:2307.09145
[8]
Patrick Baillot, Marco Gaboardi, and Virgile Mogbil. 2010. A PolyTime Functional Language from Light Linear Logic. In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, Andrew D. Gordon (Ed.) (Lecture Notes in Computer Science, Vol. 6012). Springer, 104–124. https://doi.org/10.1007/978-3-642-11957-6_7
[9]
Patrick Baillot and Virgile Mogbil. 2004. Soft lambda-Calculus: A Language for Polynomial Time Computation. In Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, Igor Walukiewicz (Ed.) (Lecture Notes in Computer Science, Vol. 2987). Springer, 27–41. https://doi.org/10.1007/978-3-540-24727-2_4
[10]
Andrew Barber. 1996. Dual Intuitionistic Linear Logic. University of Edinburgh.
[11]
Andrej Bauer. 2005. First Steps in Synthetic Computability Theory. In Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 2005, Birmingham, UK, May 18-21, 2005, Martín Hötzel Escardó, Achim Jung, and Michael W. Mislove (Eds.) (Electronic Notes in Theoretical Computer Science, Vol. 155). Elsevier, 5–31. https://doi.org/10.1016/j.entcs.2005.11.049
[12]
Stephen J. Bellantoni and Stephen A. Cook. 1992. A New Recursion-Theoretic Characterization of the Polytime Functions. Comput. Complex., 2 (1992), 97–110. https://doi.org/10.1007/BF01201998
[13]
P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, Leszek Pacholski and Jerzy Tiuryn (Eds.) (Lecture Notes in Computer Science, Vol. 933). Springer, 121–135. https://doi.org/10.1007/BFb0022251
[14]
Edwin C. Brady. 2021. Idris 2: Quantitative Type Theory in Practice. In 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), Anders Møller and Manu Sridharan (Eds.) (LIPIcs, Vol. 194). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 9:1–9:26. https://doi.org/10.4230/LIPIcs.ECOOP.2021.9
[15]
Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014. 351–370. https://doi.org/10.1007/978-3-642-54833-8_19
[16]
Iliano Cervesato and Frank Pfenning. 2002. A Linear Logical Framework. Inf. Comput., 179, 1 (2002), 19–75. https://doi.org/10.1006/inco.2001.2951
[17]
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. 2021. A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang., 5, POPL (2021), 1–32. https://doi.org/10.1145/3434331
[18]
Paolo Coppola and Simone Martini. 2001. Typing Lambda Terms in Elementary Logic with Linear Constraints. In Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings, Samson Abramsky (Ed.) (Lecture Notes in Computer Science, Vol. 2044). Springer, 76–90. https://doi.org/10.1007/3-540-45413-6_10
[19]
Ugo Dal Lago. 2011. A Short Introduction to Implicit Computational Complexity. In Lectures on Logic and Computation - ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011, Selected Lecture Notes, Nick Bezhanishvili and Valentin Goranko (Eds.) (Lecture Notes in Computer Science, Vol. 7388). Springer, 89–109. https://doi.org/10.1007/978-3-642-31485-8_3
[20]
Ugo Dal Lago and Martin Hofmann. 2010. Bounded Linear Logic, Revisited. Log. Methods Comput. Sci., 6, 4 (2010), https://doi.org/10.2168/LMCS-6(4:7)2010
[21]
Ugo Dal Lago and Martin Hofmann. 2010. A Semantic Proof of Polytime Soundness of Light Affine Logic. Theory Comput. Syst., 46, 4 (2010), 673–689. https://doi.org/10.1007/s00224-009-9210-x
[22]
Ugo Dal Lago and Martin Hofmann. 2011. Realizability models and implicit complexity. Theor. Comput. Sci., 412, 20 (2011), 2029–2047. https://doi.org/10.1016/j.tcs.2010.12.025
[23]
Ugo Dal Lago, Reinhard Kahle, and Isabel Oitavem. 2021. A Recursion-Theoretic Characterization of the Probabilistic Class PP. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), Filippo Bonchi and Simon J. Puglisi (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 202). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 35:1–35:12. isbn:978-3-95977-201-3 issn:1868-8969 https://doi.org/10.4230/LIPIcs.MFCS.2021.35
[24]
Ugo Dal Lago and Ulrich Schöpp. 2016. Computation by interaction for space-bounded functional programming. Inf. Comput., 248 (2016), 150–194. https://doi.org/10.1016/j.ic.2015.04.006
[25]
Ugo Dal Lago and Paolo Parisen Toldin. 2015. A higher-order characterization of probabilistic polynomial time. Inf. Comput., 241 (2015), 114–141. https://doi.org/10.1016/J.IC.2014.10.009
[26]
Nils Anders Danielsson. 2008. Lightweight semiformal time complexity analysis for purely functional data structures. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, George C. Necula and Philip Wadler (Eds.). ACM, 133–144. https://doi.org/10.1145/1328438.1328457
[27]
Peng Fu, Kohei Kishida, and Peter Selinger. 2022. Linear Dependent Type Theory for Quantum Programming Languages. Log. Methods Comput. Sci., 18, 3 (2022), https://doi.org/10.46298/lmcs-18(3:28)2022
[28]
Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014. 331–350. https://doi.org/10.1007/978-3-642-54833-8_18
[29]
Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci., 50 (1987), 1–102. https://doi.org/10.1016/0304-3975(87)90045-4
[30]
Jean-Yves Girard. 1998. Light Linear Logic. Inf. Comput., 143, 2 (1998), 175–204. https://doi.org/10.1006/inco.1998.2700
[31]
Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded Linear Logic: A Modular Approach to Polynomial-Time Computability. Theor. Comput. Sci., 97, 1 (1992), 1–66. https://doi.org/10.1016/0304-3975(92)90386-T
[32]
Armaël Guéneau, Arthur Charguéraud, and François Pottier. 2018. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Amal Ahmed (Ed.) (Lecture Notes in Computer Science, Vol. 10801). Springer, 533–560. https://doi.org/10.1007/978-3-319-89884-1_19
[33]
Emmanuel Hainry and Romain Péchoux. 2023. A General Noninterference Policy for Polynomial Time. Proc. ACM Program. Lang., 7, POPL (2023), 806–832. https://doi.org/10.1145/3571221
[34]
Jan Hoffmann, Ankush Das, and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 359–373. https://doi.org/10.1145/3009837.3009842
[35]
Jan Hoffmann and Steffen Jost. 2022. Two decades of automatic amortized resource analysis. Math. Struct. Comput. Sci., 32, 6 (2022), 729–759. https://doi.org/10.1017/S0960129521000487
[36]
Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. In Semantics and Logics of Computation. Cambridge University Press, 79–130.
[37]
Martin Hofmann. 1999. Linear Types and Non-Size-Increasing Polynomial Time Computation. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999. IEEE Computer Society, 464–473. https://doi.org/10.1109/LICS.1999.782641
[38]
Martin Hofmann. 2003. Linear types and non-size-increasing polynomial time computation. Inf. Comput., 183, 1 (2003), 57–85. https://doi.org/10.1016/S0890-5401(03)00009-9
[39]
Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003, Alex Aiken and Greg Morrisett (Eds.). ACM, 185–197. https://doi.org/10.1145/604131.604148
[40]
Martin Hofmann and Philip J. Scott. 2004. Realizability models for BLL-like languages. Theor. Comput. Sci., 318, 1-2 (2004), 121–137. https://doi.org/10.1016/j.tcs.2003.10.019
[41]
Gérard P. Huet. 1997. The Zipper. J. Funct. Program., 7, 5 (1997), 549–554. https://doi.org/10.1017/s0956796897002864
[42]
Neil D. Jones. 2001. The expressive power of higher-order types or, life without CONS. J. Funct. Program., 11, 1 (2001), 5–94. https://doi.org/10.1017/s0956796800003889
[43]
Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 17–30. https://doi.org/10.1145/2676726.2676969
[44]
Yves Lafont. 2004. Soft linear logic and polynomial time. Theor. Comput. Sci., 318, 1-2 (2004), 163–180. https://doi.org/10.1016/j.tcs.2003.10.018
[45]
Conor McBride. 2016. I Got Plenty o’ Nuttin’. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.) (Lecture Notes in Computer Science, Vol. 9600). Springer, 207–233. https://doi.org/10.1007/978-3-319-30936-1_12
[46]
Jay A. McCarthy, Burke Fetscher, Max S. New, Daniel Feltey, and Robert Bruce Findler. 2016. A Coq Library for Internal Verification of Running-Times. In Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings, Oleg Kiselyov and Andy King (Eds.) (Lecture Notes in Computer Science, Vol. 9613). Springer, 144–162. https://doi.org/10.1007/978-3-319-29604-3_10
[47]
Benjamin Moon, Harley Eades III, and Dominic Orchard. 2021. Graded Modal Dependent Type Theory. In Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Nobuko Yoshida (Ed.) (Lecture Notes in Computer Science, Vol. 12648). Springer, 462–490. https://doi.org/10.1007/978-3-030-72019-3_17
[48]
Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. 2022. A cost-aware logical framework. Proc. ACM Program. Lang., 6, POPL (2022), 1–31. https://doi.org/10.1145/3498670
[49]
Ulf Norell. 2008. Dependently typed programming in Agda. In International school on advanced functional programming. 230–266.
[50]
Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. 2019. Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang., 3, ICFP (2019), 110:1–110:30. https://doi.org/10.1145/3341714
[51]
Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2021. A unifying type-theory for higher-order (amortized) cost analysis. Proc. ACM Program. Lang., 5, POPL (2021), 1–28. https://doi.org/10.1145/3434308
[52]
Matthijs Vákár. 2014. Syntax and Semantics of Linear Dependent Types. CoRR, abs/1405.0033 (2014), arxiv:1405.0033
Recommendations
Light types for polynomial time computation in lambda calculus
We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one ...
Propositions as [Types]
Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational ...
Linear dependent types in a call-by-value scenario
Linear dependent types were introduced recently (Dal Lago and Gaboardi, 2012) [26] as a formal system that allows to precisely capture both the extensional behavior and the time complexity of @l-terms, when the latter are evaluated by Krivine's abstract ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
2820 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 January 2024
Published in PACMPL Volume 8, Issue POPL
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 347Total Downloads
- Downloads (Last 12 months)347
- Downloads (Last 6 weeks)52
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in