Hostname: page-component-8448b6f56d-qsmjn Total loading time: 0 Render date: 2024-04-16T20:49:06.569Z Has data issue: false hasContentIssue false
  • English
  • Français

A classification of intersection type systems

Published online by Cambridge University Press:  12 March 2014

M. W. Bunder
M. W. Bunder*
Affiliation:
School of Mathematics and Applied Statistics, University of Wollongong, Wollongong NSW 2522, Australia, E-mail: martin.bunder@uow.edu.au
Get access Rights & Permissions [Opens in a new window]

Abstract

The first system of intersection types. Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules ((ΛI ) and (ΛE) ) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction.

Urzyczyn proved in [6] that for both these systems it is undecidable whether a given intersection type is empty. Kurata and Takahashi however have shown in [5] that this emptiness problem is decidable for the sytem including (η). but without (ΛI).

The aim of this paper is to classify intersection type systems lacking some of (ΛI), (ΛE) and (η), into equivalence classes according to their strength in typing λ-terms and also according to their strength in possessing inhabitants.

This classification is used in a later paper to extend the above (un)decidability results to two of the five inhabitation-equivalence classes. This later paper also shows that the systems in two more of these classes have decidable inhabitation problems and develops algorithms to find such inhabitants.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 67 , Issue 1 , March 2002 , pp. 353 - 368
Copyright
Copyright © Association for Symbolic Logic 2002

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Barendregt, H. P., Coppo, M., and Dezani, M., A filter lambda model and the completeness of type assignment, this Journal, vol. 48 (1983), pp. 931–940.Google Scholar
[2]Bunder, M. W., Intersection types for lambda-terms and combinators and their logics, University of Wollongong, School of Mathematics and Applied Statistics, Preprint Series 11/99.CrossRefGoogle Scholar
[3]Coppo, M. and Dezani, M., A new type-assignment for lambda terms, Archive for Mathematical Logic, vol. 19 (1978), pp. 139–156.CrossRefGoogle Scholar
[4]Hindley, J. R., Types with intersection, an introduction, Formal Aspects of Computing, vol. 4 (1992), pp. 470–486.CrossRefGoogle Scholar
[5]Kurata, T. and Takahashi, M., Decidable properties of intersection type systems, TLCA '95 (Dezani, M. and Plotkin, G., editors), Lecture Notes in Computer Science, vol. 902, 1995, pp. 297–311.Google Scholar
[6]Urzyczyn, P., The emptiness problem for intersection types, Proceedings of logic in computer science, IEEE, 1994, and this Journal, vol. 64 (1999), pp. 1195–1215.Google Scholar
[7]van Bakel, S., Complete restrictions of intersection type discipline, Theoretical Computer Science, vol. 102 (1992), pp. 135–163.CrossRefGoogle Scholar
[8]Venneri, B., Intersection types as logicalformulae, Journal of Logic and Computation, vol. 4 (1994), pp. 109–124.CrossRefGoogle Scholar