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

9

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]]ξ basé sur une évaluation des variables de typeξ(α) . Et puis il construit une certaine interprétation du terme(|M|)ρ basé sur une évaluation des variables de termeρ(x) et prouve que pour des évaluations valides, l'affirmation(|M|)ρ[[T]]ξ pour tousΓM:T est valable.

Mon problème: pour les types faciles (comme les types système F), l'interprétation de type [[T]]ξ est vraiment un ensemble de termes, donc l'assertion(|M|)ρ[[T]]ξ est logique. Mais pour les types plus complexes, l'interprétation[[T]]ξ 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|)ρ[[T]]ξ pour les types plus complexesT .

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 Γ a des déclarations pour les variables de type α:A et les variables d'objet. Une évaluation de type est valide, si pour tous (α:A)Γ avec ΓA: alors ξ(α)ν(A) est valide. Mais ν(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 ρ(α) . ρ(α) 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:

[]:axiom[α:]α:variable introduction[α:]:weaken[](Πα:.):product formation[β:Πα:.]β:(Πα:.)variable introduction

Dans le dernier contexte, une évaluation de type valide doit satisfaire ξ(β)ν(Πα:.)={f|f:SATSAT} . Pour ce type d'évaluation, il n'y a pas d'évaluation de terme valide.

helmut
la source
1
La moitié des personnes lisant ceci penseront que est SAT. Vous devez expliquer ce que c'est. De plus, votre dérivation semble un peu étrange. La deuxième ligne ne doit pas mentionner α dans sa conclusion, elle devrait lire quelque chose comme [ α : ] : , n'est-ce pas? SATα[α:]:
Andrej Bauer
SATΓT:sΓ,x:Tx:Ts
Je comprends comment vous avez obtenu la deuxième ligne, mais ce n'est pas la bonne prémisse pour la formation de la troisième ligne, n'est-ce pas? Quelle règle donne la troisième ligne.
Andrej Bauer
r(s1,s2,s3;ΓA:s1;Γ,x:AB:s2Γ(Πx:A.B):s3r(,,)
[]:α:.αα:.

Réponses:

6

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 :

ΓM:T  ΓT: or 

[[T]]ξ ΓM:T[[T]]ξ

(|t|)σ[[T]]ξΓt:T:V()P(Term)V()=SAT

SAT

cody
la source
1
Merci pour l'explication. Cela résout mon problème de ne pas comprendre les fonctions utilisées dans la preuve de Geuver. J'avais déjà un soupçon en lisant et en relisant le papier de Geuver, mais vous l'avez rendu clair.
helmut