Abstract
In each variant of the \(\lambda \)-calculus, factorization and normalization are two key properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the \(\lambda \)-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV.
The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.
Chapter PDF
Similar content being viewed by others
References
Accattoli, B.: An Abstract Factorization Theorem for Explicit Substitutions. In: 23rd International Conference on Rewriting Techniques and Applications (RTA’12). Leibniz International Proceedings in Informatics (LIPIcs), vol. 15, pp. 6–21. Schloss Dagstuhl (2012). https://doi.org/10.4230/LIPIcs.RTA.2012.6
Accattoli, B., Faggian, C., Guerrieri, G.: Factorization and normalization, essentially. In: Programming Languages and Systems - 17th Asian Symposium, APLAS 2019. Lecture Notes in Computer Science, vol. 11893, pp. 159–180. Springer (2019). https://doi.org/10.1007/978-3-030-34175-6_9
Accattoli, B., Faggian, C., Guerrieri, G.: Factorize factorization. In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021. LIPIcs, vol. 183, pp. 6:1–6:25. Schloss-Dagstuhl (2021). https://doi.org/10.4230/LIPIcs.CSL.2021.6
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103. North Holland (1984)
Benton, P.N., Bierman, G.M., de Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: International Conference on Typed Lambda Calculi and Applications, TLCA ’93. Lecture Notes in Computer Science, vol. 664, pp. 75–90. Springer (1993). https://doi.org/10.1007/BFb0037099
Benton, P.N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, LICS 1996. pp. 420–431. IEEE Computer Society (1996). https://doi.org/10.1109/LICS.1996.561458
Bucciarelli, A., Kesner, D., Ríos, A., Viso, A.: The bang calculus revisited. In: Functional and Logic Programming - 15th International Symposium, FLOPS 2020. Lecture Notes in Computer Science, vol. 12073, pp. 13–32. Springer (2020). https://doi.org/10.1007/978-3-030-59025-3_2
de Carvalho, D., Pagani, M., Tortora de Falco, L.: A semantic measure of the execution time in linear logic. Theor. Comput. Sci. 412(20), 1884–1902 (2011). https://doi.org/10.1016/j.tcs.2010.12.017
Chouquet, J., Tasson, C.: Taylor expansion for Call-By-Push-Value. In: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 152, pp. 16:1–16:16. Schloss Dagstuhl (2020). https://doi.org/10.4230/LIPIcs.CSL.2020.16
Ehrhard, T.: Call-by-push-value from a linear logic point of view. In: Programming Languages and Systems - 25th European Symposium on Programming (ESOP 2016). Lecture Notes in Computer Science, vol. 9632, pp. 202–228 (2016). https://doi.org/10.1007/978-3-662-49498-1_9
Ehrhard, T., Guerrieri, G.: 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 (PPDP 2016). pp. 174–187. ACM (2016). https://doi.org/10.1145/2967973.2968608
Faggian, C., Guerrieri, G.: Factorization in call-by-name and call-by-value calculi via linear logic (long version). CoRR abs/2101.08364 (2021), https://arxiv.org/abs/2101.08364
Faggian, C., Ronchi Della Rocca, S.: Lambda calculus and probabilistic computation. In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. pp. 1–13. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785699
Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987). https://doi.org/10.1016/0304-3975(87)90045-4
Guerrieri, G., Manzonetto, G.: The bang calculus and the two Girard’s translations. In: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018). EPTCS, vol. 292, pp. 15–30 (2019). https://doi.org/10.4204/EPTCS.292.2
Guerrieri, G., Olimpieri, F.: Categorifying non-idempotent intersection types. In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021. LIPIcs, vol. 183, pp. 25:1–25:24. Schloss Dagstuhl (2021). https://doi.org/10.4230/LIPIcs.CSL.2021.25
Hindley, J.R.: The Church-Rosser Property and a Result in Combinatory Logic. Ph.D. thesis, University of Newcastle-upon-Tyne (1964)
Hindley, J.R., Seldin, J.P.: Introduction to Combinators and Lambda-Calculus. Cambridge University Press (1986)
Hirokawa, N., Middeldorp, A., Moser, G.: Leftmost Outermost Revisited. In: 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 36, pp. 209–222. Schloss Dagstuhl (2015). https://doi.org/10.4230/LIPIcs.RTA.2015.209
Levy, P.B.: Call-by-push-value: A subsuming paradigm. In: Typed Lambda Calculi and Applications, 4th International Conference (TLCA’99). Lecture Notes in Computer Science, vol. 1581, pp. 228–242 (1999). https://doi.org/10.1007/3-540-48959-2_17
Levy, P.B.: Call-by-push-value: Decomposing call-by-value and call-by-name. High. Order Symb. Comput. 19(4), 377–414 (2006). https://doi.org/10.1007/s10990-006-0480-6
de’ Liguoro, U.: Non-deterministic untyped \(\lambda \)-calculus. A study about explicit non determinism in higher-order functional calculi. Ph.D. thesis, Università di Roma La Sapienza (1991), http://www.di.unito.it/~deligu/papers/UdLTesi.pdf
de’ Liguoro, U., Piperno, A.: Non deterministic extensions of untyped lambda-calculus. Inf. Comput. 122(2), 149–177 (1995). https://doi.org/10.1006/inco.1995.1145
Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theor. Comput. Sci. 228(1-2), 175–210 (1999). https://doi.org/10.1016/S0304-3975(98)00358-2
Newman, M.: On theories with a combinatorial definition of equivalence. Annals of Mathematics 43(2) (1942)
Pagani, M., Tranquilli, P.: The conservation theorem for differential nets. Math. Struct. Comput. Sci. 27(6), 939–992 (2017). https://doi.org/10.1017/S0960129515000456
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975). https://doi.org/10.1016/0304-3975(75)90017-1
Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004)
Ronchi Della Rocca, S., Roversi, L.: Lambda calculus and intuitionistic linear logic. Stud Logica 59(3), 417–448 (1997). https://doi.org/10.1023/A:1005092630115
Santo, J.E., Pinto, L., Uustalu, T.: Modal embeddings and calling paradigms. In: 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019. LIPIcs, vol. 131, pp. 18:1–18:20. Schloss Dagstuhl (2019). https://doi.org/10.4230/LIPIcs.FSCD.2019.18
Simpson, A.K.: Reduction in a linear lambda-calculus with applications to operational semantics. In: Term Rewriting and Applications, 16th International Conference (RTA 2005). Lecture Notes in Computer Science, vol. 3467, pp. 219–234 (2005). https://doi.org/10.1007/978-3-540-32033-3_17
Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995). https://doi.org/10.1006/inco.1995.1057
Terese: Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)
Terui, K.: Light affine lambda calculus and polynomial time strong normalization. Archive for Mathematical Logic 46(3-4), 253–280 (2007). https://doi.org/10.1007/s00153-007-0042-6
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
© 2021 The Author(s)
About this paper
Cite this paper
Faggian, C., Guerrieri, G. (2021). Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)