User loginNavigation |
Weak normalisation theorem for typed lambda-calculusHi, 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 2007-12-06 17:02 | LtU Forum | previous forum topic | next forum topic | other blogs | 5231 reads
|
Browse archives
Active forum topics |
Recent comments
32 weeks 6 days ago
32 weeks 6 days ago
32 weeks 6 days ago
1 year 3 weeks ago
1 year 7 weeks ago
1 year 8 weeks ago
1 year 8 weeks ago
1 year 11 weeks ago
1 year 16 weeks ago
1 year 16 weeks ago