Hierarchies of decidable extensions of bounded quantification

Overview & Synopsis

The system $F_\leq$, the well-known second-order polymorphic typed $\lambda$-calculus with subtyping and bounded universal type quantification [Cardelli-Wegner 85], [Bruce-Longo 90], [Curien-Ghelli 92], [Pierce 92], [Cardelli-Martini-Mitchell-Scedrov 94], appears to be undecidable [Pierce 92] because of undecidability of its subtyping component. Attempts were made to obtain decidable type systems with subtyping by weakening $F_\leq$ [Castagna-Pierce 94], [Katiyar-Sankar 92], and also by reinforcing or \em extending\/ it [Vorobyov 94]. However, for the moment, these extensions lack the important proof-theoretic minimum type property, which holds for $F_\leq$ and guarantees that each typable term has the minimum type, being a subtype of any other type of the term [Curien-Ghelli 92], [Vorobyov 94]. As a preparation step to introducing the extensions of $F_\leq$ with the minimum type property and the decidable term typing relation, we define and study here the hierarchies of decidable extensions of the$F_\leq$ subtyping relation. We demonstrate conditions providing that each theory in a hierarchy: \beginenumerate \item extends $F_\leq$, proving everything that is $F_\leq$-provable \item satisfies the substitution property for boundedly quantified universal types \item is transitive (transitivity and substitutivity are indispensable for the minimum type property and typing proof normalization). We give conditions guaranteeing that a hierarchy condenses and converges to $F_\leq$, and study cases when a hierarchy collapses.