[Prev][Next][Index][Thread]
Fsub+recursive types: two FTP-papers
---------------------------------------------------------------------
The following two articles on Fsub and Fsub+recursive types are
available via anonymous FTP service ftp.loria.fr; see instructions at
the bottom. Comments are welcome.
---------------------------------------------------------------------
FsubTAPI.{dvi,ps}.Z
"Fsub: Bounded Quantification is NOT Essentially Undecidable"
Sergei Vorobyov
Abstract: Given an undecidable theory one usually tries to weaken it
to get a decidable subtheory. Yet, there sometimes exists another
possibility, to {\em reinforce} the undecidable theory in order to
obtain a decidable extension. This works only if the theory is {\em
NOT essentially undecidable}, i.e., possesses decidable extensions.
In POPL'92 B.Pierce proved the undecidability of subtyping relation in
Fsub, the second-order polymorphic typed \lambda-calculus with
subtyping, introduced by L.Cardelli and P.Wegner. We prove that Fsub
is not essentially undecidable.
To do that we introduce infinitely many ``Types-As-Propositions''
Interpretations for subtyping fragment of Fsub in S2S, the monadic
second-order theory of two successor functions, a decidable theory.
Under each such interpretattion any Fsub-axiom reads as a true formula
of S2S, and all Fsub-inference rules preserve validity w.r.t. any
interpretation, i.e., if a rule premises are interpreted as true then
so is the conclusion of the rule. This implies immediately that Fsub
is not essentially undecidable, possessing consistent decidable
extensions more powerful than Fsub.
We prove that there exists infinitely many different
S2S-interpretations of Fsub distinguishable by subtyping judgments,
and that there exist S2S-interpretations with infinitely many
incomparable types.
We then extend Fsub by two additional subtyping rules for quantified
types inherited from the Curry-style version of F, the second-order
polymorphic typed lambda-calculus. These rules allow one to compare a
quantified type with its particular cases, the feature absent in Fsub.
We prove that these rules are coherent with S2S-interpretations, i.e.,
preserve the validity w.r.t. any such interpretation. Again the
result on non-essential undecidability follows.
S2S-interpretations work equally good for other extension of Fsub by
additional rules, e.g., for type intersection rules, see the next paper.
---------------------------------------------------------------------
FsubREC.{dvi,ps}.Z
"Fsub with Recursive Types: ``Types-As-Propositions''
Interpretation in M. Rabin's S2S"
Sergei Vorobyov
Abstract: Subtyping judgments of polymorphic second-order typed
lambda-calculus Fsub extended by recursive types and different known
inference rules for these types could be interpreted in S2S, M.Rabin's
monadic second-order theory of two successor functions. On the one
hand, this provides a comprehensible model of the parametric and
inheritance polymorphisms over recursive types, on the other, proves
that the corresponding subtyping theories are not essentially
undecidable, i.e., possess consistent decidable extensions.
---------------------------------------------------------------------
Instructions to follow:
ftp ftp.loria.fr
Name: anonymous
Password: send your e-mail address as password
cd Equipe-Projet/prograis
binary
get FsubTAPI.dvi.Z or
get FsubTAPI.ps.Z
get FsubREC.dvi.Z or
get FsubREC.ps.Z
bye
uncompress FsubTAPI.dvi.Z or
uncompress FsubTAPI.ps.Z
uncompress FsubREC.dvi.Z or
uncompress FsubREC.ps.Z