Compreendendo a prova de forte normalização do cálculo de construções

Tenho dificuldades em entender a prova de forte normalização para o cálculo de construções. Tento seguir a prova no artigo de Herman Geuvers "Uma prova curta e flexível de Normalização Forte para o Cálculo de Construções".

Eu posso seguir bem a linha principal de raciocínio. Geuvers constrói para cada tipo uma interpretação base em alguma avaliação das variáveis de tipo . E então ele constrói alguma interpretação de termo base em alguma avaliação das variáveis de termo e prova que, para avaliações válidas, a asserção para todos os mantém. $T$ $[\![T]\!]_\xi$ $\xi(\alpha)$ $(\!|M|\!)_\rho$ $\rho(x)$ $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ $\Gamma\vdash M:T$

Meu problema: para tipos fáceis (como tipos do sistema F), a interpretação do tipo $[\![T]\!]_\xi$ é realmente um conjunto de termos, portanto a asserção $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ faz sentido. Porém, para tipos mais complexos, a interpretação $[\![T]\!]_\xi$ não é um conjunto de termos, mas um conjunto de funções de algum espaço funcional apropriado. Eu acho que quase entendo a construção dos espaços funcionais, mas ele não pode atribuir nenhum significado a $(\!|M|\!)_\rho \in [\![T]\!]_\xi$ para os mais complexos tipos $T$ .

Alguém pode explicar ou fornecer links para algumas apresentações mais compreensíveis da prova?

Edit: Deixe-me tentar esclarecer a questão. Um contexto $\Gamma$ possui declarações para as variáveis de tipo $\alpha:A$ e variáveis de objeto. Uma avaliação de tipo é válida se, para todos $(\alpha:A) \in \Gamma$ com $\Gamma\vdash A:\square$ então $\xi(\alpha) \in \nu(A)$ for válido. Mas $\nu(A)$ pode ser um elemento de $(SAT)^*$ e não apenas $SAT$ . Portanto, nenhuma avaliação de termo válida pode ser definida para $\rho(\alpha)$ . $\rho(\alpha)$ deve ser um termo e não uma função de um espaço de função.

Edit 2: Exemplo que não funciona

Vamos fazer a seguinte derivação válida:

\begin{array}{llll} [] & ⊢ & * : ◻ & axiom \\ [α : *] & ⊢ & α : * & variable introduction \\ [α : *] & ⊢ & * : ◻ & weaken \\ [] & ⊢ & (Π α : * . *) : ◻ & product formation \\ [β : Π α : * . *] & ⊢ & β : (Π α : * . *) & variable introduction \end{array}

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

No último contexto, uma avaliação de tipo válida deve satisfazer . Para esse tipo de avaliação, não há avaliação de termo válida. $\xi(\beta) \in \nu(\Pi \alpha:*.*) = \{f| f:\text{SAT} \to \text{SAT}\}$

lo.logic type-theory lambda-calculus typed-lambda-calculus helmut
fonte

Metade das pessoas que lêem isso acham que é SAT. Você deve explicar o que é isso. Além disso, sua derivação parece um pouco estranha. A segunda linha não deve mencionar em sua conclusão, ela deve ler algo como , não deveria?

S A T

$SAT$

α

$\alpha$

[α : *] ⊢ * : ◻

$[\alpha : *] \vdash * : \Box$

187 Andrej Bauer #

Estou usando a notação de Herman Geuvers (que parece ser padrão nesse domínio). é o conjunto de todos os conjuntos saturados de expressões lambda. Para a segunda linha da minha derivação: É a regra de introdução para variáveis de um sistema de tipo puro. Essa regra diz onde é algum tipo.

SAT

$\text{SAT}$

\frac{Γ ⊢ T : s}{Γ, x : T ⊢ x : T}

$\frac{\Gamma \vdash T:s}{\Gamma,x:T\vdash x:T}$

s

$s$

Helmut

Eu entendo como você conseguiu a segunda linha, mas não é a premissa correta para a formação da terceira linha, é? Qual regra dá a terceira linha.

Andrej Bauer

A regra de formação de produtos do PTS diz cálculo das construções tem a regra . Isso me permite usar a primeira e a segunda linha para derivar a terceira.No entanto, tive um erro de digitação no meu post. na terceira linha tinha sido falta que acrescentei agora.

\frac{r (s_{1}, s_{2}, s_{3}; Γ ⊢ A : s_{1}; Γ, x : A ⊢ B : s_{2}}{Γ ⊢ (Π x : A . B) : s_{3}}

$\frac{r(s_1,s_2,s_3;\, \Gamma\vdash A:s_1;\: \Gamma,x:A\vdash B:s_2}{\Gamma\vdash (\Pi x:A.B): s_3}$

r (*, *, *)

$r(*,*,*)$

Helmut

A primeira linha não deveria ler ? Ou você misturou e algum lugar? A segunda linha não pode ser a segunda premissa da regra de formação de produtos, porque isso significa que você está tentando formar algo como vez de .

[] ⊢ * : *

$[] \vdash * : *$

*

$*$

◻

$\Box$

\prod α : * . α

$\prod \alpha : * . \alpha$

\prod α : * . *

$\prod \alpha : * . *$

21320 Andrej Bauer

Infelizmente, não tenho certeza de que existem mais recursos amigáveis para iniciantes do que a conta do Geuvers. Você pode tentar esta nota de Chris Casinghino, que apresenta várias provas com detalhes excruciantes.

Não sei se entendi a essência da sua confusão, mas acho que uma coisa importante a ser observada é o seguinte lema (Corolário 5.2.14), comprovado no texto clássico de Barendregt :

Γ ⊢ M : T \Rightarrow Γ ⊢ T : * or ◻

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

Isso significa que enquanto pode ser uma função complicada, se mantido, então deve ser um conjunto de termos . $[\![T]\!]_\xi$ $\Gamma \vdash M:T$ $[\![T]\!]_\xi$

Isso é insinuado no esquema (seção 3.1), onde somente se , o que está de acordo com nossa expectativa, de que a interpretação de um tipo deve ser um conjunto de termos, por exemplo, (de fato, !) $(\!|t|\!)_\sigma\in[\![T]\!]_\xi$ $\Gamma \vdash t:T :*$ ${\cal V}(*)\subseteq{\cal P}(\mathrm{Term})$ ${\cal V}(*)=\mathrm{SAT}$

É uma situação comum na teoria dos tipos que, embora apenas estejamos interessados no "tipo base" (aqui ), ainda precisamos definir semântica para coisas de tipos mais altos (daí a necessidade de introduzir ) As coisas funcionam no final, porque apenas o tipo que habita os tipos é (e , mas isso não é realmente importante). $*$ $\mathrm{SAT}^*$ $*$ $\square$

cody
fonte

Obrigada pelo esclarecimento. Isso resolve meu problema de não entender as funções usadas na prova de Geuver. Eu já suspeitava de ler e reler o artigo de Geuver, mas você deixou claro.

precisa

Compreendendo a prova de forte normalização do cálculo de construções

Respostas: