The Inhabitation Problem for Intersection Types

Bunder, M.

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)