Structural decidable extensionsof bounded quantification

Abstract : We show how the subtype relation of the well-known second-order polymorphic system $F_\leq$ with bounded type quantification dupoly Cardelli, Wegner, Bruce, Longo, Curien, Ghelli, proved undecidable Ca Pierce, can be interpreted in a (weak) monadic second-order theory of one (Büchi), two (Rabin), several, or infinitely many successor functions. These \bf (W)SnS-interpretations show that undecidable $F_\leq$ possesses consistent decidable extensions, i.e., $F_\leq$ is not essentially undecidable (Tarski, 1949). We demonstrate an infinite class of ``structurWe dem decidable extensions of $F_\leq$, which combine traddecidable exten inference rules with the above \bf (W)SnS-interpretations. All thesi extensions, which we call systems $F_\leq^SnS$, are still more powerful than $F_\leq$, but less coarse than the direct \bf (W)SnS-interpretations: \[F_\leq\ \subset\ F_\l\[F_\leq\ \subset\ F (W)SnS\mbox-interpretations\] The main distinctive featuresThe main distinctive features of decidability, 2) closure w.r.t. transitivity; 3) structurednedecidabil they never subtype a functional type to a universal one or vice versa, 4) they all contain the powerful rule for subtyping boundedly quantified types: \[\frac\Gamma\ \v\[\frac\Gamma\ \vdash \tau_1\ \leq\ \sigma_ \Gamma\,,\,\alpha\ \leq\ \tau_1\ \vdash\ \sigma_2\ \leq\ \t \Ga
Type de document :
[Research Report] RR-2309, INRIA. 1994
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 15:09:20
Dernière modification le : samedi 17 septembre 2016 - 01:06:54
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:23:15



  • HAL Id : inria-00074364, version 1



Sergeï Vorobyov. Structural decidable extensionsof bounded quantification. [Research Report] RR-2309, INRIA. 1994. 〈inria-00074364〉



Consultations de la notice


Téléchargements de fichiers