# Hierarchies of decidable extensions of bounded quantification

Abstract : 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.
Keywords :
Type de document :
Rapport
[Research Report] RR-2354, INRIA. 1994
Domaine :
Liste complète des métadonnées

https://hal.inria.fr/inria-00074323
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 15:03:30
Dernière modification le : samedi 17 septembre 2016 - 01:06:53
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:08:24

### Identifiants

• HAL Id : inria-00074323, version 1

### Citation

Sergei Vorobyov. Hierarchies of decidable extensions of bounded quantification. [Research Report] RR-2354, INRIA. 1994. 〈inria-00074323〉

### Métriques

Consultations de la notice

## 118

Téléchargements de fichiers