Prova de Barendregt de redução de assunto para

12

Eu encontrei um problema na prova de redução de assunto de Barendregt (Thm 4.2.5 do cálculo Lambda com tipos ).

A última etapa da prova (página 60) diz:

"e, portanto, pelo lema 4.1.19 (1), . "Γ,x:ρP:σ

No entanto, de acordo com o Lema 4.1.19 (1) ele deve ser , uma vez que a substituição é feita para todo o contexto, não apenas a x : ρ ' .Γ[α:=τ],x:ρP:σx:ρ

Eu acho que a solução padrão pode ser de alguma forma provar que , mas não sei ao certo como.αFV(Γ)

Eu tinha uma prova para simplificá-lo, relaxando o lema de abstração da geração, mas descobri recentemente que houve um erro e minha prova está errada, por isso não tenho mais certeza de como resolver esse problema.

Alguém pode me dizer o que estou perdendo aqui?

Alejandro DC
fonte
Barendregt assume o chamado convenção variável, que nomes de variáveis ligadas e nomes de variáveis livres são padronizados para além , ou seja, assumimos implicitamente que eles são diferentes (usando -Conversão Talvez isso ajude..α
Dave Clarke
Γ,x:ρP:σΓ,x:ρP:σρ[α:=τ]=ρσ[α:=τ]=σ, então, usando esse lema, ele pode fazer a mesma substituição no contexto e o tipo inferido ao mesmo tempo ... mas ele apenas substitui no x: \ rho ', nem todo o contexto! E esse é o meu problema ...
Alejandro DC

Respostas:

8

Eu ainda acho que há uma imprecisão em como ele usa o lema. No entanto, existe uma solução (devo agradecer a Barbara Petit, que veio com a solução).

σ>ρ E se ΓP:σΓP:ρ

σ>α.σαFV(Γ)

Alejandro DC
fonte
Eu usei essa técnica em uma extensão do Sistema F para o cálculo lambda algébrico linear. O artigo com todos os detalhes da prova foi publicado hoje no LMCS 8 (1:11) .
Alejandro DC