Document Open Access Logo

Principal Types as Lambda Nets

Authors Pietro Di Gianantonio , Marina Lenisa

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.5.pdf
  • Filesize: 0.83 MB
  • 23 pages

Document Identifiers

Author Details

Pietro Di Gianantonio
  • University of Udine, Italy
Marina Lenisa
  • University of Udine, Italy

Funding

Work supported by the Italian MUR project PRIN 2017FTXR7S "IT-MaTTerS" (Methods and Tools for Trustworthy Smart Systems).

Acknowledgements

We thank Beniamino Accattoli, Paolo Coppola, Furio Honsell, Ivan Scagnetto, and Gabriele Vanoni for helpful discussions on the subject. We are indebted to the anonymous referees for their valuable comments on the present work.

Cite AsGet BibTex

Pietro Di Gianantonio and Marina Lenisa. Principal Types as Lambda Nets. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.5

Abstract

We show that there are connections between principal type schemata, cut-free λ-nets, and normal forms of the λ-calculus, and hence there are correspondences between the normalisation algorithms of the above structures, i.e. unification of principal types, cut-elimination of λ-nets, and normalisation of λ-terms. Once the above correspondences have been established, properties of the typing system, such as typability, subject reduction, and inhabitation, can be derived from properties of λ-nets, and vice-versa. We illustrate the above pattern on a specific type assignment system, we study principal types for this system, and we show that they correspond to λ-nets with a non-standard notion of cut-elimination. Properties of the type system are then derived from results on λ-nets.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Type structures
  • Theory of computation → Linear logic
Keywords
  • Lambda calculus
  • Principal types
  • Linear logic
  • Lambda nets
  • Normalization
  • Cut elimination

Metrics

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

References

  1. Beniamino Accattoli. Proof nets and the linear substitution calculus. In International Colloquium on Theoretical Aspects of Computing, volume 11187 of LNCS, pages 37-61. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02508-3_3.
  2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symb. Log., 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  3. Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. Log. Methods Comput. Sci., 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:3)2013.
  4. Gérard Boudol, Pierre-Louis Curien, and Carolina Lavatelli. A semantics for lambda calculi with resources. Math. Struct. Comput. Sci., 9(4):437-482, 1999. URL: http://journals.cambridge.org/action/displayAbstract?aid=44845.
  5. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:7)2018.
  6. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Strong normalization through intersection types and memory. In M. Benevides and R. Thiemann, editors, Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015), volume 23, pages 75-91. ENTCS, 2016. URL: https://doi.org/10.1016/j.entcs.2016.06.006.
  7. 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.
  8. S. Carlier and J. B. Wells. Type inference with expansion variables and intersection types in system E and an exact correspondence with beta-reduction. In Eugenio Moggi and David Scott Warren, editors, Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 24-26 August 2004, Verona, Italy, pages 132-143. ACM, 2004. URL: https://doi.org/10.1145/1013963.1013980.
  9. S. Carlier and J. B. Wells. Expansion: the crucial mechanism for type inference with intersection types: A survey and explanation. Electron. Notes Theor. Comput. Sci., 136:173-202, 2005. URL: https://doi.org/10.1016/j.entcs.2005.03.026.
  10. S. Carlier and J. B. Wells. The algebra of expansion. Fundam. Informaticae, 121(1-4):43-82, 2012. URL: https://doi.org/10.3233/FI-2012-771.
  11. Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. The involutions-as-principal types/application-as-unification analogy. In G. Barthe, G. Sutcliffe, and M. Veanes, editors, LPAR-22, volume 57 of EPiC Series in Computing, pages 254-270. EasyChair, 2018. URL: https://doi.org/10.29007/ntwg.
  12. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal type schemes and λ-calculus semantics. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 536-560. Academic Press, 1980. Google Scholar
  13. Daniel de Carvalho. Semantiques de la logique lineaire et temps de calcul. PhD thesis, Université Aix-Marseille II, 2007. URL: https://theses.fr/2007AIX22066.
  14. P. Di Gianantonio. A typing and normalisation algorithm for lambda terms, 2019. URL: https://users.dimi.uniud.it/~pietro.digianantonio/papers/code/principalTAS.hs.
  15. Stephen Dolan and Alan Mycroft. Polymorphism, subtyping, and type inference in mlsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pages 60-72. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009882.
  16. E. Duquesne and J. Van De Wiele. A new intrinsic characterization of the principal type schemes. Research Report RR-2416, INRIA, 1995. Projet PARA. URL: https://hal.inria.fr/inria-00074259.
  17. Thomas Ehrhard. A new correctness criterion for MLL proof nets. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603125.
  18. Maribel Fernández and Ian Mackie. A calculus for interaction nets. In G. Nadathur, editor, Principles and Practice of Declarative Programming, volume 1702 of LNCS, pages 170-187. Springer, 1999. URL: https://doi.org/10.1007/10704567_10.
  19. Stefano Guerrini. Correctness of multiplicative proof nets is linear. In Fourteenth Annual IEEE Symposium on Logic in Computer Science, pages 454-463. IEEE Computer Science Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782640.
  20. Stefano Guerrini. Proof nets and the lambda-calculus. In Thomes Ehrhard, editor, Linear Logic in Computer Science, pages 316-65. Cambridge University Press, 2004. URL: https://doi.org/10.1017/CBO9780511550850.
  21. A.J. Kfoury and J.B. Wells. Principality and type inference for intersection types using expansion variables. Theoretical Computer Science, 311(1):1-70, 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.032.
  22. D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44:51-68, 1986. Google Scholar
  23. Peter Møller Neergaard and Harry G. Mairson. Types, potency, and idempotency: Why nonlinearity and amnesia make a type system work. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP ’04, pages 138-149. ACM, 2004. URL: https://doi.org/10.1145/1016850.1016871.
  24. 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.
  25. Laurent Régnier. Lambda-Calcul et Rèseaux. PhD thesis, Université Paris VII, 1992. URL: https://theses.fr/1992PA077165.
  26. Emilie Sayag and Michel Mauny. Characterization of the principal type of normal forms in an intersection type system. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, pages 335-346, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-62034-6_61.
  27. Pawel Urzyczyn. The emptiness problem for intersection types. In Proceedings IEEE Symposium on Logic in Computer Science, pages 300-309, 1994. URL: https://doi.org/10.1109/LICS.1994.316059.
  28. J. B. Wells. The essence of principal typings. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming, ICALP ’02, pages 913-925. Springer-Verlag, 2002. URL: https://doi.org/10.1007/3-540-45465-9_78.
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