In the system \lambda^ of intersection types, without \omega, the
problem as to whether an arbitrary type has an inhabitant,
has been shown to be undecidable by Urzyczyn. For one subsystem of \lambda^, that lacks the ^-
introduction rule, the inhabitation problem has been
shown to be decidable in Kurata and Takahashi.
The natural question that arises is: What other subsystems
of \lambda^, have a decidable inhabitation problem?
Our earlier work, which classifies distinct and
inhabitation-distinct subsystems of \lambda^, leads to the
extension of the undecidability result to \lambda^ without
the (\eta) 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.
Cite as: Bunder, M. (2008). The Inhabitation Problem for Intersection Types. In Proc. Fourteenth Computing: The Australasian Theory Symposium (CATS 2008), Wollongong, NSW, Australia. CRPIT, 77. Harland, J. and Manyem, P., Eds. ACS. 7-14.
(from crpit.com)
(local if available)