A polymorphic type system {\cal T} taking in consideration subtyping relations on types, like well-known F_\leq or its variants usually consists of two separate parts : \bullet\ {\cal T}^ :, a system assigning types to terms, t :\tau, t is of type σ, and \bullet\ {\cal T}^\leq, a system for subtyping types \tau\leqσ, \tau is a subtype of σ, interacting by the so-called {\em (Subsumption)} rule promoting a type of a term to any supertype : if a term t is of type \tau and \tau is a subtype of σ then t is of type σ (formally, t :\tau\ ;\&\ ;\tau\leqσ\ ;\Rightarrow\ ;t :σ). In presence of {\em (Subsumption)} terms, in contrast to the case of Girard-Reynold's system F, are no longer uniquely typed and typing proofs are no longer unique. This poses numerous semantic problems. Curien and Ghelli in 1992 established semantic coherence for standard F_\leq : they proved that any typing proof in F_\leq can be transformed into a unique normal form with the property that all normal typing proofs assigning different types to the same term differ only by the final applications of {\em (Subsumption)}. They also proved the existence of a {\em least} type for any F_\leq-typable term in a given context, being a subtype of all other types of the term in the same context. In this paper we address the following general problem. Fix a typing subsystem {\cal T}^ : as the Girard-Reynolds-style second-order polymorphic type system based on usual \rightarrow/\forall-introductions and eliminations. Vary the subtyping part {\cal T}^\leq. What is needed for the the existence and unicity of normal form proofs and existence of least types in the resulting system? This problem becomes very important since Piercés discovery of undecidability of subtyping in F_\leq. What are the general guidelines one should follow trying to modify subtyping rules of F_\leq in order to gain decidability without loosing existence and unicity of normal form proofs and least types? Why decidable weakening of F_\leq, Castagna-Piercés system F_\leq^\top has no least typing property? Our main motivation was to investigate normalization and least typability for infinite classes of decidable extensions of F_\leq we introduced earlier. We solve this problem in general here. We show that in fact very little is needed for a system to possess unique normal proofs and least types. Just simple structural properties, like transitivity, substitutivity, and certain rule inversion properties suffice. Rule inversion is a well-known proof-theoretic notion guaranteeing that the premises of a rule are provable whenever the conclusion is. Our general result applies equally good to F_\leq, to original Cardelli-Wegner {\em Fun}, as well as to decidable subtyping extensions F_\leq^{S2S} of F_\leq we introduced recently. Our proof explains clearly what is missing in Castagna-Piercés system F_\leq^\top, which is decidable, but possesses no least typing property. We use the old Gentzen-style rule permutation technique combined with transfinite induction on trees, without any explicit coercions and rewriting on coercions . Explicit rule permutability proofs show transparently what hypotheses concerning subtyping relation are really necessary to obtain normalization and least typing.

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

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

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     CRIN:vorobyov94b
   |texte=   Polymorphic Typing with Subtyping : Proof Normalization and Least Types for the F Clone
}}