Document Open Access Logo

A Quantitative Version of Simple Types

Authors Daniele Pautasso, Simona Ronchi Della Rocca

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.29.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Author Details

Daniele Pautasso
  • Dipartimento di Informatica, University of Torino, Italy
Simona Ronchi Della Rocca
  • Dipartimento di Informatica, University of Torino, Italy

Acknowledgements

We would like to thank Delia Kesner and Antonio Bucciarelli for many useful discussions about the topic of this paper. We are also grateful to the anonymous referees for their careful reading and suggestions.

Cite AsGet BibTex

Daniele Pautasso and Simona Ronchi Della Rocca. A Quantitative Version of Simple Types. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.29

Abstract

This work introduces a quantitative version of the simple type assignment system, starting from a suitable restriction of non-idempotent intersection types. The resulting system is decidable and has the same typability power as the simple type system; thus, assigning types to terms supplies the very same qualitative information given by simple types, but at the same time can provide some interesting quantitative information. It is well known that typability for simple types is equivalent to unification; we prove a similar result for the newly introduced system. More precisely, we show that typability is equivalent to a unification problem which is a non-trivial extension of the classical one: in addition to unification rules, our typing algorithm makes use of an expansion operation that increases the cardinality of multisets whenever needed.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • λ-calculus
  • intersection types
  • unification

Metrics

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

References

  1. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North-Holland, Amsterdam, 1984. Google Scholar
  2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter model and the completeness of type assignment. J. Symb. Log., 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  3. Choukri-Bey Ben-Yelles. Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, University of Wales Swansea, 1979. Google Scholar
  4. Erika De Benedetti and Simona Ronchi Della Rocca. A type assignment for lambda-calculus complete for fptime and strong normalization. Inf. Comput., 248(195-214):195-214, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.012.
  5. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, CSL 2007, volume 4646, pages 298-312, 2007. Google Scholar
  6. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:7)2018.
  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. Google Scholar
  8. Alonzo Church. A formulation of simple theory of types. J. Symbolic Logic, 5:56-68, 1940. Google Scholar
  9. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Form. Log., 21(4):685-693, 1980. Google Scholar
  10. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Math. Log. Q., 27(2-6):45-58, 1981. Google Scholar
  11. Mario Coppo and Paola Giannini. Principal types and unification for a simple intersection type system. Inf. Comput., 122(1):70-96, 1995. Google Scholar
  12. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251, 2009. Google Scholar
  13. Roger J. Hyndley. Basic Simple Type theory. Hoepli, 1997. Google Scholar
  14. Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In TCS, LNCS, 2014. Google Scholar
  15. Assaf J. Kfoury and Joe B. Wells. Principality and decidable type inference for finite-rank intersection types. In Andrew W. Appel and Alex Aiken, editors, POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999, pages 161-174. ACM, 1999. Google Scholar
  16. Assaf J. Kfoury and Joe B. Wells. Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci., 311(1-3):1-70, 2004. Google Scholar
  17. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Essential and relational models. Mathematical Strucures in Computer Science, 27, 2017. Google Scholar
  18. John A. Robinson. A machine-oriented logic based on the resolution principle. J. Asoc. for Computing Machinery 12 (1965), 12:23-41, 1965. Google Scholar
  19. 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.
  20. Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. Google Scholar
  21. Simona Ronchi Della Rocca and Betti Venneri. Principal type schemes for an extended type theory. Theor. Comput. Sci., 28:151-169, 1984. URL: https://doi.org/10.1016/0304-3975(83)90069-5.
  22. Pawel Urzyczyn. The emptiness problem for intersection types. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994, pages 300-309. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/LICS.1994.316059.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact