Hierarchies of decidable extensions of Fsub

To: types@dcs.gla.ac.uk
Subject: Hierarchies of decidable extensions of Fsub
From: Serge Vorobyov <Serge.Vorobyov@loria.fr>
Date: Thu, 18 Aug 1994 10:49:45 +0200
Approved: types@dcs.gla.ac.uk
--------------------------------------------------------------------
The following paper is available by anonymous ftp from 
	   ftp.loria.fr
directory: pub/loria/prograis/vorobyov
files:	   FsubHi.{dvi,ps}.Z

or by xmosaic ftp://ftp.loria.fr/pub/loria/prograis/vorobyov
====================================================================

	Hierarchies of Decidable Extensions of
		Bounded Quantification
		   Sergei Vorobyov

Fsub, the second-order polymorphic typed lambda-calculus with
subtyping and bounded universal type quantification [Cardelli-Wegner
85, Bruce-Longo 90, Curien-Ghelli 92, Pierce 92,
Cardelli-Martini-Mitchell-Scedrov 94, ...], appears to be undecidable
[Pierce 92] because of undecidability of its subtyping component.
Attempts were made to obtain decidable type systems with subtyping by
weakening Fsub [Castagna-Pierce 94, Katiyar-Sankar-92], and also by
reinforcing or extending it [Vorobyov94]. However, for the moment,
these extensions lack the important proof-theoretic {\em minimum type
property}, which holds for Fsub and guarantees that each typable term
has the minimum type, being a subtype of any other type of the term
[Curien-Ghelli 92].

As a preparation step to introducing the extensions of Fsub with the
minimum type property and the decidable term typing relation, we
define and study an infinite class of hierarchies of decidable
extensions of the Fsub subtyping relation. We demonstrate conditions
providing that:

1) every theory in a hierarchy extends Fsub, i.e., proves everything
Fsub-provable;

2) every theory in a hierarchy is transitive:

	G |- S1 <: S2 and G |- S2 <: S3  imply  G |- S1 <: S3

3) every theory in a hierarchy satisfies the substitution property for
boundedly quantified universal types:

	G,|- (All A<:S1.S2) <: (All A<:R1.R2)  and  G |- Q <: R1 

		imply  G |- S2[Q/a] <: R2[Q/a]

(transitivity and substitutivity are indispensable for the
minimum type property and typing proof normalization);

4) a hierarchy condenses: $T(i+1) \subseteq T(i)$ for every i,
and converges to Fsub:

\[\lim_{n\arr\infty} T(i) = \bigcap_{n=0}^\infty T(i) = Fsub\]

5) a hierarchy collapses: T(i) = T(i+1) for every i