Extensions of F_\leq with Decidable Typing
Identifieur interne : 003129 ( Crin/Checkpoint ); précédent : 003128; suivant : 003130Extensions of F_\leq with Decidable Typing
Auteurs : S. VorobyovSource :
Abstract
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.
Links toward previous steps (curation, corpus...)
Links to Exploration step
CRIN:vorobyov94eLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="191">Extensions of F_\leq with Decidable Typing</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:vorobyov94e</idno>
<date when="1994" year="1994">1994</date>
<idno type="wicri:Area/Crin/Corpus">001506</idno>
<idno type="wicri:Area/Crin/Curation">001506</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001506</idno>
<idno type="wicri:Area/Crin/Checkpoint">003129</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">003129</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Extensions of F_\leq with Decidable Typing</title>
<author><name sortKey="Vorobyov, S" sort="Vorobyov, S" uniqKey="Vorobyov S" first="S." last="Vorobyov">S. Vorobyov</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="6707">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.</div>
</front>
</TEI>
<BibTex type="techreport"><ref>vorobyov94e</ref>
<crinnumber>94-R-127</crinnumber>
<category>15</category>
<equipe>PROGRAIS</equipe>
<author><e>Vorobyov, S.</e>
</author>
<title>Extensions of F_\leq with Decidable Typing</title>
<institution>Centre de Recherche en Informatique de Nancy</institution>
<year>1994</year>
<type>Rapport interne</type>
<address>Vandoeuvre-lès-Nancy</address>
<url>http://www.loria.fr/publications/1994/94-R-127/94-R-127.ps</url>
<abstract>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.</abstract>
</BibTex>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003129 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Checkpoint/biblio.hfd -nk 003129 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Crin |étape= Checkpoint |type= RBID |clé= CRIN:vorobyov94e |texte= Extensions of F_\leq with Decidable Typing }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |