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

Re: A decidable variant of Fsub



Your variant of Fsub is interesting.  Your rule (S-All-New) seems 
to say that 
 
    All(X<S1)S2 <  All(X<T1)T2 
            iff 
    (All(X<S1)S2)* <  (All(X<T1)T2)* 

where X does not occur in S1, T1, and A* is the "Pennsylvania translation" 
of A: 

    Top*         = Top
    (A -> B)*    = A* -> B*
    (All(X<A)B)* = All(X)(X->A*)->B*
    
(see Breazu-Tannen et al., Information and Computation, Vol. 93,  
no. 1).

With a bit of luck this may help in settling some of your questions, 
for example in claiming that no expressive power is lost with (S-All-New). 

Regards,
        Martin Abadi