The inhabitation problem for intersection types
Martin W. Bunder · Research Online (University of Wollongong) · 2008
In the system λ ∧ of intersection types, without ω, the problem as to whether an arbitrary type has an inhabitant, has been shown to be undecidable by Urzyczyn in [10]. For one subsystem of λ∧, 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 λ∧, have a decidable inhabitation problem? The work in [2], which classifies distinct and inhabitation-distinct subsystems of λ∧, leads to the extension of the undecidability result to λ ∧ without the (η) rule. By new methods, this paper shows, for the remaining six (two of them trivial) distinct subsystems of λ∧, that inhabitation is decidable. For the latter subsystems inhabitant finding algorithms are provided.