Document Open Access Logo

Isomorphism of "Functional" Intersection Types

Authors Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, Maddalena Zacchi

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2013.129.pdf
  • Filesize: 0.63 MB
  • 21 pages

Document Identifiers

Author Details

Mario Coppo
Mariangiola Dezani-Ciancaglini
Ines Margaria
Maddalena Zacchi

Cite AsGet BibTex

Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. Isomorphism of "Functional" Intersection Types. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 129-149, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.TYPES.2013.129

Abstract

Type isomorphism for intersection types is quite odd, since it is not a congruence and it does not extend type equality in the standard interpretation of types. The lack of congruence is due to the proof theoretic nature of the intersection introduction rule, which requires the same term to be the subject of both premises. A partial congruence can be recovered by introducing a suitable notion of type similarity. Type equality in standard models becomes included in type isomorphism whenever atomic types have "functional" interpretations, i.e. they are equivalent to arrow types. This paper characterises type isomorphism for a type system in which the equivalence between atomic types and arrow types is induced by the initial projections of the Scott's model via the correspondence between inverse limit models and filter lambda-models.
Keywords
  • Type Isomorphism
  • Lambda calculus
  • Intersection Types

Metrics

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

References

  1. Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Furio Honsell. Inverse limit models as filter models. In D. Kesner, F. van Raamsdonk, and J. Wells, editors, Higher-Order Rewriting, pages 3-25. RWTH Aachen, 2004. Google Scholar
  2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931-940, 1983. Google Scholar
  3. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in Logic. Cambridge, 2013. Google Scholar
  4. Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231-247, 1992. Google Scholar
  5. Kim Bruce and Giuseppe Longo. Provable isomorphisms and domain equations in models of typed languages. In R. Sedgewick, editor, Symposium on the Theory of Computing, pages 263-272. ACM Press, 1985. Google Scholar
  6. Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium, pages 241-262. North-Holland, 1984. Google Scholar
  7. Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. Towards isomorphism of intersection and union types. In S. Graham-Lengrand and L. Paolini, editors, Intersection Types and Related Systems, volume 121 of EPTCS, pages 58-80, 2013. Google Scholar
  8. Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. Isomorphism of intersection and union types. Mathematical Structures in Computer Science, 2014. To appear. Google Scholar
  9. Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. On isomorphism of "functional" intersection and union types. In J. Rehof, editor, Intersection Types and Related Systems, EPTCS, 2014. To appear. Google Scholar
  10. Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279-301, 1982. Google Scholar
  11. Mariangiola Dezani-Ciancaglini. Characterisation of normal forms possessing an inverse in the λβη-calculus. Theoretical Computer Science, 2(3):323-337, 1976. Google Scholar
  12. Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta. On isomorphisms of intersection types. ACM Transactions on Computational Logic, 11(4):1-22, 2010. Google Scholar
  13. Roberto Di Cosmo. Second order isomorphic types. A proof theoretic study on second order λ-calculus with surjective pairing and terminal object. Information and Computation, 119(2):176-201, 1995. Google Scholar
  14. Roberto Di Cosmo. A short survey of isomorphisms of types. Mathematical Structures in Computer Science, 15:825-838, 2005. Google Scholar
  15. Alejandro Díaz-Caro and Gilles Dowek. Simply typed lambda-calculus modulo type isomorphisms. https://who.rocq.inria.fr/Alejandro.Diaz-Caro/stmti.pdf, 2014.
  16. Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. Operational, Denotational and Logical Descriptions: a Case Study. Fundamenta Informaticae, 16(1):149-169, 1992. Google Scholar
  17. Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. Annals of Pure and Applied Logic, 141(1-2):35-50, 2006. Google Scholar
  18. Maxwell H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43(2):223-243, 1942. Google Scholar
  19. Simona Ronchi Della Rocca. Principal type scheme and unification for intersection type discipline. Theoretical Computer Science, 59(1-2):1-29, 1988. Google Scholar
  20. Richard Routley and Robert K. Meyer. The semantics of entailment III. Journal of Philosophical Logic, 1:192-208, 1972. Google Scholar
  21. Dana Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry, and Logic, number 274 in Lecture Notes in Mathematics, pages 97-136. Springer-Verlag, 1972. Google Scholar
  22. Sergei Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387-1400, 1983. English translation of the original paper in Russian published in Zapiski Nauchnych Seminarov LOMI, v.105, 1981. Google Scholar
  23. Sergei Soloviev. A complete axiom system for isomorphism of types in closed categories. In A. Voronkov, editor, Logic Programming and Automated Reasoning, volume 698 of LNCS, pages 360-371. Springer-Verlag, 1993. 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