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. |
(from crpit.com)
