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 .
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 ϕ ( α )ϕ ( α → ⊥ )
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.
fonte