[Prev][Next][Index][Thread]
Extensions of Fsub with Decidable Typing
Dear Phil,
I'd greatly appeciate it if you would announce the following paper.
Sincerely,
Sergei
----------------------------------------------------------------
The following paper
Extensions of Fsub with Decidable Typing
by Sergei Vorobyov
is now available by anonymous ftp.
FTP instructions:
ftp ftp.loria.fr
login: anonymous
password: <your mail address>
cd pub/loria/prograis/vorobyov
binary
get FsubDecTyping.dvi.Z (or FsubDecTyping.ps.Z)
MOSAIC:
ftp://ftp.loria.fr/pub/loria/prograis/vorobyov
--------------------------
Abstract. Both subtyping and typing relations in the system Fsub,
the well-known second-order polymorphic typed lambda-calculus with
subtyping [Cardelli-Wegner 85], [Bruce-Longo 90],
[Breazu-Coquand-Gunter-Scedrov 91], [Curien-Ghelli 92],
[Cardelli-Martini-Mitchell-Scedrov 94] appeared to be undecidable
[Pierce 92]. We demonstrate an infinite class of extensions of the
system Fsub, where both relations are decidable. Our
extensions are based on the converging hierarchies of decidable
extensions of the Fsub-subtyping relation (announced earlier).
Every system G from the class satisfies the following properties:
1) all subtyping and typing judgments provable in Fsub are also
G-provable; in particular, every Fsub-typable term is G-typable,
but not conversely: an Fsub-typable term may have additional types in
G, and there exist G-typable terms that are not Fsub-typable;
2) the G-canonical types, analogous to the Fsub-minimum types
[Curien-Ghelli 92], are {\em effectively computable} (as opposed to
Fsub); there exists a decision procedure, which given a context Gamma
and a term t always terminates yielding the G-canonical type
mu(Gamma |- t) of t in Gamma whenever it exists, and the result
"undefined" otherwise; canonical types are used to decide the typing
relation: Gamma |- t : tau iff Gamma |- mu(Gamma |- t) <: tau;
3) the resulting decidable} G-canonical typing relation extends the
Fsub-minimum typing relation: if sigma is the minimum type of t in
Gamma wrt Fsub, then mu(Gamma |- t) = sigma in G, but not conversely,
in general, since the Fsub-minimum typing relation is undecidable.
Additionally, as every decidable extension of the undecidable Fsub
should inevitably prove ``senseless'' Fsub-unprovable judgments, we
show that there exist extensions G approximating Fsub 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 Fsub [Curien-Ghelli92], fails in the extensions.
But we show that these pathological cases are {\em harmless},
corresponding to the Fsub-untypable (i.e., senseless) terms; so they
can be ignored without influencing the decidability of typing in
extensions.