Document Open Access Logo

Separating Terms by Means of Multi Types, Coinductively

Author Adrienne Lancelot

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.4.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • lambda calculus
  • intersection types
  • program equivalence

Metrics

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

Abstract

Intersection type systems, as adequate models of the λ-calculus, induce an equational theory on terms, that we refer to as type equivalence. We give a new proof technique to coinductively characterize type equivalence. To do so, we explore a simple setting, namely weak head type equivalence, which is the equational theory induced by a weak head non-idempotent intersection type system. 
We prove a folklore result: weak head type equivalence coincides with Sangiorgi’s normal form bisimilarity. What is new in our development is that we only rely on coinductive program equivalences, bypassing the need to introduce term approximants, which were used in previous works characterizing type equivalence.
The crucial part of this characterization is to show that type equivalent terms are normal form bisimilar: we do so by constructing shape typings that can only type terms of a specific normal form structure. Shape typings are a light form of principal types, a technique often used in intersection types to generate from one or few principal typing all possible typings of a term.

Cite As Get BibTex

Adrienne Lancelot. Separating Terms by Means of Multi Types, Coinductively. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.4

Author Details

Adrienne Lancelot
  • Inria & LIX, École Polytechnique, UMR 7161, Palaiseau, France
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France

Acknowledgements

I am grateful to the reviewers for their careful read of the paper and helpful comments and to Beniamino Accattoli for providing me feedback on a first draft.

References

  1. S. Abramsky and C. H. L. Ong. Full Abstraction in the Lazy Lambda Calculus. Information and Computation, 105(2):159-267, 1993. URL: https://doi.org/10.1006/inco.1993.1044.
  2. Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1-7:24, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.7.
  3. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1-94:30, 2018. URL: https://doi.org/10.1145/3236789.
  4. Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In Luís Caires, editor, Programming Languages and Systems, pages 410-439, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-17184-1_15.
  5. Beniamino Accattoli, Adrienne Lancelot, and Claudia Faggian. Normal form bisimulations by value, 2023. URL: https://doi.org/10.48550/arXiv.2303.08161.
  6. Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, and Gabriele Vanoni. Interaction equivalence. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704891.
  7. Victor Arrial, Giulio Guerrieri, and Delia Kesner. An implementation of the quantitative inhabitation for different lambda calculi in a unifying framework, 2023. URL: https://doi.org/10.1145/3554339.
  8. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Quantitative inhabitation for different lambda calculi in a unifying framework. Proc. ACM Program. Lang., 7(POPL):1483-1513, 2023. URL: https://doi.org/10.1145/3571244.
  9. 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
  10. Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.
  11. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Proving soundness of extensional normal-form bisimilarities. Electronic Notes in Theoretical Computer Science, 336:41-56, 2018. The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). URL: https://doi.org/10.1016/j.entcs.2018.03.015.
  12. Viviana Bono and Mariangiola Dezani-Ciancaglini. A tale of intersection types. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 7-20, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394733.
  13. Flavien Breuvart, Giulio Manzonetto, and Domenico Ruoppolo. Relational Graph Models at Work. Logical Methods in Computer Science, Volume 14, Issue 3, July 2018. URL: https://doi.org/10.23638/LMCS-14(3:2)2018.
  14. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, pages 298-312, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-74915-8_24.
  15. 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.
  16. Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia Likavec. Behavioural inverse limit λ-models. Theoretical Computer Science, 316(1):49-74, 2004. Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott. URL: https://doi.org/10.1016/j.tcs.2004.01.023.
  17. 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.
  18. Axel 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.
  19. Søren B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In Stephen D. Brookes, Achim Jung, Michael W. Mislove, and Andre Scedrov, editors, Fifteenth Conference on Mathematical Foundations of Progamming Semantics, MFPS 1999, Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999, volume 20 of Electronic Notes in Theoretical Computer Science, pages 346-374. Elsevier, 1999. URL: https://doi.org/10.1016/S1571-0661(04)80083-5.
  20. Andrew Polonsky and Richard Statman. On sets of terms having a given intersection type. Logical Methods in Computer Science, Volume 18, Issue 3, September 2022. URL: https://doi.org/10.46298/lmcs-18(3:35)2022.
  21. Simona Ronchi Della Rocca. Intersection Types and Denotational Semantics: An Extended Abstract. In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic, editors, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), volume 97 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:7, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2016.2.
  22. Simonetta Ronchi Della Rocca. Characterization theorems for a filter lambda model. Information and Control, 54(3):201-216, 1982. URL: https://doi.org/10.1016/S0019-9958(82)80022-3.
  23. Davide Sangiorgi. The lazy lambda calculus in a concurrency scenario. Information and Computation, 111(1):120-153, 1994. URL: https://doi.org/10.1006/inco.1994.1042.
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