Document Open Access Logo

Call-By-Value, Again!

Authors Axel Kerinec, Giulio Manzonetto, Simona Ronchi Della Rocca

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.7.pdf
  • Filesize: 0.75 MB
  • 18 pages

Document Identifiers

Author Details

Axel Kerinec
  • Laboratoire LIPN, CNRS UMR 7030, Université Sorbonne Paris-Nord, France
Giulio Manzonetto
  • Laboratoire LIPN, CNRS UMR 7030, Université Sorbonne Paris-Nord, France
Simona Ronchi Della Rocca
  • Computer Science Department, University of Torino, Italy

Funding

  • Manzonetto, Giulio: This work is partly supported by ANR Project ANR-19-CE48-0014.

Acknowledgements

We would like to thank Giulio Guerrieri for interesting discussions, as well as the anonymous reviewers for helpful suggestions.

Cite AsGet BibTex

Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-By-Value, Again!. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.7

Abstract

The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Linear logic
Keywords
  • λ-calculus
  • call-by-value
  • intersection types
  • solvability
  • inhabitation

Metrics

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

References

  1. Samson Abramsky. Domain theory in logical form. Ann. Pure Appl. Log., 51(1-2):1-77, 1991. URL: https://doi.org/10.1016/0168-0072(91)90065-T.
  2. Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 206-226, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_12.
  3. Beniamino Accattoli and Giulio Guerrieri. Types of fireballs. In Sukyoung Ryu, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 45-66. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02768-1_3.
  4. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. URL: http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types.
  5. Henk P. Barendregt. The lambda-calculus, its syntax and semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1984. Google Scholar
  6. O. Bastonero, Alberto Pravato, and Simona Ronchi Della Rocca. Structures for lazy semantics. In David Gries and Willem P. de Roever, editors, Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET '98) 8-12 June 1998, Shelter Island, New York, USA, volume 125 of IFIP Conference Proceedings, pages 30-48. Chapman & Hall, 1998. Google Scholar
  7. Flavien Breuvart, Giulio Manzonetto, and Domenico Ruoppolo. Relational graph models at work. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:2)2018.
  8. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Solvability = typability + inhabitation. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7141.
  9. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:7)2018.
  10. Albero Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, 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, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  11. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Math. Log. Q., 27(2-6):45-58, 1981. URL: https://doi.org/10.1002/malq.19810270205.
  12. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  13. Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. Fundam. Informaticae, 16(1):149-169, 1992. Google Scholar
  14. Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 259-273. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.259.
  15. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Log., 37(2):129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  16. Giulio Guerrieri. Personal communication, 2017. Google Scholar
  17. Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization and conservativity of a refined call-by-value lambda-calculus. Log. Methods Comput. Sci., 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:29)2017.
  18. Furio Honsell and Marina Lenisa. Some results on the full abstraction problem for restricted lambda calculi. In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 84-104. Springer, 1993. URL: https://doi.org/10.1007/3-540-57182-5_6.
  19. Emma Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting call-by-value Böhm trees in light of their Taylor expansion. Log. Methods Comput. Sci., 16(3), 2020. URL: https://lmcs.episciences.org/6638.
  20. Giulio Manzonetto, Michele Pagani, and Simona Ronchi Della Rocca. New semantical insights into call-by-value λ-calculus. Fundam. Informaticae, 170(1-3):241-265, 2019. URL: https://doi.org/10.3233/FI-2019-1862.
  21. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO Theor. Informatics Appl., 33(6):507-534, 1999. URL: https://doi.org/10.1051/ita:1999130.
  22. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  23. Alberto Pravato, Simona Ronchi Della Rocca, and Luca Roversi. The call by value λ-calculus: a semantic investigation. Mathematical Structures in Computer Science, 9(5):617-650, 1999. Google Scholar
  24. Laurent Regnier. Une équivalence sur les lambda-termes. Theor. Comput. Sci., 126(2):281-292, 1994. URL: https://doi.org/10.1016/0304-3975(94)90012-4.
  25. Simona Ronchi Della Rocca. Intersection types and denotational semantics: An extended abstract (invited paper). In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic, editors, 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, volume 97 of LIPIcs, pages 2:1-2:7. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.TYPES.2016.2.
  26. Simona Ronchi Della Rocca and Luca Paolini. The Parametric λ-Calculus: a Metamodel for Computation. EATCS Series. Springer, Berlin, 2004. Google Scholar
  27. Pawel Urzyczyn. The emptiness problem for intersection types. J. Symb. Log., 64(3):1195-1215, 1999. URL: https://doi.org/10.2307/2586625.
  28. Pawel Urzyczyn. Personal communication, 2014. Google Scholar
  29. Steffen van Bakel. Complete restrictions of the intersection type discipline. Theor. Comput. Sci., 102(1):135-163, 1992. URL: https://doi.org/10.1016/0304-3975(92)90297-S.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact