Preuve de Barendregt de réduction de sujet pour

J'ai trouvé un problème dans la preuve de réduction de sujet de Barendregt (Thm 4.2.5 des calculs Lambda avec types ).

La dernière étape de la preuve (page 60), dit:

"et donc par le lemme 4.1.19 (1), $\quad\Gamma,x:\rho\vdash P:\sigma'$ . "

Cependant, selon le lemme 4.1.19 (1), il devrait être , puisque la substitution est faite à l'ensemble du contexte, pas seulement à . $\Gamma[\vec{\alpha}:=\vec{\tau}],x:\rho\vdash P:\sigma'$ $x:\rho'$

Je suppose que la solution standard pourrait être de prouver d'une manière ou d'une autre que , mais je ne sais pas comment. $\vec{\alpha}\notin FV(\Gamma)$

J'avais une preuve le simplifiant en assouplissant le lemme de génération des abstractions, mais j'ai récemment découvert qu'il y avait une erreur et ma preuve est fausse, donc je ne sais plus comment résoudre ce problème.

Quelqu'un peut-il me dire ce qui me manque ici?

lo.logic type-theory lambda-calculus proof-theory Alejandro DC
la source

Barendregt suppose la convention dite des variables, selon laquelle les noms de variables liées et les noms de variables libres sont standardisés séparément , à savoir, nous supposons implicitement qu'ils sont différents (en utilisant la conversion

α

$\alpha$ . Peut-être que cela aide.

Dave Clarke

Γ, x : ρ ⊢ P : σ^{'}

$\Gamma,x:\rho\vdash P:\sigma'$

Γ, x : ρ^{'} ⊢ P : σ^{″}

$\Gamma,x:\rho'\vdash P:\sigma''$

ρ^{'} [\vec{α} := \vec{τ}] = ρ

$\rho'[\vec{\alpha}:=\vec{\tau}]=\rho$

σ^{″} [\vec{α} := \vec{τ}] = σ^{'}

$\sigma''[\vec{\alpha}:=\vec{\tau}]=\sigma'$

Alejandro DC

Réponses:

Je pense toujours qu'il y a une imprécision dans la façon dont il utilise le lemme. Cependant il y a une solution (je dois remercier Barbara Petit qui est venue avec la solution).

En fait, la solution vient de la définition de (déf. 4.2.1), qui est moralement la suivante: $\geq$

$\sigma>\rho\quad$ if $\quad\dfrac{\Gamma\vdash P:\sigma}{\Gamma\vdash P:\rho}$

Cependant, au lieu de la définir de cette façon, il définit la relation uniquement en termes de types. L'avantage de le définir en termes de séquences, est que l'on peut en déduire que si , alors , ce qui est exactement ce dont il a besoin dans la preuve (et d'où vient l'imprécision). $\sigma>\forall\alpha.\sigma$ $\alpha\notin FV(\Gamma)$

Alejandro DC
la source

J'ai utilisé cette technique dans une extension du système F pour le lambda-calcul linéaire-algébrique. Le papier avec tous les détails de la preuve est paru aujourd'hui dans LMCS 8 (1:11) .

Alejandro DC