Both subtyping and typing relations in the system F_\leq, the well-known second-order polymorphic typed lambda-calculus with subtyping appeared to be undecidable. We demonstrate an infinite class of extensions of the system F_\leq, where both relations are decidable. Our extensions are based on the converging hierarchies of decidable extensions of the F_\leq-subtyping relation. Every system G from the class satisfies the following properties\, : 1) all subtyping and typing judgments provable in F_\leq are also G-provable ; in particular, every F_\leq-typable term is G-typable, but not conversely : an F_\leq-typable term may have additional types in G, and there exist G-typable terms that are not F_\leq-typable ; 2) the G-canonical types, analogous to the F_\leq-minimum types, are {\em effectively computable} (as opposed to F_\leq) ; there exists a decision procedure, which given a context \Gamma and a term t always terminates yielding the G-canonical type \mu(\Gamma \vdash t) of t in \Gamma whenever it exists, and the result ``undefined'' otherwise\, ; canonical types are used to decide the typing relation : \Gamma \vdash t : \tau iff \Gamma \vdash \mu(\Gamma \vdash t) \leq \tau ; 3) the resulting decidable G-canonical typing relation extends the F_\leq-minimum typing relation : if σ is the minimum type of t in \Gamma w.r.t. F_\leq, then \mu(\Gamma \vdash t) = σ in G, but not conversely, in general, since the F_\leq-minimum typing relation is undecidable. Additionally, as every decidable extension of the undecidable F_\leq should inevitably prove ``senseless'' F_\leq-unprovable judgments, we show that there exist extensions G approximating F_\leq with any desired precision. We investigate the properties of the G-typing relation. We prove, in particular, the G-typing proof normalization theorem, which gives conditions guaranteeing that a given typing proof in an extension can be transformed to a unique canonical form. It turns out that some G-typing proofs fail to normalize, and sometimes the minimum type property, valid for F_\leq, fails in the extensions. But we show that these pathological cases are {\em harmless}, corresponding to theF_\leq-untypable (i.e., senseless) terms ; so they can be ignored without influencing the decidability of typing in extensions.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D427 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00D427 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     CRIN:vorobyov94e
   |texte=   Extensions of F_\leq with Decidable Typing
}}