Document Open Access Logo

Pregrammars and Intersection Types

Author Sabine Broda

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.14.pdf
  • Filesize: 0.58 MB
  • 22 pages

Document Identifiers

Author Details

Sabine Broda
  • CMUP, Departamento de Ciência de Computadores, Faculdade de Ciências, University of Porto, Portugal

Funding

The author was partially supported by CMUP, which is financed by national funds through FCT – Fundação para a Ciência e a Tecnologia, I.P., under the project with reference UIDB/00144/2020.

Cite AsGet BibTex

Sabine Broda. Pregrammars and Intersection Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.14

Abstract

A representation of intersection types in terms of pregrammars is presented. Pregrammar based rewriting relations, corresponding respectively to type checking and inhabitation are defined and the latter is used to implement a Wajsberg/Ben-Yelles style alternating semi-decision algorithm for inhabitation. The usefulness of the framework is illustrated by revisiting and partially extending standard inhabitation related results for intersection types, as well as establishing new ones. It is shown how the notion of bounded multiset dimension emerges naturally and the relation between the two settings is clarified. A meaningful rank independent superset of the set of rank 2 types is identified for which EXPSPACE-completeness for inhabitation as well as for counting is proved. Finally, a standard result on negatively non-duplicated simple types is extended to intersection types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic
  • Theory of computation → Lambda calculus
Keywords
  • Intersection Types
  • Pregrammars
  • Inhabitation

Metrics

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

References

  1. S. Alves and S. Broda. Inhabitation machines: determinism and principality. In Ninth Workshop on Non-Classical Models of Automata and Applications, NCMA 2017, pages 57-70, 2017. Google Scholar
  2. S. Alves and S. Broda. A unifying framework for type inhabitation. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), 2018. Google Scholar
  3. Sandra Alves and Sabine Broda. Pre-grammars and inhabitation for a subset of rank 2 intersection types. Electr. Notes Theor. Comput. Sci., 344:25-45, 2019. Google Scholar
  4. T. Aoto. Uniqueness of normal proofs in implicational intuitionistic logic. Journal of Logic, Language and Information, 8(2):217-242, 1999. Google Scholar
  5. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. Google Scholar
  6. Ch. Ben-Yelles. Type Assignment in the Lambda-Calculus: Syntax and Semantics. PhD thesis, University College of Swansea, September 1979. Google Scholar
  7. P. Bourreau and S. Salvati. A datalog recognizer for almost affine -cfgs. In MOL, pages 21-38, 2011. Google Scholar
  8. Sabine Broda and Luís Damas. Counting a type’s principal inhabitants. In Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, pages 69-82, 1999. Google Scholar
  9. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. Logical Methods in Computer Science, 14(3), 2018. Google Scholar
  10. 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. Google Scholar
  11. Martin W. Bunder. The inhabitation problem for intersection types. In Theory of Computing 2008. Proc. Fourteenth Computing: The Australasian Theory Symposium (CATS 2008), Wollongong, NSW, Australia, January 22-25, 2008. Proceedings, pages 7-14, 2008. Google Scholar
  12. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for λ-terms. Arch. Math. Log., 19(1):139-156, 1978. Google Scholar
  13. 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. Google Scholar
  14. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Math. Log. Q., 27(2-6):45-58, 1981. Google Scholar
  15. Boris Düdder, Moritz Martens, and Jakob Rehof. Staged composition synthesis. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, pages 67-86, 2014. Google Scholar
  16. Andrej Dudenhefner and Jakob Rehof. Intersection type calculi of bounded dimension. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 653-665, 2017. Google Scholar
  17. Andrej Dudenhefner and Jakob Rehof. Typability in bounded dimension. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. Google Scholar
  18. Andrej Dudenhefner and Jakob Rehof. Principality and approximation under dimensional bound. PACMPL, 3(POPL):8:1-8:29, 2019. Google Scholar
  19. Joshua Dunfield. Elaborating intersection and union types. J. Funct. Program., 24(2-3):133-165, 2014. Google Scholar
  20. Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pages 250-266, 2003. Google Scholar
  21. Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. Example-directed synthesis: a type-theoretic interpretation. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 802-815, 2016. Google Scholar
  22. Timothy S. Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, pages 268-277, 1991. Google Scholar
  23. J.R. Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997. Google Scholar
  24. S. Hirokawa. Infiniteness of proof (α) is polynomial-space complete. Theoretical Computer Science, 206(1-2):331-339, 1998. Google Scholar
  25. Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood series in computers and their applications. Masson, 1993. Google Scholar
  26. Toshihiko Kurata and Masako Takahashi. Decidable properties of intersection type systems. In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings, pages 297-311, 1995. Google Scholar
  27. D. Kusmierek. The inhabitation problem for rank two intersection types. In Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, pages 240-254, 2007. Google Scholar
  28. D. Leivant. Polymorphic type inference. In Proceedings of Principles of Programming Languages (POPL'83), pages 88-98, New York, NY, USA, 1983. ACM Press. Google Scholar
  29. Ralph Loader. The undecidability of lambda-definability. Google Scholar
  30. Christian Mossin. Exact flow analysis. Mathematical Structures in Computer Science, 13(1):125-156, 2003. Google Scholar
  31. Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. J. Funct. Program., 11(3):263-317, 2001. Google Scholar
  32. G. Plotkin. Lambda definability and logical relations, Technical Report Memorandum SAI-RM-4, School of Artificial Intelligence, University of Edingburgh, (1973). Google Scholar
  33. G. Pottinger. A type assignment for the strongly normalizable lambda-terms. In J. Hindley and J. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 561-577. Academic Press, 1980. Google Scholar
  34. Steven J. Ramsay. Exact intersection type abstractions for safety checking of recursion schemes. In Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014, pages 175-186, 2014. Google Scholar
  35. Jakob Rehof and Pawel Urzyczyn. The complexity of inhabitation with explicit intersection. In Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, pages 256-270, 2012. Google Scholar
  36. John C. Reynolds. Design of the Programming Language FORSYTHE, page 173–233. Birkhauser Boston Inc., USA, 1997. Google Scholar
  37. Sylvain Salvati. Recognizability in the simply typed lambda-calculus. In Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings, pages 48-60, 2009. Google Scholar
  38. Sylvain Salvati, Giulio Manzonetto, Mai Gehrke, and Henk Barendregt. Loader and urzyczyn are logically related. In Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II, pages 364-376, 2012. Google Scholar
  39. R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67-72, 1979. Google Scholar
  40. M. Takahashi, Y. Akama, and S. Hirokawa. Normal proofs and their grammar. Information and Computation, 125(2):144-153, 1996. Google Scholar
  41. P. Urzyczyn. Inhabitation in typed lambda-calculi (a syntactic approach). In TLCA'97, volume 1210 of LNCS, pages 373-389. Springer, 1997. Google Scholar
  42. P. Urzyczyn. The emptiness problem for intersection types. Journal of Symbolic Logic, 64(3):1195-1215, 1999. Google Scholar
  43. P. Urzyczyn. Inhabitation of low-rank intersection types. In TLCA'09, volume 5608 of LNCS, pages 356-370. Springer, 2009. Google Scholar
  44. Steffen van Bakel. Strict intersection types for the lambda calculus. ACM Comput. Surv., 43(3):20:1-20:49, 2011. Google Scholar
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