Abstract
We present the spinal atomic \(\lambda \)-calculus, a typed \(\lambda \)-calculus with explicit sharing and atomic duplication that achieves spinal full laziness: duplicating only the direct paths between a binder and bound variables is enough for beta reduction to proceed. We show this calculus is the result of a Curry–Howard style interpretation of a deep-inference proof system, and prove that it has natural properties with respect to the \(\lambda \)-calculus: confluence and preservation of strong normalisation.
This work was supported by EPSRC Project EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing and ANR project 15-CE25-0014 The Fine Structure of Formal Proof Systems and their Computational Interpretations (FISP).
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991)
Accattoli, B., Kesner, D.: Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science 8(1) (2012)
Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge University Press (1998)
Balabonski, T.: A unified approach to fully lazy sharing. ACM SIGPLAN Notices 47(1), 469–480 (2012)
Balabonski, T.: Weak Optimality, and the Meaning of Sharing. In: International Conference on Functional Programming (ICFP). pp. 263–274. Boston, United States (Sep 2013). https://doi.org/10.1145/2500365.2500606, https://hal.archives-ouvertes.fr/hal-00907056
Barendregt, H.P.: The Lambda Calculus – Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland (1984)
Berkling, K.J., Fehr, E.: A consistent extension of the lambda-calculus as a base for functional programming languages. Information and Control 55, 89–101 (1982)
Blanc, T., Lévy, J.J., Maranget, L.: Sharing in the weak lambda-calculus. Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday 3838, 70 (2005)
Brünnler, K., McKinley, R.: An algorithmic interpretation of a deep inference system. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). pp. 482–496 (2008)
Brünnler, K., Tiu, A.: A local system for classical logic. In: 8th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). LNCS, vol. 2250, pp. 347–361 (2001)
Church, A., Rosser, J.B.: Some properties of conversion. Transactions of the American Mathematical Society 39(3), 472–482 (1936), http://www.jstor.org/stable/1989762
Cockett, R., Seely, R.: Weakly distributive categories. Journal of Pure and Applied Algebra 114(2), 133–173 (1997)
Fernández, M., Mackie, I., Sinot, F.R.: Lambda-calculus with director strings. Applicable Algebra in Engineering, Communication and Computing 15(6), 393–437 (2005)
Guenot, N., Straßburger, L.: Symmetric normalisation for intuitionistic logic. 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) (2014)
Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: 21st International Conference on Rewriting Techniques and Applications (RTA). pp. 135–150 (2010)
Gundersen, T., Heijltjes, W., Parigot, M.: Atomic lambda-calculus: a typed lambda-calculus with explicit sharing. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 311–320 (2013)
He, F.: The Atomic Lambda-Mu Calculus. Ph.D. thesis, University of Bath (2018)
Hendriks, D., van Oostrom, V.: Adbmal. In: 19th International Conference on Automated Deduction (CADE). LNCS, vol. 2741, pp. 136–150 (2003)
Kennaway, R., Sleep, R.: Director strings as combinators. ACM Transactions on Programming Languages and Systems (1988)
Klop, J.W.: Combinatory Reduction Systems. Ph.D. thesis, Utrecht University (1980)
Lamping, J.: An algorithm for optimal lambda calculus reduction. In: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 16–30 (1990)
Launchbury, J.: A natural semantics for lazy evaluation. In: 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL). pp. 144–154 (1993)
Lévy, J.J.: Optimal reductions in the lambda-calculus. In: To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism. Academic Press (1980)
van Oostrom, V., van de Looij, K.J., Zwitserlood, M.: Lambdascope: another optimal implementation of the lambda-calculus. In: Workshop on Algebra and Logic on Programming Systems (ALPS) (2004)
Sherratt, D.R.: A lambda-calculus that achieves full laziness with spine duplication. Ph.D. thesis, University of Bath (2019)
Tiu, A.: A local system for intuitionistic logic. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). pp. 242–256 (2006)
Wadsworth, C.P.: Semantics and Pragmatics of the Lambda-Calculus. Ph.D. thesis, University of Oxford (1971)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Sherratt, D., Heijltjes, W., Gundersen, T., Parigot, M. (2020). Spinal Atomic Lambda-Calculus. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_30
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_30
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)