{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,11]],"date-time":"2022-09-11T11:09:09Z","timestamp":1662894549530},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"\n We study the weak call-by-value \u03bb-calculus as a model for computational complexity theory and establish the natural measures for time and space \u2014 the number of beta-reduction steps and the size of the largest term in a computation \u2014 as reasonable measures with respect to the invariance thesis of Slot and van Emde Boas from 1984. More precisely, we show that, using those measures, Turing machines and the weak call-by-value \u03bb-calculus can simulate each other within a polynomial overhead in time and a constant factor overhead in space for all computations terminating in (encodings of) \u201dtrue\u201d or \u201dfalse\u201d. The simulation yields that standard complexity classes like\n P<\/jats:italic>\n ,\n NP<\/jats:italic>\n ,\n PSPACE<\/jats:italic>\n , or\n EXP<\/jats:italic>\n can be defined solely in terms of the \u03bb-calculus, but does not cover sublinear time or space.\n <\/jats:p>\n Note that our measures still have the well-known size explosion property, where the space measure of a computation can be exponentially bigger than its time measure. However, our result implies that this exponential gap disappears once complexity classes are considered instead of concrete computations.<\/jats:p>\n We consider this result a first step towards a solution for the long-standing open problem of whether the natural measures for time and space of the \u03bb-calculus are reasonable. Our proof for the weak call-by-value \u03bb-calculus is the first proof of reasonability (including both time and space) for a functional language based on natural measures and enables the formal verification of complexity-theoretic proofs concerning complexity classes, both on paper and in proof assistants.<\/jats:p>\n \n The proof idea relies on a hybrid of two simulation strategies of reductions in the weak call-by-value \u03bb-calculus by Turing machines, both of which are insufficient if taken alone. The first strategy is the most naive one in the sense that a reduction sequence is simulated precisely as given by the reduction rules; in particular, all substitutions are executed immediately. This simulation runs within a constant overhead in space, but the overhead in time might be exponential. The second strategy is heap-based and relies on structure sharing, similar to existing compilers of eager functional languages. This strategy only has a polynomial overhead in time, but the space consumption might require an additional factor of log\n n<\/jats:italic>\n , which is essentially due to the size of the pointers required for this strategy. Our main contribution is the construction and verification of a space-aware interleaving of the two strategies, which is shown to yield both a constant overhead in space\n and<\/jats:italic>\n a polynomial overhead in time.\n <\/jats:p>","DOI":"10.1145\/3371095","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-23","source":"Crossref","is-referenced-by-count":7,"title":["The weak call-by-value \u03bb-calculus is reasonable for both time and space"],"prefix":"10.1145","volume":"4","author":[{"given":"Yannick","family":"Forster","sequence":"first","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Fabian","family":"Kunze","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]},{"given":"Marc","family":"Roth","sequence":"additional","affiliation":[{"name":"Saarland University, Germany \/ M2CI, Germany \/ University of Oxford, UK"}]}],"member":"320","reference":[{"key":"key-10.1145\/3371095-1","unstructured":"Beniamino Accattoli. 2016. The Complexity of Abstract Machines. In Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE@FSCD 2016, Porto, Portugal, 23rd June 2016. 1–15."},{"key":"key-10.1145\/3371095-2","unstructured":"Beniamino Accattoli. 2018. (In)Efficiency and Reasonable Cost Models. Electr. Notes Theor. Comput. Sci. 338 (2018), 23–43."},{"key":"key-10.1145\/3371095-3","unstructured":"Beniamino Accattoli and Claudio Sacerdoti Coen. 2015. On the Relative Usefulness of Fireballs. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. 141–155."},{"key":"key-10.1145\/3371095-4","unstructured":"Beniamino Accattoli and Ugo Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA’12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan. 22–37."},{"key":"key-10.1145\/3371095-5","doi-asserted-by":"crossref","unstructured":"Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science 12, 1 (2016).","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"key-10.1145\/3371095-6","unstructured":"Beniamino Accattoli and Giulio Guerrieri. 2017. Implementing Open Call-by-Value. In Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers. 1–19."},{"key":"key-10.1145\/3371095-7","unstructured":"Andrea Asperti and Wilmer Ricciotti. 2015. A formalization of multi-tape Turing machines. Theoretical Computer Science 603 (Oct. 2015), 23–42."},{"key":"key-10.1145\/3371095-8","unstructured":"Andrea Asperti and Luca Roversi. 2002. Intuitionistic Light Affine Logic. ACM Trans. Comput. Log. 3, 1 (2002), 137–175."},{"key":"key-10.1145\/3371095-9","unstructured":"Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. 226–237."},{"key":"key-10.1145\/3371095-10","unstructured":"Nicolaas Govert De Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes Mathematicae (Proceedings), Vol. 75. Elsevier, 381–392. Issue 5."},{"key":"key-10.1145\/3371095-11","unstructured":"Ugo Dal Lago and Beniamino Accattoli. 2017. Encoding Turing Machines into the Deterministic Lambda-Calculus. CoRR abs\/1711.10078 (2017). arXiv: 1711.10078 http:\/\/arxiv.org\/abs\/1711.10078"},{"key":"key-10.1145\/3371095-12","unstructured":"Ugo Dal Lago and Simone Martini. 2008. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. 398, 1-3 (2008), 32–50."},{"key":"key-10.1145\/3371095-13","unstructured":"Ugo Dal Lago and Ulrich Schöpp. 2010. Functional Programming in Sublinear Space. 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. 205–225."},{"key":"key-10.1145\/3371095-14","unstructured":"Nachum Dershowitz and Evgenia Falkovich-Derzhavetz. 2015. The Invariance Thesis. Logical Methods in Computer Science (to appear) (2015). http:\/\/www.cs.tau.ac.il\/~nachumd\/papers\/InvarianceThesis.pdf"},{"key":"key-10.1145\/3371095-15","unstructured":"Yannick Forster, Fabian Kunze, and Marc Roth. 2017. The strong invariance thesis for a 𝜆-calculus. Workshop on Syntax and Semantics of Low-Level Languages (LOLA) (2017)."},{"key":"key-10.1145\/3371095-16","doi-asserted-by":"crossref","unstructured":"Yannick Forster, Fabian Kunze, and Maximilian Wuttke. 2019. Verified Programming of Turing Machines in Coq. (2019). https:\/\/github.com\/uds- psl\/tm- verification- framework\/","DOI":"10.1145\/3372885.3373816"},{"key":"key-10.1145\/3371095-17","unstructured":"Yannick Forster and Gert Smolka. 2017. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings. 189–206."},{"key":"key-10.1145\/3371095-18","unstructured":"Marco Gaboardi, Jean-Yves Marion, and Simona Ronchi Della Rocca. 2008. A logical account of PSPACE. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. 121–131."},{"key":"key-10.1145\/3371095-19","unstructured":"Fabian Kunze, Gert Smolka, and Yannick Forster. 2018. Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings. 264–283."},{"key":"key-10.1145\/3371095-20","unstructured":"Julia L. Lawall and Harry G. Mairson. 1996. Optimality and Inefficiency: What Isn’t a Cost Model of the Lambda Calculus?. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, Philadelphia, Pennsylvania, USA, May 24-26, 1996. 92–101."},{"key":"key-10.1145\/3371095-21","unstructured":"Michael Norrish. 2011. Mechanised Computability Theory. In Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings. 297–311."},{"key":"key-10.1145\/3371095-22","unstructured":"Gordon D. Plotkin. 1975. Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci. 1, 2 (1975), 125–159."},{"key":"key-10.1145\/3371095-23","unstructured":"Patrick M. Sansom and Simon L. Peyton Jones. 1995. Time and Space Profiling for Non-Strict Higher-Order Functional Languages. In Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995. 355–366."},{"key":"key-10.1145\/3371095-24","unstructured":"Ulrich Schöpp. 2006. Space-Efficient Computation by Interaction. In Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings. 606–621."},{"key":"key-10.1145\/3371095-25","unstructured":"Cees F. Slot and Peter van Emde Boas. 1984. On Tape Versus Core; An Application of Space Efficient Perfect Hash Functions to the Invariance of Space. In Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1984, Washington, DC, USA. 391–400."},{"key":"key-10.1145\/3371095-26","unstructured":"Daniel Spoonhower, Guy E. Blelloch, Robert Harper, and Phillip B. Gibbons. 2008. Space profiling for parallel functional programs. J. Funct. Program. 20, 5-6 (2008), 417–461."},{"key":"key-10.1145\/3371095-27","unstructured":"The Coq Proof Assistant. 2019. http:\/\/coq.inria.fr ."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371095","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,6]],"date-time":"2021-10-06T06:19:54Z","timestamp":1633501194000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371095"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":27,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371095"],"URL":"http:\/\/dx.doi.org\/10.1145\/3371095","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":["Safety, Risk, Reliability and Quality","Software"],"published":{"date-parts":[[2020,1]]}}}