Erro de digitação no cálculo de papel de construção?

No clássico, o cálculo de papel de construção existe uma regra que declara

(página 7 do pdf, página 101 do documento original)

Esta regra significaria que qualquer contexto é redutível a um membro desse contexto. Parece que não deveria estar correto, pois isso implicaria

1 ≅ Nat
3 ≅ Nat
1 ≅ 3

se Nat é um contexto.

Penso que a melhor interpretação é que o delta inferior deveria ser um M. Especialmente considerando as regras fornecidas na próxima página.

Então isso é simplesmente um erro de digitação ou alguma regra lógica sutil que eu não entendo?

lo.logic calculus-of-constructions sequent-calculus user833970
fonte

Respostas:

\frac{Γ ⊢ M : Δ}{Γ ⊢ M ≅ M}

$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M}$

$\Gamma\vdash N\cong M$

De certa forma contra-intuitivo, provar que o sistema com conversão de tipos é equivalente ao sistema sem tipos é muito difícil e foi resolvido em 2010 por Siles e Herbelin .

cody
fonte

"Tratamentos modernos" aqui significa "tratamentos de ciência da computação que estão mais interessados em computação".

Andrej Bauer

Justo. Eu quase criei escolas "suecas" versus "francesas" da teoria dos tipos, mas não tenho certeza de que exista alguma distinção.

Cody

Não existe tal distinção, como testemunha o fato de Thierry Coquand viver na Suécia. Eles são todos computacionais.

Andrej Bauer

@ody: Eu pensei que praticamente todos os tratamentos modernos de ciência da computação usam julgamentos digitados, porque é a maneira mais conveniente de obter o eta para pi / sigma. (Certamente Coq e Agda apoio que.)

Neel Krishnaswami

@NeelKrishnaswami A conversão digitada é necessária para que o eta faça sentido na maioria das situações, mas fiquei com a impressão de que isso poderia tornar a meta-teoria consideravelmente mais complicada. Talvez eu esteja completamente errado e isso realmente torne tudo simples. Há também a questão de otimizar a verificação de conversão para realizar a menor quantidade de trabalho, incluindo obrigações extras de verificação de tipo. Certamente, essa seria uma ótima pergunta de acompanhamento.

07716