## Weak normalisation theorem for typed lambda-calculus

Hi,
I read the proof of the weak normalisation theorem on the book Proofs and Types, on the chapter 4.

There is something that seems strange to me.

It says that:

The degree &(T) of a type is defined by:
- &(Ti) = 1 if Ti is atomic.
- &(U x V) = &(U -> V) = max(&(U), &(V)) + 1

The degree &(r) of a redex is defined by:
- &(fst) = &(snd) = &(U x V) where U x V is the type of
- &((\x.v)u) = &(U -> V) where U -> V is the type of (\x.v)

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

## Comment viewing options

### Explanation

(Your definition for the redex degree of the projections got garbled by the HTML-filter).

Here are some examples . Suppose T is atomic and X is a normal form of type T.

• &(T) = 1
• &(T x T) = max (&(T), &(T)) + 1 = 2
• &(X) = 0
• &(fst <X, X>) = &(T x T) = 2

So the redex degree in the last line is equal to the degree of the tuple type and not equal to the degree of the type of the first element.

(edit: fixed tuple type syntax)

### By the way, does anyone have

By the way, does anyone have any suggestions as to how I might legally obtain a reasonably priced copy of this book? The cheapest listing on amazon.co.uk at the moment is Â£211.44. It's only a little book.

### Free

There's a downloadable version on Paul Taylor's web pages.

### Excellent! Thank you.

Excellent! Thank you.