F_\leq~ : Bounded Quantification is NOT Essentially Undecidable
Identifieur interne : 001411 ( Crin/Corpus ); précédent : 001410; suivant : 001412F_\leq~ : Bounded Quantification is NOT Essentially Undecidable
Auteurs : S. VorobyovSource :
English descriptors
Abstract
Given an undecidable theory T one usually tries to weaken it to get a decidable subtheory T_0\subseteq T. Yet, there sometimes exists another possibility, to {\em reinforce} the undecidable T in order to obtain a decidable extension T_0\supseteq T. This works only if T is {\em not essentially undecidable}, i.e., possesses decidable extensions. In 1992 B.Pierce proved the undecidability of subtyping relation in F_\leq, the second-order polymorphic typed λ-calculus with subtyping, introduced by L.Cardelli and P.Wegner in 1985. We prove that F_\leq is not essentially undecidable. To do that we introduce infinitely many ``{\em Types-As-Propositions}'' {\em Interpretations} for subtyping fragment of F_\leq in S2S, the monadic second-order theory of two successor functions, a decidable theory. Under each such interpretation any axiom of F_\leq reads as a true formula of S2S, and all F_\leq-inference rules preserve validity wrt any interpretation, i.e., if a rule premises are interpreted as true then so is the conclusion of the rule. This implies immediately that F_\leq is not essentially undecidable, possessing consistent decidable extensions more powerful than F_\leq. We prove that there exists infinitely many different interpretations distinguishable by subtyping judgments, and that there exist interpretations with infinitely many incomparable types. We then extend F_\leq by two additional subtyping rules for quantified types inherited from the Curry-style version of the second-order polymorphic typed λ-calculus. These rules allow one to compare a quantified type with its particular cases, the feature absent in F_\leq. We prove that these rules are coherent with our interpretations, i.e., preserve the validity wrt. any such interpretation. Again the result on non-essential undecidability holds. Finally we show that our interpretations work equally good for other extension of F_\leq by additional rules, e.g., for type intersection rules.
Links to Exploration step
CRIN:vorobyov94aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="239">F_\leq~ : Bounded Quantification is NOT Essentially Undecidable</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:vorobyov94a</idno>
<date when="1994" year="1994">1994</date>
<idno type="wicri:Area/Crin/Corpus">001411</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">F_\leq~ : Bounded Quantification is NOT Essentially Undecidable</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><keywords scheme="KwdEn" xml:lang="en"><term>polymorphism</term>
<term>second-order polymorphic typed calculus</term>
<term>subtyping relation</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="3373">Given an undecidable theory T one usually tries to weaken it to get a decidable subtheory T_0\subseteq T. Yet, there sometimes exists another possibility, to {\em reinforce} the undecidable T in order to obtain a decidable extension T_0\supseteq T. This works only if T is {\em not essentially undecidable}, i.e., possesses decidable extensions. In 1992 B.Pierce proved the undecidability of subtyping relation in F_\leq, the second-order polymorphic typed λ-calculus with subtyping, introduced by L.Cardelli and P.Wegner in 1985. We prove that F_\leq is not essentially undecidable. To do that we introduce infinitely many ``{\em Types-As-Propositions}'' {\em Interpretations} for subtyping fragment of F_\leq in S2S, the monadic second-order theory of two successor functions, a decidable theory. Under each such interpretation any axiom of F_\leq reads as a true formula of S2S, and all F_\leq-inference rules preserve validity wrt any interpretation, i.e., if a rule premises are interpreted as true then so is the conclusion of the rule. This implies immediately that F_\leq is not essentially undecidable, possessing consistent decidable extensions more powerful than F_\leq. We prove that there exists infinitely many different interpretations distinguishable by subtyping judgments, and that there exist interpretations with infinitely many incomparable types. We then extend F_\leq by two additional subtyping rules for quantified types inherited from the Curry-style version of the second-order polymorphic typed λ-calculus. These rules allow one to compare a quantified type with its particular cases, the feature absent in F_\leq. We prove that these rules are coherent with our interpretations, i.e., preserve the validity wrt. any such interpretation. Again the result on non-essential undecidability holds. Finally we show that our interpretations work equally good for other extension of F_\leq by additional rules, e.g., for type intersection rules.</div>
</front>
</TEI>
<BibTex type="techreport"><ref>vorobyov94a</ref>
<crinnumber>94-R-018</crinnumber>
<category>15</category>
<equipe>PROGRAIS</equipe>
<author><e>Vorobyov, S.</e>
</author>
<title>F_\leq~ : Bounded Quantification is NOT Essentially Undecidable</title>
<institution>Centre de Recherche en Informatique de Nancy</institution>
<year>1994</year>
<type>Rapport interne</type>
<address>Vandoeuvre-lès-Nancy</address>
<keywords><e>second-order polymorphic typed calculus</e>
<e>subtyping relation</e>
<e>polymorphism</e>
</keywords>
<abstract>Given an undecidable theory T one usually tries to weaken it to get a decidable subtheory T_0\subseteq T. Yet, there sometimes exists another possibility, to {\em reinforce} the undecidable T in order to obtain a decidable extension T_0\supseteq T. This works only if T is {\em not essentially undecidable}, i.e., possesses decidable extensions. In 1992 B.Pierce proved the undecidability of subtyping relation in F_\leq, the second-order polymorphic typed λ-calculus with subtyping, introduced by L.Cardelli and P.Wegner in 1985. We prove that F_\leq is not essentially undecidable. To do that we introduce infinitely many ``{\em Types-As-Propositions}'' {\em Interpretations} for subtyping fragment of F_\leq in S2S, the monadic second-order theory of two successor functions, a decidable theory. Under each such interpretation any axiom of F_\leq reads as a true formula of S2S, and all F_\leq-inference rules preserve validity wrt any interpretation, i.e., if a rule premises are interpreted as true then so is the conclusion of the rule. This implies immediately that F_\leq is not essentially undecidable, possessing consistent decidable extensions more powerful than F_\leq. We prove that there exists infinitely many different interpretations distinguishable by subtyping judgments, and that there exist interpretations with infinitely many incomparable types. We then extend F_\leq by two additional subtyping rules for quantified types inherited from the Curry-style version of the second-order polymorphic typed λ-calculus. These rules allow one to compare a quantified type with its particular cases, the feature absent in F_\leq. We prove that these rules are coherent with our interpretations, i.e., preserve the validity wrt. any such interpretation. Again the result on non-essential undecidability holds. Finally we show that our interpretations work equally good for other extension of F_\leq by additional rules, e.g., for type intersection rules.</abstract>
</BibTex>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001411 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 001411 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Crin |étape= Corpus |type= RBID |clé= CRIN:vorobyov94a |texte= F_\leq~ : Bounded Quantification is NOT Essentially Undecidable }}
This area was generated with Dilib version V0.6.33. |