[Prev][Next][Index][Thread]

Re: A decidable variant of Fsub





>	From: Giuseppe Castagna <castagna@dmi.ens.fr>
>	Date: Wed, 17 Feb 1993 14:15:49 +0100
>
>	The Fsub subtyping rule for comparing quantified types [CG92]
>
>                E |- T1 < S1        E, X<T1 |- S2 < T2 
>                --------------------------------------            (S-All-Orig)
>                   E |- All(X<S1)S2 <  All(X<T1)T2 
>
>	has often been the subject of discussion in this list and elsewhere.
>	[...]
>	The crux of the problem is that the upper bound of the bound
>	    ^^^^
>	variable X in S2 changes from S1 in the rule's conclusion to T1
>	in the right-hand premise
>	[...]
>	Other variants of (S-All-Orig) have been proposed [e.g. K92],
>	but we are not presently aware of any investigation of one
>	especially simple and appealing alternative,
>
>                E |- T1 < S1        E, X<Top |- S2 < T2 
>                ---------------------------------------            (S-All-New)
>                   E |- All(X<S1)S2 <  All(X<T1)T2 
>
>	[...] The subtyping problem for Fsub with (S-All-New) instead of
>	(S-All-Orig) is decidable.

If the above is indeed the crux of the problem, then the advantages of
S-All-New over

                E |- T1 < S1        E, X<S1 |- S2 < T2 
                ---------------------------------------            (S-All-Loc)
                   E |- All(X<S1)S2 <  All(X<T1)T2 

are not apparent.  Here X is taken to be LOCal to the prevailing types,
for which S1 presents itself as the obvious bound for defining this
neighborhood.

In particular, is subtyping for FSub with S-All-Loc decidable?

Vaughan Pratt