Is there a proof of strong normalisation that uses ordinal numbers?

Question

I am currently trying to find a proof for strong normalisation of an extension of $\lambda$-calculus. I've tried several approaches and one would be to assign an ordinal number $\operatorname{cs}(t)$ to each term $t$ in the calculus, and then show that this assigned ordinal number at least does not increase under any reduction and is reduced in certain cases. Then one could conclude that these certain cases can only occur a finite number of times in each reduction chain.

Is there a proof of strong normalisation for any calculus which uses ordinal numbers in this way?

Answer 1

I believe that Chapter 4 of Girard's Proofs and Types proves weak normalization for typed $\lambda$-calculus in this way, using ordinals up to $\omega^2$.

He first assigns a natural number "degree" to any type, then to any redex (the degree of the type of its discriminee), then to any term (the maximum degree of its redexes). Then he shows that degree is nonincreasing under reduction, and that moreover it is always possible to choose a redex to reduce such that either the degree of the term decreases or the number of redexes of maximal degree decreases. This provides a pair of natural numbers (i.e. an ordinal $\omega\cdot n + m$ less than $\omega^2$) that can always be made to decrease lexicographically, so that there must be a terminating reduction sequence.

I don't know whether this can be adapted to strong normalization.

Answer 2

As far as I know, such a strong normalization proof is not known even for the simply-typed $\lambda$-calculus. It is mentioned as Problem 26 in the TLCA List of Open Problems.

(It must be noted though that the list does not seem to have been updated since 2014, so the problem might have been solved in the meantime. I personally doubt it, but who knows!).