Re: A decidable variant of Fsub

• To: pratt@CS.Stanford.EDU
• Subject: Re: A decidable variant of Fsub
• From: pierce@quincy.inria.fr
• Date: Tue, 23 Feb 93 12:58:49 N
• Approved: types@dcs.gla.ac.uk

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

• Prev: Hypercoherences
• Next: references on partial comb algebras
• Index(es):
  • Main
  • Thread