Comprendre la preuve d'une forte normalisation du calcul des constructions

J'ai du mal à comprendre la preuve d'une forte normalisation pour le calcul des constructions. J'essaye de suivre la preuve dans le papier de Herman Geuvers "Une preuve courte et flexible de Normalisation Forte pour le Calcul des Constructions".

Je peux bien suivre le raisonnement principal. Geuvers construit pour chaque type $T$ une interprétation $[\![T]\!]_\xi$ basé sur une évaluation des variables de type$\xi(\alpha)$ . Et puis il construit une certaine interprétation du terme$(\!|M|\!)_\rho$ basé sur une évaluation des variables de terme$\rho(x)$ et prouve que pour des évaluations valides, l'affirmation$(\!|M|\!)_\rho \in [\![T]\!]_\xi$ pour tous$\Gamma\vdash M:T$ est valable.

Mon problème: pour les types faciles (comme les types système F), l'interprétation de type $[\![T]\!]_\xi$ est vraiment un ensemble de termes, donc l'assertion$(\!|M|\!)_\rho \in [\![T]\!]_\xi$ est logique. Mais pour les types plus complexes, l'interprétation$[\![T]\!]_\xi$ n'est pas un ensemble de termes mais un ensemble de fonctions d'un espace fonctionnel approprié. Je pense que je comprends presque la construction des espaces fonctionnels, mais elle ne peut attribuer aucun sens à$(\!|M|\!)_\rho \in [\![T]\!]_\xi$ pour les types plus complexes$T$ .

Quelqu'un peut-il expliquer ou donner des liens vers des présentations plus compréhensibles de la preuve?

Edit: Permettez-moi d'essayer de rendre la question plus claire. Un contexte $\Gamma$ a des déclarations pour les variables de type $\alpha:A$ et les variables d'objet. Une évaluation de type est valide, si pour tous $(\alpha:A) \in \Gamma$ avec $\Gamma\vdash A:\square$ alors $\xi(\alpha) \in \nu(A)$ est valide. Mais $\nu(A)$ peut être un élément de $(SAT)^*$ et pas seulement $SAT$. Par conséquent, aucune évaluation de terme valide ne peut être définie pour $\rho(\alpha)$ . $\rho(\alpha)$ doit être un terme et non une fonction d'un espace de fonction.

Edit 2: Exemple qui ne fonctionne pas

Faisons la dérivation valide suivante:

$$\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}$$

Dans le dernier contexte, une évaluation de type valide doit satisfaire $\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$ . Pour ce type d'évaluation, il n'y a pas d'évaluation de terme valide.

Malheureusement, je ne suis pas sûr qu'il y ait plus de ressources conviviales pour les débutants que le compte de Geuvers. Vous pourriez essayer cette note de Chris Casinghino qui donne un compte rendu de plusieurs preuves dans des détails atroces.

Je ne suis pas sûr de comprendre l'essentiel de votre confusion, mais je pense qu'une chose importante à noter est le lemme suivant (Corollaire 5.2.14), prouvé dans le texte classique de Barendregt :

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

$[\![T]\!]_\xi$ $\Gamma \vdash M:T$$[\![T]\!]_\xi$

$(\!|t|\!)_\sigma\in[\![T]\!]_\xi$$\Gamma \vdash t:T :*$${\cal V}(*)\subseteq{\cal P}(\mathrm{Term})$${\cal V}(*)=\mathrm{SAT}$

$*$$\mathrm{SAT}^*$$*$$\square$