Sharing a Perspective on the 𝜆-Calculus
Pages 179 - 190
Abstract
The λ-calculus models the core of functional programming languages. This essay discusses a gap between the theory of the λ-calculus and functional languages, namely the fact that the former does not give a status to sharing, the essential ingredient for efficiency in the lattter.
The essay provides an overview of the perspective of the author, who has been and still is studying sharing from various angles. In particular, it explains how sharing impacts the equational and denotational semantics of the λ-calculus, breaking some expected properties, and demanding the development of new, richer semantics of the λ-calculus.
References
[1]
Samson Abramsky, Kohei Honda, and Guy McCusker. 1998. A Fully Abstract Game Semantics for General References. In Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998. IEEE Computer Society, 334–344. https://doi.org/10.1109/LICS.1998.705669
[2]
Samson Abramsky and Guy McCusker. 1997. Call-by-Value Games. In Computer Science Logic, 11th International Workshop, CSL ’97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers, Mogens Nielsen and Wolfgang Thomas (Eds.) (Lecture Notes in Computer Science, Vol. 1414). Springer, 1–17. https://doi.org/10.1007/BFb0028004
[3]
Samson Abramsky and C.-H. Luke Ong. 1993. Full Abstraction in the Lazy Lambda Calculus. Inf. Comput., 105, 2 (1993), 159–267. https://doi.org/10.1006/inco.1993.1044
[4]
Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA’12), RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, Ashish Tiwari (Ed.) (LIPIcs, Vol. 15). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 6–21. https://doi.org/10.4230/LIPIcs.RTA.2012.6
[5]
Beniamino Accattoli. 2015. Proof nets and the call-by-value λ -calculus. Theor. Comput. Sci., 606 (2015), 2–24. https://doi.org/10.1016/j.tcs.2015.08.006
[6]
Beniamino Accattoli. 2018. Proof Nets and the Linear Substitution Calculus. In Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings, Bernd Fischer and Tarmo Uustalu (Eds.) (Lecture Notes in Computer Science, Vol. 11187). Springer, 37–61. https://doi.org/10.1007/978-3-030-02508-3_3
[7]
Beniamino Accattoli. 2019. A Fresh Look at the lambda-Calculus (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, Herman Geuvers (Ed.) (LIPIcs, Vol. 131). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1:1–1:20. https://doi.org/10.4230/LIPIcs.FSCD.2019.1
[8]
Beniamino Accattoli. 2022. Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, Christel Baier and Dana Fisman (Eds.). ACM, 49:1–49:15. https://doi.org/10.1145/3531130.3532445
[9]
Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2014. Distilling abstract machines. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 363–376. https://doi.org/10.1145/2628136.2628154
[10]
Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. 2014. A nonstandard standardization theorem. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 659–670. https://doi.org/10.1145/2535838.2535886
[11]
Beniamino Accattoli, Andrea Condoluci, and Claudio Sacerdoti Coen. 2021. Strong Call-by-Value is Reasonable, Implosively. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 1–14. https://doi.org/10.1109/LICS52264.2021.9470630
[12]
Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019. Crumbling Abstract Machines. In Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, Ekaterina Komendantskaya (Ed.). ACM, 4:1–4:15. https://doi.org/10.1145/3354166.3354169
[13]
Beniamino Accattoli and Ugo Dal Lago. 2014. Beta reduction is invariant, indeed. In 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, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 8:1–8:10. https://doi.org/10.1145/2603088.2603105
[14]
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2022. Reasonable Space for the λ -Calculus, Logarithmically. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, Christel Baier and Dana Fisman (Eds.). ACM, 47:1–47:13. https://doi.org/10.1145/3531130.3533362
[15]
Beniamino Accattoli, Claudia Faggian, and Adrienne Lancelot. 2023. Normal Form Bisimulations By Value. CoRR, abs/2303.08161 (2023), https://doi.org/10.48550/arXiv.2303.08161 arXiv:2303.08161.
[16]
Beniamino Accattoli and Giulio Guerrieri. 2016. Open Call-by-Value. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, Atsushi Igarashi (Ed.) (Lecture Notes in Computer Science, Vol. 10017). 206–226. https://doi.org/10.1007/978-3-319-47958-3_12
[17]
Beniamino Accattoli and Giulio Guerrieri. 2019. Abstract machines for Open Call-by-Value. Sci. Comput. Program., 184 (2019), https://doi.org/10.1016/j.scico.2019.03.002
[18]
Beniamino Accattoli and Giulio Guerrieri. 2022. The theory of call-by-value solvability. Proc. ACM Program. Lang., 6, ICFP (2022), 855–885. https://doi.org/10.1145/3547652
[19]
Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. 2019. Types by Need. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, LuĂs Caires (Ed.) (Lecture Notes in Computer Science, Vol. 11423). Springer, 410–439. https://doi.org/10.1007/978-3-030-17184-1_15
[20]
Beniamino Accattoli and Delia Kesner. 2010. The Structural lambda-Calculus. In Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, Anuj Dawar and Helmut Veith (Eds.) (Lecture Notes in Computer Science, Vol. 6247). Springer, 381–395. https://doi.org/10.1007/978-3-642-15205-4_30
[21]
Beniamino Accattoli and Maico Leberle. 2022. Useful Open Call-By-Need. In 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), Florin Manea and Alex Simpson (Eds.) (LIPIcs, Vol. 216). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 4:1–4:21. https://doi.org/10.4230/LIPIcs.CSL.2022.4
[22]
Beniamino Accattoli and Luca Paolini. 2012. Call-by-Value Solvability, Revisited. In Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, Tom Schrijvers and Peter Thiemann (Eds.) (Lecture Notes in Computer Science, Vol. 7294). Springer, 4–16. https://doi.org/10.1007/978-3-642-29822-6_4
[23]
Zena M. Ariola and Matthias Felleisen. 1997. The Call-By-Need lambda Calculus. J. Funct. Program., 7, 3 (1997), 265–301. https://doi.org/10.1017/s0956796897002724
[24]
Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. 2017. Foundations of strong call by need. Proc. ACM Program. Lang., 1, ICFP (2017), 20:1–20:29. https://doi.org/10.1145/3110264
[25]
Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics, Vol. 103). North-Holland. isbn:978-0-444-86748-3
[26]
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, John Williams (Ed.). ACM, 226–237. https://doi.org/10.1145/224164.224210
[27]
Alberto Carraro and Giulio Guerrieri. 2014. A Semantical and Operational Account of Call-by-Value Solvability. In Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Anca Muscholl (Ed.) (Lecture Notes in Computer Science, Vol. 8412). Springer, 103–118. https://doi.org/10.1007/978-3-642-54830-7_7
[28]
Pierre Clairambault and Marc de Visme. 2020. Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang., 4, POPL (2020), 63:1–63:28. https://doi.org/10.1145/3371131
[29]
Pierre-Louis Curien and Hugo Herbelin. 2000. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, 233–243. https://doi.org/10.1145/351240.351262
[30]
Vincent Danos, Hugo Herbelin, and Laurent Regnier. 1996. Game Semantics & Abstract Machines. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. IEEE Computer Society, 394–405. https://doi.org/10.1109/LICS.1996.561456
[31]
Daniel de Carvalho. 2018. Execution time of λ -terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28, 7 (2018), 1169–1203. https://doi.org/10.1017/S0960129516000396
[32]
Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. 1992. Operational, denotational and logical descriptions: a case study. Fundam. Inform., 16, 1 (1992), 149–169.
[33]
Thomas Ehrhard. 2012. Collapsing non-idempotent intersection types. In Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, Patrick Cégielski and Arnaud Durand (Eds.) (LIPIcs, Vol. 16). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 259–273. https://doi.org/10.4230/LIPIcs.CSL.2012.259
[34]
Thomas Ehrhard and Giulio Guerrieri. 2016. The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, James Cheney and Germán Vidal (Eds.). ACM, 174–187. https://doi.org/10.1145/2967973.2968608
[35]
Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci., 50 (1987), 1–102. https://doi.org/10.1016/0304-3975(87)90045-4
[36]
Timothy Griffin. 1990. A Formulae-as-Types Notion of Control. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, Frances E. Allen (Ed.). ACM Press, 47–58. https://doi.org/10.1145/96709.96714
[37]
Kohei Honda and Nobuko Yoshida. 1999. Game-Theoretic Analysis of Call-by-Value Computation. Theor. Comput. Sci., 221, 1-2 (1999), 393–456. https://doi.org/10.1016/S0304-3975(99)00039-0
[38]
Delia Kesner. 2016. Reasoning About Call-by-need by Means of Types. In Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Bart Jacobs and Christof Löding (Eds.) (Lecture Notes in Computer Science, Vol. 9634). Springer, 424–441. https://doi.org/10.1007/978-3-662-49630-5_25
[39]
Delia Kesner, Loïc Peyrot, and Daniel Ventura. 2021. The Spirit of Node Replication. In Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 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, Stefan Kiefer and Christine Tasson (Eds.) (Lecture Notes in Computer Science, Vol. 12650). Springer, 344–364. https://doi.org/10.1007/978-3-030-71995-1_18
[40]
Vasileios Koutavas, Yu-Yang Lin, and Nikos Tzevelekos. 2023. Fully Abstract Normal Form Bisimulation for Call-by-Value PCF. In LICS. 1–13. https://doi.org/10.1109/LICS56636.2023.10175778
[41]
John Launchbury. 1993. A Natural Semantics for Lazy Evaluation. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, Mary S. Van Deusen and Bernard Lang (Eds.). ACM Press, 144–154. https://doi.org/10.1145/158511.158618
[42]
Olivier Laurent. 2002. https://dumas.ccsd.cnrs.fr/IML/tel-00007884 Université Aix-Marseille II.
[43]
Paul Blain Levy. 2006. Call-by-push-value: Decomposing call-by-value and call-by-name. High. Order Symb. Comput., 19, 4 (2006), 377–414. https://doi.org/10.1007/s10990-006-0480-6
[44]
Giuseppe Longo. 1983. Set-theoretical models of λ -calculus: theories, expansions, isomorphisms. Ann. Pure Appl. Log., 24, 2 (1983), 153–188. https://doi.org/10.1016/0168-0072(83)90030-1
[45]
Giulio Manzonetto. 2009. A General Class of Models of H^ *. In Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings, Rastislav Královic and Damian Niwinski (Eds.) (Lecture Notes in Computer Science, Vol. 5734). Springer, 574–586. https://doi.org/10.1007/978-3-642-03816-7_49
[46]
Giulio Manzonetto, Michele Pagani, and Simona Ronchi Della Rocca. 2019. New Semantical Insights Into Call-by-Value λ -Calculus. Fundam. Informaticae, 170, 1-3 (2019), 241–265. https://doi.org/10.3233/FI-2019-1862
[47]
John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. 1999. Call-by-name, Call-by-value, Call-by-need and the Linear lambda Calculus. Theor. Comput. Sci., 228, 1-2 (1999), 175–210. https://doi.org/10.1016/S0304-3975(98)00358-2
[48]
John Maraist, Martin Odersky, and Philip Wadler. 1998. The Call-by-Need Lambda Calculus. J. Funct. Program., 8, 3 (1998), 275–317. https://doi.org/10.1017/s0956796898003037
[49]
Paul-André Melliès. 1995. Typed lambda-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA ’95, Edinburgh, UK, April 10-12, 1995, Proceedings, Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin (Eds.) (Lecture Notes in Computer Science, Vol. 902). Springer, 328–334. https://doi.org/10.1007/BFb0014062
[50]
Robin Milner. 2006. Local Bigraphs and Confluence: Two Conjectures: (Extended Abstract). In Proceedings of the 13th International Workshop on Expressiveness in Concurrency, EXPRESS 2006, Bonn, Germany, August 26, 2006, Roberto M. Amadio and Iain Phillips (Eds.) (Electronic Notes in Theoretical Computer Science, Vol. 175). Elsevier, 65–73. https://doi.org/10.1016/j.entcs.2006.07.035
[51]
James Hiram Morris. 1968. https://books.google.is/books?id=DklAAQAAIAAJ Ph. D. Dissertation. MIT.
[52]
Reiji Nakajima. 1975. Infinite normal forms for the lambda - calculus. In Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, Italy, March 25-27, 1975, Corrado Böhm (Ed.) (Lecture Notes in Computer Science, Vol. 37). Springer, 62–82. https://doi.org/10.1007/BFb0029519
[53]
Andrew M. Pitts. 2012. Howe’s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan J. M. M. Rutten (Eds.) (Cambridge tracts in theoretical computer science, Vol. 52). Cambridge University Press, 197–232. https://doi.org/10.1017/CBO9780511792588.006
[54]
Gordon D. Plotkin. 1975. Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci., 1, 2 (1975), 125–159. https://doi.org/10.1016/0304-3975(75)90017-1
[55]
Peter Sestoft. 1997. Deriving a Lazy Abstract Machine. J. Funct. Program., 7, 3 (1997), 231–264. https://doi.org/10.1017/s0956796897002712
[56]
Christopher P. Wadsworth. 1971. https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.476186 Oxford.
Index Terms
- Sharing a Perspective on the 𝜆-Calculus
Recommendations
Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer ApplicationsThe Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional ...
Two-level Lambda-calculus
Two-level lambda-calculus is designed to provide a mathematical model of capturing substitution, also called instantiation. Instantiation is a feature of the 'informal meta-level'; it appears pervasively in specifications of the syntax and semantics of ...
Topological incompleteness and order incompleteness of the lambda calculus
A model of the untyped lambda calculus univocally induces a lambda theory (i.e., a congruence relation on λ-terms closed under α- and β-conversion) through the kernel congruence relation of the interpretation function. A semantics of lambda calculus is (...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
204 pages
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 19 October 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
Onward! '23
Sponsor:
Onward! '23: 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
October 25 - 27, 2023
Cascais, Portugal
Acceptance Rates
Overall Acceptance Rate 40 of 105 submissions, 38%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 99Total Downloads
- Downloads (Last 12 months)99
- Downloads (Last 6 weeks)6
Reflects downloads up to 26 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in