[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.