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

Select your preferred way to display the comments and click "Save settings" to activate your changes.

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.