Abstract

The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ 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 ( $\wedge$ I). The aim of this paper is to classify intersection type systems lacking some of ( $\wedge$ I), ( $\wedge$ 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