Como mostrar que um tipo em um sistema com tipos dependentes não é habitado (isto é, fórmula não comprovável)?

15

Para sistemas sem tipos dependentes, como o sistema de Hindley-Milner, os tipos correspondem a fórmulas da lógica intuicionista. Sabemos que seus modelos são álgebras de Heyting e, em particular, para refutar uma fórmula, podemos restringir a uma álgebra de Heyting em que cada fórmula é representada por um subconjunto aberto de .R

Por exemplo, se queremos mostrar que não é habitado, construímos um mapeamento partir de fórmulas para abrir subconjuntos de definindo: Em seguida, Isso mostra que a fórmula original não pode ser comprovada, pois temos um modelo em que não é verdadeira ou, de forma equivalente (pelo isomorfismo de Curry-Howard), o tipo não pode ser habitado.ϕ R ϕ ( α )α.α(α)ϕRϕ ( α )

ϕ(α)=(-,0 0)
ϕ(α)=int([0 0,))=(0 0,)ϕ(α(α))=(-,0 0)(0 0,)=R0 0.

Outra possibilidade seria usar os quadros Kriepke .


Existem métodos semelhantes para sistemas com tipos dependentes? Como alguma generalização de álgebras de Heyting ou molduras de Kripke?

Nota: não estou solicitando um procedimento de decisão, sei que não pode haver nenhum. Estou pedindo apenas um mecanismo que permita testemunhar a impossibilidade de uma fórmula - convencer alguém de que é impossível de provar.

Petr Pudlák
fonte

Respostas:

13

O fato de uma fórmula não ser comprovável pode ser essencialmente feito de duas maneiras. Com alguma sorte, poderemos mostrar, dentro da teoria dos tipos, que a fórmula implica uma que já é conhecida por não ser comprovável. A outra maneira é encontrar um modelo no qual a fórmula seja inválida, e isso pode ser bastante difícil. Por exemplo, demorou muito tempo para encontrar o modelo grupóide da teoria dos tipos dependentes, que foi o primeiro a invalidar a exclusividade das provas de identidade .

A pergunta "o que é um modelo de teoria dos tipos dependentes?" tem uma resposta um tanto complicada. Se você ignorar certas propriedades de substituição, um modelo é uma categoria fechada cartesiana localmente , e essa pode ser a resposta mais simples. Se você deseja um modelo "real", existem várias opções, consulte a página do nLab sobre modelos categóricos da teoria dos tipos dependentes . De qualquer forma, a resposta é sempre um pouco complicada porque a teoria do tipo dependente é um sistema formal bastante complexo.

Se eu sugerisse apenas um artigo sobre o assunto, provavelmente recomendaria o artigo original de Robert Seely, "Categorias fechadas localmente cartesianas e teoria dos tipos" . Se eu sugerisse outra, provavelmente seria aquela que explica o que precisa ser corrigido no artigo de Seely, por exemplo, "Sobre a interpretação da teoria dos tipos em categorias fechadas localmente cartesianas" , de Martin Hoffman .

Um recente avanço importante nessa área é a constatação de que os modelos teóricos da homotopia também são modelos da teoria dos tipos dependentes, consulte as referências homotopytypetheory.org . Isso oferece muitas possibilidades, mas é preciso agora aprender a teoria da homotopia para colocar as mãos nos modelos.

Andrej Bauer
fonte
2
Essa resposta é bastante agradável, embora ignore talvez a maneira mais simples possível de provar que um tipo não é habitado: indução em formas normais! Em particular, é fácil provar que o meio excluído não pode ser habitado no Cálculo de Construções por essa indução. Claro, então você precisa mostrar que cada termo pode ser colocado em uma forma normal do mesmo tipo, e que envolve uma construção modelo ...
Cody
@ codigo: bom ponto, formas normais podem ser muito úteis.
Andrej Bauer
@cody: "você precisa mostrar que todos os termos podem ser colocados em uma forma normal do mesmo tipo": não é uma parte padrão da metateoria para um sistema de tipo "bom" (desde que você não tem axiomas) ou uma lógica "boa" (onde isso é eliminação de cortes)? Então você pode reutilizar a prova existente, certo?
Blaisorblade 12/03
@ Blaisorblade: é claro que você só precisa provar a eliminação de cortes uma vez. Pode-se apontar que o uso de indução em formas normais, em vez de construções de modelos, era uma maneira de implantar a pergunta: você já está construindo um modelo para mostrar que todos os termos podem ser colocados na forma normal. Em certo sentido, você está trabalhando no "modelo de forma normal", em vez de realizar um trabalho estritamente sintático.
Cody
Entendo - eu estava pensando no "esforço de prova", enquanto acho que você está pensando sobre como toda a prova é implementada. Mas você me fez questionar mais uma vez a distinção entre abordagens sintática e semântica, dadas construções como modelos de termos. Então eu fiz uma pergunta separada sobre isso: cstheory.stackexchange.com/q/21534/989
Blaisorblade