[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