F_\leq~ : Bounded Quantification is NOT Essentially Undecidable
Identifieur interne : 001411 ( Crin/Curation ); 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 toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001411
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><idno type="wicri:Area/Crin/Curation">001411</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">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/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001411 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/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= Curation
|type= RBID
|clé= CRIN:vorobyov94a
|texte= F_\leq~ : Bounded Quantification is NOT Essentially Undecidable
}}
| This area was generated with Dilib version V0.6.33. |  |