A maioria dos sistemas tipificados dependentes possui condições estritas de positividade para tipos indutivos. Alguém conhece um exemplo em que a violação da condição leva à inconsistência no sistema?
fonte
A maioria dos sistemas tipificados dependentes possui condições estritas de positividade para tipos indutivos. Alguém conhece um exemplo em que a violação da condição leva à inconsistência no sistema?
Na verdade, é possível relaxar uma estrita positividade e permanecer consistente. Por exemplo, basta ter apenas uma condição de positividade. Ou seja, podemos aceitar definições de tipo como
onde variáveis de tipo recursivo ocorrem à esquerda de um número par de setas e mantêm a consistência.
No entanto, as teorias que permitem esse tipo de tipo indutivo não possuem modelos teóricos dos conjuntos - você não pode interpretar tipos como conjuntos e termos como elementos de conjuntos. Nesse caso, estamos dizendo que é isomórfico ao seu conjunto de dupla potência (isto é, ), e isso viola o teorema de Cantor .
Como as teorias de tipos dependentes são frequentemente usadas para formalizar a matemática, seus projetistas geralmente hesitam em adicionar princípios que não são compatíveis com uma semântica da teoria dos conjuntos, mesmo que sejam consistentes.
EDIT: Estou adicionando esta edição em resposta à pergunta de Andrej. O tipo é consistente se você o adicionar a (digamos) Agda; não há problemas com isso. Só temos um problema se combinarmos positividade não estrita com meio excluído.
A intuição do porquê é seguro é (IMO) mais bem vista através das lentes da parametridade. No Sistema F, podemos mostrar usando a parametridade que, para qualquer função definível , o tipo é realmente um tipo indutivo.
Agora, lembre-se de que um functor definível é um operador de tipo , junto com um operador satisfazendo as condições de funcionalidade (por exemplo, e ).
Agora, podemos definir um operador de tipo para o conjunto de energia duplo
e como ocorre apenas positivamente, também podemos definir um operador de mapa para ele:
Portanto, sabemos que é um tipo indutivo legítimo.