Understanding the Proof of Strong Normalization of the Calculus of Constructions

Question

I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong Normalization for the Calculus of Constructions".

I can follow the main line of reasoning well. Geuvers constructs for each type $T$ an interpretation $[\![T]\!]_\xi$ based on some evaluation of type variables $\xi(\alpha)$. And then he constructs some term interpretation $(\!|M|\!)_\rho$ based on some evaluation of term variables $\rho(x)$ and proves that for valid evaluations the assertion $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ for all $\Gamma\vdash M:T$ holds.

My problem: For easy types (like system F types) the type interpretation $[\![T]\!]_\xi$ is really a set of terms, so the assertion $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ makes sense. But for more complex types the interpretation $[\![T]\!]_\xi$ is not a set of terms but a set of functions of some appropriate function space. I think, I almost understand the construction of the function spaces, however it cannot assign any meaning to $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ for the more complex types $T$.

Can anybody explain or give links to some more understandable presentations of the proof?

Edit: Let me try to make the question clearer. A context $\Gamma$ has declarations for type variables $\alpha:A$ and object variables. A type valuation is valid, if for all $(\alpha:A) \in \Gamma$ with $\Gamma\vdash A:\square$ then $\xi(\alpha) \in \nu(A)$ is valid. But $\nu(A)$ can be an element of $(SAT)^*$ and not only $SAT$. Therefore no valid term evaluation can be defined for $\rho(\alpha)$. $\rho(\alpha)$ must be a term and not some function of a function space.

Edit 2: Example which does not work

Let's make the following valid derivation: $$ \begin{array}{llll} [] &\vdash & *:\square &\text{axiom} \\ [\alpha:*] &\vdash& \alpha:* &\text{variable introduction} \\ [\alpha:*] &\vdash& *:\square &\text{weaken} \\ [] &\vdash & (\Pi \alpha:*.*):\square &\text{product formation} \\ [\beta:\Pi \alpha:*.*] &\vdash& \beta:(\Pi \alpha:*.*) &\text{variable introduction} \end{array} $$

In the last context a valid type evaluation must satisfy $\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$. For this type evaluation there is no valid term evaluation.

Answer 1

Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try this note from Chris Casinghino which gives an account of several proofs in excruciating detail.

I'm not sure I understand the gist of your confusion, but I think one important thing to note, is the following lemma (Corollary 5.2.14), proven in the classic Barendregt text:

$$\Gamma \vdash M:T\ \Rightarrow\ \Gamma \vdash T:*\mbox{ or }\square $$

This means that while $[\![T]\!]_\xi$ can be some complicated function, if $\Gamma \vdash M:T$ holds, then $[\![T]\!]_\xi$ has to be a set of terms.

This is insinuated in the outline (section 3.1), where $(\!|t|\!)_\sigma\in[\![T]\!]_\xi$ only if $\Gamma \vdash t:T :*$, which lines up with our expectation, which is that the interpretation of a type must be a set of terms, i.e. ${\cal V}(*)\subseteq{\cal P}(\mathrm{Term})$ (indeed, ${\cal V}(*)=\mathrm{SAT}$!)

It's a common situation in type theory that even though we're only interested in the "base kind" (here $*$), we still have to define semantics for things at higher kinds (hence the need to introduce $\mathrm{SAT}^*$). Things then work out at the end, because only kind which inhabited by types is $*$ (and $\square$, but that's not really important).