[Next]  [Previous]  [Up]  

Problem # 13

Submitted by Mariangiola Dezani-Ciancaglini
Date: 1993–2006
Statement. Inhabitation for intersection type systems
Problem Origin. Different variants of the problem were stated by Henk Barendregt, Mariangiola Dezani-Ciancaglini, Paula Severi, Paweł Urzyczyn, and others.


The inhabitation problem is to determine whether there exists a closed term of a given type. [Urzyczyn, 1999] shows the undecidability of inhabitation for the intersection type system of [Barendregt et al., 1983]. Decidable restrictions are discussed in [Kurata and Takahashi, 1995].

Many different intersection type systems have been introduced, mainly for describing λ  -models: for a list see [Alessi et al., 2006] and the references there. A natural question is decidability of inhabitation for these systems. Using the notation of [Alessi et al., 2006], undecidability of the inhabitation for the system of [Barendregt et al., 1983] implies undecidability of the inhabitation for the systems ℬa  , 𝒞𝒟 𝒱 , ℰ n  . It is easy to show that all types are inhabited in 𝒜 𝒪 and 𝒫a  systems, since all terms inhabit the top type and all closed terms inhabit the bottom type [Honsell and Ronchi Della Rocca, 1992]. A similar argument shows decidability for ℰℋ ℛ system. The question remains open for the systems ℋ ℒ , ℋ ℛ , 𝒮c  , 𝒞𝒟 𝒵 , 𝒟 ℋ ℳ .

A related issue is the inhabitation problem for intersection types of rank at most 3, according to the classification of [Leivant, 1983]. The undecidability proof in [Urzyczyn, 1999] works for rank 4, the problem for rank 2 is decidable, but Exptime-hard [Kuśmierek, 2007].

Yet another open question is the inhabitation problems for systems with recursive intersection types, cf. Problem 11.

Partial solution: The inhabitation problem turned out to be undecidable for types of rank 3 and Expspace-complete for rank 2 [Urzyczyn, 2009].

References for # 13

[Alessi et al., 2006]    Alessi, F., Barbanera, F., and Dezani-Ciancaglini, M. (2006). Intersection types and lambda models. Theoretical Computer Science, 355(2):108–126.

[Barendregt et al., 1983]    Barendregt, H., Coppo, M., and Dezani-Ciancaglini, M. (1983). A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940.

[Honsell and Ronchi Della Rocca, 1992]    Honsell, F. and Ronchi Della Rocca, S. (1992). An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49–75.

[Kurata and Takahashi, 1995]    Kurata, T. and Takahashi, M. (1995). Decidable properties of intersection type systems. In Dezani-Ciancaglini, M. and Plotkin, G., editors, Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 297–311. Springer-Verlag.

[Kuśmierek, 2007]    Kuśmierek, D. (2007). The inhabitation problem for rank two intersection types. In Ronchi Della Rocca, S., editor, Typed Lambda Calculi and Applications, volume 4583 of Lecture Notes in Computer Science, pages 240–254. Springer-Verlag.

[Leivant, 1983]    Leivant, D. (1983). Polymorphic type inference. In Symposium on Principles of Programming Languages, pages 88–98. ACM Press.

[Urzyczyn, 1999]    Urzyczyn, P. (1999). The emptiness problem for intersection types. Journal of Symbolic Logic, 64(3):1195–1215. (Preliminary version in Proc. LICS 94).

[Urzyczyn, 2009]    Urzyczyn, P. (2009). Inhabitation of low-rank intersection types. In Curien, P.-L., editor, Typed Lambda Calculi and Applications, volume 5608 of Lecture Notes in Computer Science, pages 356–370. Springer-Verlag.

[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014