The emptiness problem for intersection types

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...

Full description

Saved in:
Bibliographic Details
Published in:The Journal of symbolic logic 1999-09, Vol.64 (3), p.1195-1215
Main Author: Urzyczyn, Paweł
Format: Article
Language:English
Subjects:
Alphabets
Automata
Fathers
Lambda calculus
Logical proofs
Rooting depth
Sons
Symbols
Trees
Undecidability
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0022-4812
1943-5886
DOI:10.2307/2586625