Document Open Access Logo

Categorifying Non-Idempotent Intersection Types

Authors Giulio Guerrieri , Federico Olimpieri

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2021.25.pdf
  • Filesize: 0.66 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Linear logic
  • Theory of computation → Categorical semantics
Keywords
  • Linear logic
  • bang calculus
  • non-idempotent intersection types
  • distributors
  • relational semantics
  • combinatorial species
  • symmetric sequences
  • bicategory
  • categorification

Metrics

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

Abstract

Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.

Cite As Get BibTex

Giulio Guerrieri and Federico Olimpieri. Categorifying Non-Idempotent Intersection Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.25

Author Details

Giulio Guerrieri
  • University of Bath, Department of Computer Science, Bath, UK
Federico Olimpieri
  • Institut de Mathématiques de Marseille (I2M), Aix-Marseille Université, Marseille, France

Funding

This work is partially supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing.

Acknowledgements

The authors thank Lionel Vaux Auclair for insightful discussions and comments.

References

  1. Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoretical Computer Science, 355(2):108-126, 2006. Logic, Language, Information and Computation. URL: https://doi.org/10.1016/j.tcs.2006.01.004.
  2. 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
  3. Jean Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, pages 1-77, Berlin, Heidelberg, 1967. Springer Berlin Heidelberg. Google Scholar
  4. Alexis Bernadet and Stéphane Jean Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, Volume 9, Issue 4, 2013. URL: https://doi.org/10.2168/LMCS-9(4:3)2013.
  5. Robert Blackwell, Gregory Maxwell Kelly, and John Power. Two-dimensional monad theory. Journal of Pure and Applied Algebra, 59(1):1-41, 1989. URL: https://doi.org/10.1016/0022-4049(89)90160-6.
  6. Francis Borceux. Handbook of Categorical Algebra, volume 1 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994. URL: https://doi.org/10.1017/CBO9780511525858.
  7. Flavien Breuvart and Ugo Dal Lago. On Intersection Types and Probabilistic Lambda Calculi. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pages 8:1-8:13, 2018. URL: https://doi.org/10.1145/3236950.3236968.
  8. 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, volume 12073 of Lecture Notes in Computer Science, pages 13-32. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_2.
  9. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/jigpal/jzx018.
  10. Jean Bénabou. Distributors at work. Lecture notes of a course given at TU Darmstadt, 2000. URL: http://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.
  11. Alberto Carraro and Giulio Guerrieri. A Semantical and Operational Account of Call-by-Value Solvability. In Foundations of Software Science and Computation Structures, FOSSACS 2014, volume 8412 of Lecture Notes in Computer Science, pages 103-118, Berlin, Heidelberg, 2014. Springer. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  12. Gian Luca Cattani and Glynn Winskel. Profunctors, open maps and bisimulation. Mathematical Structures in Computer Science, 15(3):553–614, 2005. URL: https://doi.org/10.1017/S0960129505004718.
  13. Jules Chouquet and Christine Tasson. Taylor expansion for Call-by-Push-Value. In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, volume 152 of LIPIcs, pages 16:1-16:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.16.
  14. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type-assignment for lambda terms. Arch. Math. Log., 19(1):139-156, 1978. URL: https://doi.org/10.1007/BF02011875.
  15. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  16. Daniel de Carvalho. Semantique de la logique lineaire et temps de calcul. PhD thesis, Aix-Marseille Université, 2007. Google Scholar
  17. 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.
  18. Daniel de Carvalho. Taylor expansion in linear logic is invertible. Log. Methods Comput. Sci., 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:21)2018.
  19. Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A semantic measure of the execution time in linear logic. Theoretical Computer Science, 412(20):1884-1902, 2011. URL: https://doi.org/10.1016/j.tcs.2010.12.017.
  20. 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.
  21. Thomas Ehrhard. Collapsing non-idempotent intersection types. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, 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.
  22. Thomas Ehrhard. The Scott model of linear logic is the extensional collapse of its relational model. Theoretical Computer Science, 424:20-45, 2012. URL: https://doi.org/10.1016/j.tcs.2011.11.027.
  23. Thomas Ehrhard. Call-by-push-value from a linear logic point of view. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, volume 9632 of Lecture Notes in Computer Science, pages 202-228. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_9.
  24. Thomas Ehrhard and Giulio Guerrieri. 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, pages 174-187. Association for Computing Machinery, 2016. URL: https://doi.org/10.1145/2967973.2968608.
  25. Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine’s machine and the Taylor expansion of lambda-terms. In Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, volume 3988 of Lecture Notes in Computer Science, pages 186-197. Springer, 2006. URL: https://doi.org/10.1007/11780342_20.
  26. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary λ-terms. Theoretical Computer Science, 403(2-3), 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  27. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. of the London Mathematical Society, 77(1):203-220, 2008. URL: https://doi.org/10.1112/jlms/jdm096.
  28. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, November 2017. URL: https://doi.org/10.1007/s00029-017-0361-3.
  29. Zeinab Galal. A Profunctorial Scott Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.16.
  30. Nicola Gambino and André Joyal. On operads, bimodules and analytic functors. Memoirs of the American Mathematical Society, 249(1184):0–0, September 2017. URL: https://doi.org/10.1090/memo/1184.
  31. Philippa Gardner. Discovering needed reductions using type theory. In Theoretical Aspects of Computer Software, International Conference TACS '94, volume 789 of Lecture Notes in Computer Science, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  32. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  33. Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two Girard’s translations. In Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, volume 292 of EPTCS, pages 15-30, 2018. URL: https://doi.org/10.4204/EPTCS.292.2.
  34. Martin Hyland. Classical lambda calculus in modern dress. Mathematical Structures in Computer Science, 27(5):762-781, 2017. URL: https://doi.org/10.1017/S0960129515000377.
  35. André Joyal. Foncteurs analytiques et espèces de structures. In Combinatoire énumérative, pages 126-159, Berlin, Heidelberg, 1986. Springer Berlin Heidelberg. Google Scholar
  36. Gregory Maxwell Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bulletin of the Australian Mathematical Society, 22(1):1-83, 1980. URL: https://doi.org/10.1017/S0004972700006353.
  37. Jean-Louis Krivine. Lambda-calculus, types and models. In Ellis Horwood series in computers and their applications, 1993. Google Scholar
  38. Ugo Dal Lago and Thomas Leventis. On the Taylor expansion of probabilistic lambda-terms. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 13:1-13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.13.
  39. Paul Blain Levy. Call-by-Push-Value: A Subsuming Paradigm. In Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, volume 1581 of Lecture Notes in Computer Science, page 228–242. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_17.
  40. Fosco Loregian. This is the (co)end, my only (co)friend, 2015. URL: http://arxiv.org/abs/1501.02503.
  41. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. Proc. ACM Program. Lang., 2(POPL):6:1-6:28, 2018. URL: https://doi.org/10.1145/3158094.
  42. Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. SIGPLAN Not., 50(1):3-16, January 2015. URL: https://doi.org/10.1145/2775051.2676970.
  43. Federico Olimpieri. Intersection Type Distributors, 2020. URL: http://arxiv.org/abs/2002.01287.
  44. Federico Olimpieri. Intersection Types and Resource Calculi in the Denotational Semantics of Lambda-Calculus. PhD thesis, Aix-Marseille Université, 2020. Google Scholar
  45. 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.
  46. José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal embeddings and calling paradigms. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, volume 131 of LIPIcs, pages 18:1-18:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.18.
  47. Alex K. Simpson. Reduction in a linear lambda-calculus with applications to operational semantics. In Term Rewriting and Applications, 16th International Conference, RTA 2005, volume 3467 of Lecture Notes in Computer Science, pages 219-234. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-32033-3_17.
  48. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised Species of Rigid Resource Terms. In Proceedings of the 32rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005093.
  49. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Species, profunctors and Taylor expansion weighted by SMCC: A unified framework for modelling nondeterministic, probabilistic and quantum programs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 889-898. IEEE Computer Society, 2018. URL: https://doi.org/10.1145/3209108.3209157.
  50. Pierre Vial. Infinitary intersection types as sequences: A new answer to Klop’s problem. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005103.
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