[POPLmark] Experience report with Twelf

Jevgenijs Sallinens jevgenijs at dva.lv
Wed Aug 31 15:54:56 EDT 2005


Quoting "Brian E. Aydemir" <baydemir at cis.upenn.edu>:

> 
> Unlike in Featherweight Java, a derivation of "t1 --> t2" in F-sub  
> does not require the construction of any subtyping derivations.   
> Thus, the undecidability of the subtyping and typing relations does  
> not necessarily imply that the evaluation relation is also undecidable.
> 

Brian,

Thank you for confirmation on undecidabilty of F-sub.
I think it could be important aspect for 'challengers'.
As per evaluation relation : if we consider only one step of reduction then
it is decidable (and presented as explicit operator to bool in my submission),
but it should be imposible to decide in general if t1 could be reduced to
t2 with some unknown number of steps, since otherwise we would have something 
like strong normalization and usually it implies decidability of typing 
relation.

Best Regards,
Jevgenijs Sallinens.      



-------------------------------------------------
This mail sent through IMP: http://webmail.dva.lv/



More information about the Poplmark mailing list