Document Open Access Logo

A Fresh Look at the lambda-Calculus (Invited Talk)

Author Beniamino Accattoli

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.1.pdf
  • Filesize: 477 kB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Software and its engineering → Functional languages
  • Theory of computation → Operational semantics
Keywords
  • lambda-calculus
  • sharing
  • abstract machines
  • type systems
  • rewriting

Metrics

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

Abstract

The (untyped) lambda-calculus is almost 90 years old. And yet - we argue here - its study is far from being over. The paper is a bird’s eye view of the questions the author worked on in the last few years: how to measure the complexity of lambda-terms, how to decompose their evaluation, how to implement it, and how all this varies according to the evaluation strategy. The paper aims at inducing a new way of looking at an old topic, focussing on high-level issues and perspectives.

Cite As Get BibTex

Beniamino Accattoli. A Fresh Look at the lambda-Calculus (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.1

Author Details

Beniamino Accattoli
  • Inria & LIX, École Polytechnique, UMR 7161, France

Funding

  • Accattoli, Beniamino: This work has been partially funded by the ANR JCJC grant COCA HOLA (ANR-16-CE40-004-01).

Acknowledgements

To Herman Geuvers, Giulio Guerrieri, and Gabriel Scherer for comments on a first draft.

References

  1. Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit Substitutions. J. Funct. Program., 1(4):375-416, 1991. URL: http://dx.doi.org/10.1017/S0956796800000186.
  2. Samson Abramsky and C.-H. Luke Ong. Full Abstraction in the Lazy Lambda Calculus. Inf. Comput., 105(2):159-267, 1993. Google Scholar
  3. Beniamino Accattoli. An Abstract Factorization Theorem for Explicit Substitutions. In RTA, pages 6-21, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2012.6.
  4. Beniamino Accattoli. Evaluating functions as processes. In TERMGRAPH, pages 41-55, 2013. URL: http://dx.doi.org/10.4204/EPTCS.110.6.
  5. Beniamino Accattoli. Proof nets and the call-by-value λ-calculus. Theor. Comput. Sci., 606:2-24, 2015. URL: http://dx.doi.org/10.1016/j.tcs.2015.08.006.
  6. Beniamino Accattoli. The Complexity of Abstract Machines. In WPTE@FSCD 2016, pages 1-15, 2016. URL: http://dx.doi.org/10.4204/EPTCS.235.1.
  7. Beniamino Accattoli. The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus. In WoLLIC 2016, pages 1-21, 2016. URL: http://dx.doi.org/10.1007/978-3-662-52921-8_1.
  8. Beniamino Accattoli. Proof Nets and the Linear Substitution Calculus. In ICTAC 2018, pages 37-61, 2018. URL: http://dx.doi.org/10.1007/978-3-030-02508-3_3.
  9. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In ICFP 2014, pages 363-376, 2014. URL: http://dx.doi.org/10.1145/2628136.2628154.
  10. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A Strong Distillery. In APLAS 2015, pages 231-250, 2015. URL: http://dx.doi.org/10.1007/978-3-319-26529-2_13.
  11. Beniamino Accattoli and Bruno Barras. Environments and the complexity of abstract machines. In PPDP 2017, pages 4-16, 2017. URL: http://dx.doi.org/10.1145/3131851.3131855.
  12. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. 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, pages 659-670, 2014. URL: http://dx.doi.org/10.1145/2535838.2535886.
  13. Beniamino Accattoli and Claudio Sacerdoti Coen. On the Relative Usefulness of Fireballs. In LICS 2015, pages 141-155, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.23.
  14. Beniamino Accattoli and Claudio Sacerdoti Coen. On the value of variables. Inf. Comput., 255:224-242, 2017. URL: http://dx.doi.org/10.1016/j.ic.2017.01.003.
  15. Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. Crumbling Abstract Machines. Submitted, 2019. Google Scholar
  16. Beniamino Accattoli and Ugo Dal Lago. On the Invariance of the Unitary Cost Model for Head Reduction. In RTA, pages 22-37, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2012.22.
  17. Beniamino Accattoli and Ugo Dal Lago. Beta reduction is invariant, indeed. In CSL-LICS '14, pages 8:1-8:10, 2014. URL: http://dx.doi.org/10.1145/2603088.2603105.
  18. Beniamino Accattoli and Ugo Dal Lago. (Leftmost-Outermost) Beta-Reduction is Invariant, Indeed. Logical Methods in Computer Science, 12(1), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(1:4)2016.
  19. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1-94:30, 2018. URL: http://dx.doi.org/10.1145/3236789.
  20. Beniamino Accattoli and Giulio Guerrieri. Open Call-by-Value. In APLAS 2016, pages 206-226, 2016. URL: http://dx.doi.org/10.1007/978-3-319-47958-3_12.
  21. Beniamino Accattoli and Giulio Guerrieri. Implementing Open Call-by-Value. In FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers, pages 1-19, 2017. URL: http://dx.doi.org/10.1007/978-3-319-68972-2_1.
  22. Beniamino Accattoli and Giulio Guerrieri. Types of Fireballs. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, pages 45-66, 2018. URL: http://dx.doi.org/10.1007/978-3-030-02768-1_3.
  23. Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. 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, pages 410-439, 2019. URL: http://dx.doi.org/10.1007/978-3-030-17184-1_15.
  24. Beniamino Accattoli and Luca Paolini. Call-by-Value Solvability, revisited. In FLOPS, pages 4-16, 2012. URL: http://dx.doi.org/10.1007/978-3-642-29822-6_4.
  25. Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The Call-by-Need Lambda Calculus. In POPL'95, pages 233-246, 1995. URL: http://dx.doi.org/10.1145/199448.199507.
  26. Federico Aschieri. Game Semantics and the Geometry of Backtracking: a New Complexity Analysis of Interaction. J. Symb. Log., 82(2):672-708, 2017. URL: http://dx.doi.org/10.1017/jsl.2016.48.
  27. Andrea Asperti and Harry G. Mairson. Parallel Beta Reduction is not Elementary Recursive. In POPL, pages 303-315, 1998. URL: http://dx.doi.org/10.1145/268946.268971.
  28. Patrick Baillot. Stratified coherence spaces: a denotational semantics for light linear logic. Theor. Comput. Sci., 318(1-2):29-55, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2003.10.015.
  29. Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. Foundations of strong call by need. PACMPL, 1(ICFP):20:1-20:29, 2017. URL: http://dx.doi.org/10.1145/3110264.
  30. Pablo Barenbaum and Eduardo Bonelli. Optimality and the Linear Substitution Calculus. In FSCD 2017, pages 9:1-9:16, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.9.
  31. Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  32. Guy E. Blelloch and John Greiner. Parallelism in Sequential Functional Languages. In FPCA, pages 226-237, 1995. URL: http://dx.doi.org/10.1145/224164.224210.
  33. Alberto Carraro and Giulio Guerrieri. 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, pages 103-118, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_7.
  34. Pierre Clairambault. Estimation of the Length of Interactions in Arena Game Semantics. In FOSSACS, pages 335-349, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19805-2_23.
  35. Pierre Clairambault. Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction. In TLCA, pages 109-124, 2013. URL: http://dx.doi.org/10.1007/978-3-642-38946-7_10.
  36. Pierre Crégut. An Abstract Machine for Lambda-Terms Normalization. In LISP and Functional Programming, pages 333-340, 1990. Google Scholar
  37. Pierre Crégut. Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation, 20(3):209-230, 2007. URL: http://dx.doi.org/10.1007/s10990-007-9015-z.
  38. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In ICFP, pages 233-243, 2000. URL: http://dx.doi.org/10.1145/351240.351262.
  39. Ugo Dal Lago and Simone Martini. An Invariant Cost Model for the Lambda Calculus. In CiE 2006, pages 105-114, 2006. URL: http://dx.doi.org/10.1007/11780342_11.
  40. Ugo Dal Lago and Simone Martini. Derivational Complexity Is an Invariant Cost Model. In FOPARA 2009, pages 100-113, 2009. URL: http://dx.doi.org/10.1007/978-3-642-15331-0_7.
  41. Ugo Dal Lago and Simone Martini. On Constructor Rewrite Systems and the Lambda-Calculus. In ICALP (2), pages 163-174, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02930-1_14.
  42. Vincent Danos, Hugo Herbelin, and Laurent Regnier. Game Semantics & Abstract Machines. In LICS, pages 394-405, 1996. URL: http://dx.doi.org/10.1109/LICS.1996.561456.
  43. Vincent Danos and Laurent Regnier. Reversible, Irreversible and Optimal lambda-Machines. Theor. Comput. Sci., 227(1-2):79-97, 1999. URL: http://dx.doi.org/10.1016/S0304-3975(99)00049-3.
  44. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2018. URL: http://dx.doi.org/10.1017/S0960129516000396.
  45. Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A semantic measure of the execution time in linear logic. Theor. Comput. Sci., 412(20):1884-1902, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2010.12.017.
  46. Roy Dyckhoff and Stéphane Lengrand. Call-by-Value lambda-calculus and LJQ. J. Log. Comput., 17(6):1109-1134, 2007. URL: http://dx.doi.org/10.1093/logcom/exm037.
  47. Thomas Ehrhard. Collapsing non-idempotent intersection types. In CSL, pages 259-273, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2012.259.
  48. Dan R. Ghica. Slot games: a quantitative model of computation. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 85-97, 2005. URL: http://dx.doi.org/10.1145/1040305.1040313.
  49. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50:1-102, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  50. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In (ICFP '02)., pages 235-246, 2002. URL: http://dx.doi.org/10.1145/581478.581501.
  51. Hugo Herbelin and Stéphane Zimmermann. An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. In TLCA, pages 142-156, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02273-9_12.
  52. Andrew Kennedy. Compiling with continuations, continued. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 177-190, 2007. URL: http://dx.doi.org/10.1145/1291151.1291179.
  53. Delia Kesner. Reasoning About Call-by-need by Means of Types. In FOSSACS 2016, pages 424-441, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49630-5_25.
  54. Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood series in computers and their applications. Masson, 1993. Google Scholar
  55. Arne Kutzner and Manfred Schmidt-Schauß. A Non-Deterministic Call-by-Need Lambda Calculus. In ICFP 1998, pages 324-335, 1998. URL: http://dx.doi.org/10.1145/289423.289462.
  56. Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo, and Akira Yoshimizu. The geometry of synchronization. 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, pages 35:1-35:10, 2014. URL: http://dx.doi.org/10.1145/2603088.2603154.
  57. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. Parallelism and Synchronization in an Infinitary Context. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 559-572, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.58.
  58. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The geometry of parallelism: classical, probabilistic, and quantum effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 833-845, 2017. URL: http://dl.acm.org/citation.cfm?id=3009859.
  59. Ugo Dal Lago and Martin Hofmann. Quantitative Models and Implicit Complexity. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Hyderabad, India, December 15-18, 2005, Proceedings, pages 189-200, 2005. URL: http://dx.doi.org/10.1007/11590156_15.
  60. Ugo Dal Lago and Olivier Laurent. Quantitative Game Semantics for Linear Logic. In Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, pages 230-245, 2008. URL: http://dx.doi.org/10.1007/978-3-540-87531-4_18.
  61. Ugo Dal Lago and Simone Martini. On Constructor Rewrite Systems and the Lambda Calculus. Logical Methods in Computer Science, 8(3), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:12)2012.
  62. Ugo Dal Lago, Ryo Tanaka, and Akira Yoshimizu. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005112.
  63. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted Relational Models of Typed Lambda-Calculi. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 301-310, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.36.
  64. John Lamping. An Algorithm for Optimal Lambda Calculus Reduction. In POPL, pages 16-30, 1990. URL: http://dx.doi.org/10.1145/96709.96711.
  65. John Launchbury. A Natural Semantics for Lazy Evaluation. In POPL, pages 144-154, 1993. URL: http://dx.doi.org/10.1145/158511.158618.
  66. Olivier Laurent and Lorenzo Tortora de Falco. Obsessional Cliques: A Semantic Characterization of Bounded Time Complexity. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 179-188, 2006. URL: http://dx.doi.org/10.1109/LICS.2006.37.
  67. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. Thése d'Etat, Univ. Paris VII, France, 1978. Google Scholar
  68. Jean-Jacques Lévy and Luc Maranget. Explicit Substitutions and Programming Languages. In Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings, pages 181-200, 1999. URL: http://dx.doi.org/10.1007/3-540-46691-6_14.
  69. Ian Mackie. The Geometry of Interaction Machine. In Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 198-208, 1995. URL: http://dx.doi.org/10.1145/199448.199483.
  70. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, Call-by-value, Call-by-need and the Linear lambda Calculus. Theor. Comput. Sci., 228(1-2):175-210, 1999. URL: http://dx.doi.org/10.1016/S0304-3975(98)00358-2.
  71. John Maraist, Martin Odersky, and Philip Wadler. The Call-by-Need Lambda Calculus. J. Funct. Program., 8(3):275-317, 1998. URL: http://journals.cambridge.org/action/displayAbstract?aid=44169.
  72. Damiano Mazza. Simple Parsimonious Types and Logarithmic Space. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), volume 41 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24-40, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.24.
  73. Robin Milner. Functions as Processes. Math. Str. in Comput. Sci., 2(2):119-141, 1992. URL: http://dx.doi.org/10.1017/S0960129500001407.
  74. Robin Milner. Local Bigraphs and Confluence: Two Conjectures. Electr. Notes Theor. Comput. Sci., 175(3):65-73, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2006.07.035.
  75. Robin Milner, Joachim Parrow, and David Walker. A Calculus of Mobile Processes, I. Inf. Comput., 100(1):1-40, 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90008-4.
  76. Eugenio Moggi. Computational λ-Calculus and Monads. In LICS '89, pages 14-23, 1989. Google Scholar
  77. Andrzej S. Murawski and C.-H. Luke Ong. Discreet Games, Light Affine Logic and PTIME Computation. In Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings, pages 427-441, 2000. URL: http://dx.doi.org/10.1007/3-540-44622-2_29.
  78. Koko Muroya and Dan R. Ghica. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In CSL 2017, pages 32:1-32:15, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.32.
  79. Luca Paolini. Call-by-Value Separability and Computability. In ICTCS, pages 74-89, 2001. URL: http://dx.doi.org/10.1007/3-540-45446-2_5.
  80. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value Solvability. ITA, 33(6):507-534, 1999. URL: http://dx.doi.org/10.1051/ita:1999130.
  81. Gordon D. Plotkin. Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: http://dx.doi.org/10.1016/0304-3975(75)90017-1.
  82. Simona Ronchi Della Rocca and Luca Paolini. The Parametric λ-Calculus. Springer Berlin Heidelberg, 2004. Google Scholar
  83. Amr Sabry and Matthias Felleisen. Reasoning about Programs in Continuation-Passing Style. Lisp and Symbolic Computation, 6(3-4):289-360, 1993. URL: http://dx.doi.org/10.1007/BF01019462.
  84. Amr Sabry and Philip Wadler. A Reflection on Call-by-Value. ACM Trans. Program. Lang. Syst., 19(6):916-941, 1997. URL: http://dx.doi.org/10.1145/267959.269968.
  85. David Sands, Jörgen Gustavsson, and Andrew Moran. Lambda Calculi and Linear Speedups. In The Essence of Computation, pages 60-84, 2002. URL: http://dx.doi.org/10.1007/3-540-36377-7_4.
  86. Ulrich Schöpp. Space-Efficient Computation by Interaction. In CSL 2006, pages 606-621, 2006. URL: http://dx.doi.org/10.1007/11874683_40.
  87. Peter Sestoft. Deriving a Lazy Abstract Machine. J. Funct. Program., 7(3):231-264, 1997. URL: http://journals.cambridge.org/action/displayAbstract?aid=44087.
  88. Cees F. Slot and Peter van Emde Boas. On Tape Versus Core; An Application of Space Efficient Perfect Hash Functions to the Invariance of Space. In STOC 1984, pages 391-400, 1984. URL: http://dx.doi.org/10.1145/800057.808705.
  89. Christopher P. Wadsworth. Semantics and pragmatics of the lambda-calculus. PhD Thesis, Oxford, 1971. 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