Abstract
Multi types—aka non-idempotent intersection types—have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps.
Starting from this observation, we refine and generalise a technique introduced by Bernadet & Graham-Lengrand to provide exact bounds for the maximal strategy. Our typing judgements carry two counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the λ-calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation).
Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet & Graham-Lengrand via a uniform technique and a complexity-based perspective. The two main novelties are exact split bounds for the leftmost strategy—the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure—and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear substitution calculus.
Supplemental Material
- Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In RTA’12 (LIPIcs), Ashish Tiwari (Ed.), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6–21.Google Scholar
- Beniamino Accattoli. 2018. (In)Efficiency and Reasonable Cost Models. Invited paper at LSFA 2017, to appear. (2018).Google Scholar
- Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. 2014. A nonstandard standardization theorem. In POPL 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 659–670. Google ScholarDigital Library
- Beniamino Accattoli and Ugo Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In RTA’12 (LIPIcs), Ashish Tiwari (Ed.), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 22–37.Google Scholar
- Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta-Reduction is Invariant, Indeed. Logical Methods in Computer Science 12, 1 (2016).Google Scholar
- Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. 2018. Tight Typings and Split Bounds (Long Version). (2018). http://arxiv.org/abs/1807.02358Google Scholar
- Martin Avanzini and Ugo Dal Lago. 2017. Automating sized-type inference for complexity analysis. PACMPL 1, ICFP (2017), 43:1–43:29. Google ScholarDigital Library
- Erika De Benedetti and Simona Ronchi Della Rocca. 2016. A type assignment for λ-calculus complete both for FPTIME and strong normalization. Information and Computation 248 (2016), 195–214. Google ScholarDigital Library
- Alexis Bernadet and Stéphane Graham-Lengrand. 2013a. A big-step operational semantics via non-idempotent intersection types. (2013). https://hal.archives- ouvertes.fr/hal- 01830232 Technical Report.Google Scholar
- Alexis Bernadet and Stéphane Graham-Lengrand. 2013b. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9, 4 (2013).Google Scholar
- Alexis Bernadet and Stéphane Lengrand. 2011. Complexity of Strongly Normalising Lambda-Terms via Non-idempotent Intersection Types. In FoSSaCS’11 (Lecture Notes in Computer Science), Martin Hofmann (Ed.), Vol. 6604. Springer, 88–107. Google ScholarDigital Library
- Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In FPCA’95, John Williams (Ed.). ACM, 226–237. Google ScholarDigital Library
- Antonio Bucciarelli and Thomas Ehrhard. 2001. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic 109, 3 (2001), 205–241.Google ScholarCross Ref
- Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. 2012. A relational semantics for parallelism and nondeterminism in a functional setting. Annals of Pure and Applied Logic 163, 7 (2012), 918–934.Google ScholarCross Ref
- Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. 2014. The Inhabitation Problem for Non-idempotent Intersection Types. In IFIP-TCS’14 (Lecture Notes in Computer Science), Josep Díaz, Ivan Lanese, and Davide Sangiorgi (Eds.), Vol. 8705. Springer, 341–354.Google Scholar
- Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017. Non-idempotent intersection types for the Lambda-Calculus. Logic Journal of the IGPL 25, 4 (2017), 431–464.Google ScholarCross Ref
- Alberto Carraro and Giulio Guerrieri. 2014. A Semantical and Operational Account of Call-by-Value Solvability. In FoSSaCS 2014 (Lecture Notes in Computer Science), Anca Muscholl (Ed.), Vol. 8412. Springer, 103–118.Google Scholar
- Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for lambda-terms. Archive for Mathematical Logic 19 (1978), 139–156.Google ScholarCross Ref
- Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 4 (1980), 685–693.Google ScholarCross Ref
- Vincent Danos and Laurent Regnier. 2004. Head Linear Reduction. Technical Report.Google Scholar
- Daniel de Carvalho. 2007. Sémantiques de la logique linéaire et temps de calcul. Thèse de Doctorat. Université Aix-Marseille II.Google Scholar
- Daniel de Carvalho. 2009. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs/0905.4251 (2009).Google Scholar
- Daniel de Carvalho. 2016. The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In CSL 2016, (LIPIcs), Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 41:1–41:19.Google Scholar
- Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. 2011. A semantic measure of the execution time in linear logic. Theoretical Computer Science 412, 20 (2011), 1884–1902. Google ScholarDigital Library
- Daniel de Carvalho and Lorenzo Tortora de Falco. 2016. A semantic account of strong normalization in linear logic. Information and Computation 248 (2016), 104–129. Google ScholarDigital Library
- Alejandro Díaz-Caro, Giulio Manzonetto, and Michele Pagani. 2013. Call-by-Value Non-determinism in a Linear Logic Type Discipline. In LFCS 2013 (Lecture Notes in Computer Science), Sergei N. Artëmov and Anil Nerode (Eds.), Vol. 7734. Springer, 164–178.Google ScholarCross Ref
- Andrej Dudenhefner and Jakob Rehof. 2017. Intersection type calculi of bounded dimension. In POPL’17, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 653–665. Google ScholarDigital Library
- Thomas Ehrhard. 2012. Collapsing non-idempotent intersection types. In CSL’12 (LIPIcs), Patrick Cégielski and Arnaud Durand (Eds.), Vol. 16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 259–273.Google Scholar
- Thomas Ehrhard and Giulio Guerrieri. 2016. The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In PPDP 2016. ACM, 174–187. Google ScholarDigital Library
- Philippa Gardner. 1994. Discovering Needed Reductions Using Type Theory. In TACS ’94 (Lecture Notes in Computer Science), Masami Hagiya and John C. Mitchell (Eds.), Vol. 789. Springer, 555–574. Google ScholarDigital Library
- Jean-Yves Girard. 1988. Normal functors, power series and the λ-calculus. Annals of Pure and Applied Logic 37 (1988), 129–177.Google ScholarCross Ref
- Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types. Cambridge University Press, New York, NY, USA. Google ScholarDigital Library
- Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. 2016. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In FSCD 2016 (LIPIcs), Delia Kesner and Brigitte Pientka (Eds.), Vol. 52. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 20:1–20:18.Google Scholar
- Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Resource Aware ML. In CAV 2012 (Lecture Notes in Computer Science), P. Madhusudan and Sanjit A. Seshia (Eds.), Vol. 7358. Springer, 781–786. Google ScholarDigital Library
- Jan Hoffmann and Martin Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential - A Static Inference of Polynomial Bounds for Functional Programs. In ESOP’10 (Lecture Notes in Computer Science), Andrew D. Gordon (Ed.), Vol. 6012. Springer, 287–306. Google ScholarDigital Library
- Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In POPL 2003, Alex Aiken and Greg Morrisett (Eds.). ACM, 185–197. Google ScholarDigital Library
- John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In POPL’96, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM, 410–423. Google ScholarDigital Library
- Steffen Jost, Pedro B. Vasconcelos, Mário Florido, and Kevin Hammond. 2017. Type-Based Cost Analysis for Lazy Functional Languages. Journal of Automated Reasoning 59, 1 (2017), 87–120. Google ScholarDigital Library
- Delia Kesner and Daniel Ventura. 2014. Quantitative Types for the Linear Substitution Calculus. In IFIP-TCS’14 (Lecture Notes in Computer Science), Josep Díaz, Ivan Lanese, and Davide Sangiorgi (Eds.), Vol. 8705. Springer, 296–310.Google Scholar
- Delia Kesner and Daniel Ventura. 2015. A Resource Aware Computational Interpretation for Herbelin’s Syntax. In ICTAC 2015 (Lecture Notes in Computer Science), Martin Leucker, Camilo Rueda, and Frank D. Valencia (Eds.), Vol. 9399. Springer, 388–403. Google ScholarDigital Library
- Delia Kesner and Pierre Vial. 2017. Types as Resources for Classical Natural Deduction. In FSCD 2017 (LIPIcs), Dale Miller (Ed.), Vol. 84. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 24:1–24:17.Google Scholar
- Delia Kesner, Andrés Viso, and Alejandro Ríos. 2018. Call-by-need, neededness and all that. In FoSSaCS’18 (Lecture Notes in Computer Science), Christel Baier and Ugo Dal Lago (Eds.), Vol. 10803. Springer, 241–257.Google Scholar
- Assaf J. Kfoury. 2000. A linearization of the Lambda-calculus and consequences. Journal of Logic and Computation 10, 3 (2000), 411–436.Google ScholarCross Ref
- Jan Willem Klop. 1980. Combinatory Reduction Systems. PhD thesis. Utrecht University.Google Scholar
- Jean-Louis Krivine. 1993. Lambda-calculus, types and models. Ellis Horwood. Google ScholarDigital Library
- Gianfranco Mascari and Marco Pedicini. 1994. Head Linear Reduction and Pure Proof Net Extraction. Theoretical Computer Science 135, 1 (1994), 111–137. Google ScholarDigital Library
- Damiano Mazza, Luc Pellissier, and Pierre Vial. 2018. Polyadic approximations, fibrations and intersection types. PACMPL 2, POPL (2018), 6:1–6:28. Google ScholarDigital Library
- Robin Milner. 2007. Local Bigraphs and Confluence: Two Conjectures. Electronic Notes in Theoretical Computer Science 175, 3 (2007), 65–73. Google ScholarDigital Library
- Peter Møller Neergaard and Harry G. Mairson. 2004. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In ICFP 2004, Chris Okasaki and Kathleen Fisher (Eds.). ACM, 138–149.Google Scholar
- C.-H. Luke Ong. 2017. Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In LICS 2017, Joel Ouaknine (Ed.). IEEE Computer Society, 1–12.Google Scholar
- Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. 2017. Essential and relational models. Mathematical Structures in Computer Science 27, 5 (2017), 626–650.Google ScholarCross Ref
- Garrel Pottinger. 1980. A Type Assignment for The Strongly Normalizable λ-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.). Academic Press, 561–578.Google Scholar
- Hugo R. Simões, Kevin Hammond, Mário Florido, and Pedro B. Vasconcelos. 2007. Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs. In TYPES 2006, Revised Selected Papers (Lecture Notes in Computer Science), Thorsten Altenkirch and Conor McBride (Eds.), Vol. 4502. Springer, 221–236.Google Scholar
- Pawel Urzyczyn. 1999. The Emptiness Problem for Intersection Types. Journal of Symbolic Logic 64, 3 (1999), 1195–1215.Google ScholarCross Ref
- Pawel Urzyczyn. 2009. Inhabitation of Low-Rank Intersection Types. In TLCA 2009 (Lecture Notes in Computer Science), Pierre-Louis Curien (Ed.), Vol. 5608. Springer, 356–370. Google ScholarDigital Library
- Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen, and Hongwei Xi. 1999. Perpetual Reductions in LambdaCalculus. Information and Computation 149, 2 (1999), 173–225. Google ScholarDigital Library
- Pedro B. Vasconcelos and Kevin Hammond. 2004. Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In IFL 2003, Revised Papers (Lecture Notes in Computer Science), Vol. 3145. Springer, 86–101. Google ScholarDigital Library
Index Terms
- Tight typings and split bounds
Recommendations
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Blame for all
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesSeveral programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0 and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, ...
Comments