The Emptiness Problem for Intersection Types
Urzyczyn, Pawel
J. Symbolic Logic, Tome 64 (1999) no. 1, p. 1195-1215 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of "strong conjunction" of Mints and Lopez-Escobar is also undecidable.
Publié le : 1999-09-14
Classification:  
@article{1183745876,
     author = {Urzyczyn, Pawel},
     title = {The Emptiness Problem for Intersection Types},
     journal = {J. Symbolic Logic},
     volume = {64},
     number = {1},
     year = {1999},
     pages = { 1195-1215},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745876}
}

Urzyczyn, Pawel. The Emptiness Problem for Intersection Types. J. Symbolic Logic, Tome 64 (1999) no. 1, pp.  1195-1215. http://gdmltest.u-ga.fr/item/1183745876/