The emptiness problem for intersection types
- 1 September 1999
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 64 (3) , 1195-1215
- https://doi.org/10.2307/2586625
Abstract
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.Keywords
This publication has 14 references indexed in Scilit:
- The undecidability of typability in the Lambda-Pi-calculusPublished by Springer Nature ,2006
- The emptiness problem for intersection typesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The "Relevance" of Intersection and Union TypesNotre Dame Journal of Formal Logic, 1997
- Inhabitation in typed lambda-calculi (a syntactic approach)Published by Springer Nature ,1997
- Type reconstruction in finite rank fragments of the second-order λ-calculusInformation and Computation, 1992
- The completeness of provable realizability.Notre Dame Journal of Formal Logic, 1989
- Functional Characters of Solvable TermsMathematical Logic Quarterly, 1981
- Semantical Investigations in Heyting’s Intuitionistic LogicPublished by Springer Nature ,1981
- Intuitionistic propositional logic is polynomial-space completeTheoretical Computer Science, 1979
- The Principal Type-Scheme of an Object in Combinatory LogicTransactions of the American Mathematical Society, 1969