Publication Details

This conference paper was originally published as Bunder, MW, The inhabitation problem for intersection types, in Harland, J & Manyem, P (eds), Theory of Computing 2008 - Proceedings of the Fourteenth Computing: The Australasian Theory Symposium (CAT2008) Australian Computer Society, 2008, 7-14.


In the system lambda ^ of intersection types, without w, the problem as to whether an arbitrary type has an inhabitant, has been shown to be undecidable by Urzyczyn in [9]. For one subsystem of lambda ^, that lacks the ^- introduction rule, the inhabitation problem has been shown to be decidable in Kurata and Takahashi [9]. The natural question that arises is: What other subsystems of lambda ^, have a decidable inhabitation problem? The work in [2], which classifies distinct and inhabitation-distinct subsystems of lambda ^, leads to the extension of the undecidability result to lambda ^ without the (n) rule. By new methods, this paper shows, for the remaining six (two of them trivial) distinct subsystems of lambda ^, that inhabitation is decidable. For the latter subsystems inhabitant finding algorithms are provided.