Prueba de Barendregt de reducción de sujeto para

Encontré un problema en la prueba de reducción de sujetos de Barendregt (Thm 4.2.5 de cálculos Lambda con tipos ).

El último paso de la prueba (página 60) dice:

"y, por lo tanto, según el Lema 4.1.19 (1), $\quad\Gamma,x:\rho\vdash P:\sigma'$ ".

Sin embargo, de acuerdo con el Lema 4.1.19 (1) debe ser $\Gamma[\vec{\alpha}:=\vec{\tau}],x:\rho\vdash P:\sigma'$ , ya que la sustitución se realiza en todo el contexto, no solo en $x:\rho'$ .

Supongo que la solución estándar puede ser demostrar de alguna manera que $\vec{\alpha}\notin FV(\Gamma)$ , pero no estoy seguro de cómo.

Tenía una prueba que lo simplificaba al relajar el lema generacional de las abstracciones, pero recientemente descubrí que había un error y mi prueba es incorrecta, por lo que ya no estoy seguro de cómo resolver este problema.

¿Alguien, por favor, puede decirme lo que me falta aquí?

lo.logic type-theory lambda-calculus proof-theory Alejandro DC
fuente

Barendregt asume la llamada convención de variables, que los nombres de variables enlazadas y los nombres de variables libres están estandarizados , es decir, suponemos implícitamente que son diferentes (usando la conversión

. Tal vez esto ayude.)

α

$\alpha$

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

Respuestas:

Todavía creo que hay una imprecisión en cómo usa el lema. Sin embargo, hay una solución (debo agradecer a Barbara Petit que vino con la solución).

De hecho, la solución proviene de la definición de (def. 4.2.1), que es moralmente esto: $\geq$

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

Sin embargo, en lugar de definirlo de esa manera, define la relación solo en términos de los tipos. La ventaja de definirlo en términos de secuenciantes es que podemos deducir que si , entonces , que es exactamente lo que necesita en la prueba (y de donde viene la imprecisión). $\sigma>\forall\alpha.\sigma$ $\alpha\notin FV(\Gamma)$

Alejandro DC
fuente

He usado esta técnica en una extensión del Sistema F para el cálculo lambda lineal-algebraico. El documento con todos los detalles de la prueba ha aparecido hoy en LMCS 8 (1:11) .

Alejandro DC