Por que tipos codificados pela Igreja não são suficientes para expressar provas indutivas?

Respostas:

5

Como você provaria dentro do CoC puro que o princípio de indução contém os numerais da Igreja? Veja Thomas Streicher, Independência do princípio da indução e o axioma da escolha no cálculo puro das construções .

Martin Berger
fonte
11
Herman Geuvers também provou ( aqui ) que nenhuma codificação possível dos números naturais pode funcionar.
Cody
O resultado do @cody Geuvers é para tipos dependentes de segunda ordem. É óbvio que generaliza para tipos dependentes de ordem superior?
Martin Berger
11
Não é óbvio, não. Eu acho que a construção do modelo descrita no artigo generaliza, pois é baseada em um modelo originalmente desenvolvido para o cálculo completo.
Cody
1

Há um resultado publicado recentemente em Annals of Pure and Applic Logic, no qual os dados codificados da igreja são realizadores de seu próprio princípio de indução. Neste sistema, o princípio de indução para números naturais, árvores, listas ... é derivável. O cálculo principal não possui nenhum construtor de tipo de dados empacotado. Inicia em um Sistema F extrínseco (estilo curry) adicionando três construções de digitação: produto implícito, igualdade heterogênea e interseção dependente.

O resultado das manobras não se aplica a este cálculo e é mencionado no artigo.

artigo: "Da realização à indução via interseção dependente" , de Aaron Stump

Eric Bond
fonte