RIS ID
21880
Abstract
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.
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.