Document Open Access Logo

Semantic Bounds and Multi Types, Revisited

Author Beniamino Accattoli

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.7.pdf
  • Filesize: 0.97 MB
  • 24 pages

Document Identifiers

Author Details

Beniamino Accattoli
  • Inria & LIX, École Poytechnique, Palaiseau, France

Cite AsGet BibTex

Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.7

Abstract

Intersection types are a standard tool in operational and semantical studies of the λ-calculus. De Carvalho showed how multi types, a quantitative variant of intersection types providing a handy presentation of the relational denotational model, allows one to extract precise bounds on the number of β-steps and the size of normal forms. In the last few years, de Carvalho’s work has been extended and adapted to a number of λ-calculi, evaluation strategies, and abstract machines. These works, however, only adapt the first part of his work, that extracts bounds from multi type derivations, while never consider the second part, which deals with extracting bounds from the multi types themselves. The reason is that this second part is more technical, and requires to reason up to type substitutions. It is however also the most interesting, because it shows that the bounding power is inherent to the relational model (which is induced by the types, without the derivations), independently of its presentation as a type system. Here we dissect and clarify the second part of de Carvalho’s work, establishing a link with principal multi types, and isolating a key property independent of type substitutions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Denotational semantics
  • Theory of computation → Operational semantics
Keywords
  • Lambda calculus
  • intersection types
  • denotational semantics
  • linear logic

Metrics

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

Related Versions

References

  1. Beniamino Accattoli. Semantic bound and multi types, revisited, 2023. URL: https://arxiv.org/abs/2311.18233.
  2. Beniamino Accattoli and Ugo Dal Lago. (Leftmost-outermost) Beta reduction is invariant, indeed. Logical Methods in Computer Science, 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  3. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The (in)efficiency of interaction. Proc. ACM Program. Lang., 5(POPL):1-33, 2021. URL: https://doi.org/10.1145/3434332.
  4. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The space of interaction. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470726.
  5. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. Multi types and reasonable space. Proc. ACM Program. Lang., 6(ICFP):799-825, 2022. URL: https://doi.org/10.1145/3547650.
  6. Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorization and normalization, essentially. In Anthony Widjaja Lin, editor, Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of Lecture Notes in Computer Science, pages 159-180. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_9.
  7. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds, fully developed. J. Funct. Program., 30:e14, 2020. URL: https://doi.org/10.1017/S095679682000012X.
  8. 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, 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.
  9. Beniamino Accattoli and Giulio Guerrieri. The theory of call-by-value solvability. Proc. ACM Program. Lang., 6(ICFP):855-885, 2022. URL: https://doi.org/10.1145/3547652.
  10. 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, volume 11423 of Lecture Notes in Computer Science, pages 410-439. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_15.
  11. Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Semantic bounds and strong call-by-value normalization. CoRR, abs/2104.13979, 2021. URL: https://arxiv.org/abs/2104.13979.
  12. Sandra Alves, Delia Kesner, and Miguel Ramos. Quantitative global memory. In Helle Hvid Hansen, Andre Scedrov, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 29th International Workshop, WoLLIC 2023, Halifax, NS, Canada, July 11-14, 2023, Proceedings, volume 13923 of Lecture Notes in Computer Science, pages 53-68. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-39784-4_4.
  13. Sandra Alves, Delia Kesner, and Daniel Ventura. A quantitative understanding of pattern matching. In 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway, volume 175 of LIPIcs, pages 3:1-3:36. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.3.
  14. Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:3)2013.
  15. 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.
  16. Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full abstraction for resource calculus with tests. In Marc Bezem, editor, Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, volume 12 of LIPIcs, pages 97-111. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.CSL.2011.97.
  17. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Logic, 109(3):205-241, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00056-7.
  18. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. A relational model of a parallel and non-deterministic lambda-calculus. In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings, volume 5407 of Lecture Notes in Computer Science, pages 107-121. Springer, 2009. URL: https://doi.org/10.1007/978-3-540-92687-0_8.
  19. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. In Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings, pages 13-32. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_2.
  20. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/JIGPAL/JZX018.
  21. Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. Exponentials with infinite multiplicities. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 170-184. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_16.
  22. 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.
  23. Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. Intersection types and (positive) almost-sure termination. Proc. ACM Program. Lang., 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434313.
  24. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Inf. Comput., 209(6):966-991, 2011. URL: https://doi.org/10.1016/j.ic.2011.02.001.
  25. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. Thèse de doctorat, Université Aix-Marseille II, 2007. Google Scholar
  26. Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 41:1-41:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.41.
  27. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Str. in Comput. Sci., 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  28. 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: https://doi.org/10.1016/j.tcs.2010.12.017.
  29. Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. Inf. Comput., 248:104-129, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.010.
  30. Thomas Ehrhard. Hypercoherences: A strongly stable model of linear logic. Math. Struct. Comput. Sci., 3(4):365-385, 1993. URL: https://doi.org/10.1017/S0960129500000281.
  31. Thomas Ehrhard. Finiteness spaces. Math. Struct. Comput. Sci., 15(4):615-646, 2005. URL: https://doi.org/10.1017/S0960129504004645.
  32. Thomas Ehrhard. 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, 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.
  33. Thomas Ehrhard. The scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci., 424:20-45, 2012. URL: https://doi.org/10.1016/j.tcs.2011.11.027.
  34. Thomas Ehrhard. Non-idempotent intersection types in logical form. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 198-216. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_11.
  35. José Espírito Santo, Delia Kesner, and Loïc Peyrot. A faithful and quantitative notion of distant reduction for generalized applications. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 285-304. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_15.
  36. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  37. Jean-Yves Girard. Normal functors, power series and the λ-calculus. Annals of Pure and Applied Logic, 37:129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  38. Martin Hyland, Misao Nagayama, John Power, and Giuseppe Rosolini. A category theoretic formulation for engeler-style models of the untyped λ-calculus. Electronic Notes in Theoretical Computer Science, 161:43-57, 2006. Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2004). URL: https://doi.org/10.1016/j.entcs.2006.04.024.
  39. Delia Kesner, Loïc Peyrot, and Daniel Ventura. The spirit of node replication. In Stefan Kiefer and Christine Tasson, editors, 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, volume 12650 of Lecture Notes in Computer Science, pages 344-364. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_18.
  40. Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 296-310. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44602-7_23.
  41. Delia Kesner and Pierre Vial. Consuming and persistent types for classical logic. In LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 619-632, 2020. URL: https://doi.org/10.1145/3373718.3394774.
  42. Delia Kesner and Andrés Viso. Encoding tight typing in a unified framework. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 27:1-27:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.27.
  43. A. J. Kfoury and J. B. Wells. Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci., 311(1-3):1-70, 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.032.
  44. Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood series. Masson, 1993. Google Scholar
  45. 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. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.36.
  46. Giulio Manzonetto. A general class of models of H^*. In Rastislav Královic and Damian Niwinski, editors, Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings, volume 5734 of Lecture Notes in Computer Science, pages 574-586. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03816-7_49.
  47. Giulio Manzonetto and Domenico Ruoppolo. Relational graph models, taylor expansion and extensionality. In Bart Jacobs, Alexandra Silva, and Sam Staton, editors, Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2014, Ithaca, NY, USA, June 12-15, 2014, volume 308 of Electronic Notes in Theoretical Computer Science, pages 245-272. Elsevier, 2014. URL: https://doi.org/10.1016/j.entcs.2014.10.014.
  48. C.-H. Luke Ong. Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005064.
  49. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Essential and relational models. Math. Struct. Comput. Sci., 27(5):626-650, 2017. URL: https://doi.org/10.1017/S0960129515000316.
  50. Simona Ronchi Della Rocca. Principal type scheme and unification for intersection type discipline. Theor. Comput. Sci., 59:181-209, 1988. URL: https://doi.org/10.1016/0304-3975(88)90101-6.
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