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

Re: A decidable variant of Fsub




>>                 E |- T1 < S1        E, X<S1 |- S2 < T2 
>>                 ---------------------------------------        (S-All-Loc)
>>                    E |- All(X<S1)S2 <  All(X<T1)T2 
>> 
>> In particular, is subtyping for FSub with S-All-Loc decidable?

Unfortunately, it is not.  The problem remains essentially the same:
the "apparent bound" of the variable X changes between the conclusion
and the second premise.  All that has changed here is that it is the
free occurrences of X in T2 -- rather than S2 -- that get "re-bounded."

Giorgio Ghelli and I checked this last summer.  The proof is a
straightforward variant of the undecidability proof for the standard
version of Fsub (POPL '92).

Cheers,

        Benjamin Pierce