User loginNavigation 
Weak normalisation theorem for typed lambdacalculusHi, There is something that seems strange to me. It says that: The degree &(T) of a type is defined by: The degree &(r) of a redex is defined by: Reading this it seems to me that a redex has the degree of its type. Am I wrong? Anyway, after it says: Note that, if r is a redex of type T, then &(r) > &(T). Why should &(r) be greater than &(T)? thanks, By ilSignorCarlo at 20071206 17:02  LtU Forum  previous forum topic  next forum topic  other blogs  3880 reads

Browse archivesActive forum topics 
Recent comments
59 min 48 sec ago
1 hour 32 min ago
4 hours 35 min ago
5 hours 1 min ago
6 hours 23 min ago
6 hours 28 min ago
6 hours 57 min ago
11 hours 54 min ago
11 hours 54 min ago
12 hours 6 min ago