Eu me deparei com um desacordo confuso entre Agda e Coq que não está obviamente relacionado às distinções mais conhecidas entre suas teorias de tipos (por exemplo, (im) predicatividade, indução-recursão etc.).
Em particular, a seguinte definição é aceita pela Agda:
data Ty : Set0 -> Set0 where
c1 : Ty ℕ
c2 : Ty (Ty ℕ)
enquanto a definição equivalente de Coq é rejeitada porque a aparência de [Ty _] como um índice em si mesmo em c2 é considerada uma violação de estrita positividade.
Inductive Ty : Set -> Set :=
| c1 : Ty nat
| c2 : Ty (Ty nat).
De fato, este caso é quase literalmente um exemplo da Seção 14.1.2.1 de Coq'Art de violar uma estrita positividade:
Inductive T : Set -> Set := c : (T (T nat)).
Mas não vejo as razões dessa diferença entre as teorias de tipos. O exemplo clássico de provar False usando uma ocorrência negativa de um tipo em um argumento construtor é claro para mim, mas não consigo ver como alguém pode derivar uma contradição desse estilo de indexação (independentemente de argumentos construtores estritamente positivos).
Examinando a literatura, o trabalho inicial de Dybjer Inductive Families faz um comentário imediato sobre a solução de Paulin-Mohring no artigo do CID com restrições um pouco diferentes e sugere vagamente que as diferenças podem estar relacionadas à impredicatividade, mas não é mais elaborada. O artigo de Dybjer parece permitir isso, enquanto o de Paulin-Mohring o proíbe claramente.
Aparentemente, não sou o primeiro a perceber essa diferença de opinião, e alguns acreditam que essa definição não deve ser permitida em nenhum dos sistemas ( https://lists.chalmers.se/pipermail/agda/2012/004249.html ), mas Não encontrei explicações sobre por que isso é válido em um sistema, mas não no outro, ou apenas uma diferença de opinião.
Então, suponho que tenho várias perguntas:
- Este é um exemplo de um tipo monótono, mas não estritamente positivo? (Na Coq; claramente a Agda considera estritamente positivo)
- Por que a Agda permite isso, enquanto a Coq o rejeita? É simplesmente uma diferença idiossincrática na interpretação de "estritamente positivo"; existe uma diferença sutil entre Coq e Agda que faz soar em Agda e não ser sólido em Coq, ou é uma questão de gosto impulsionada por preferências teóricas específicas?
- Existe uma diferença significativa entre a primeira definição acima e a definição indutiva-recursiva equivalente abaixo?
Definição indutivo-recursiva:
mutual
data U : Set0 -> Set0 where
c : (i : Fin 2) -> U (T i)
T : Fin 2 -> Set0
T zero = ℕ
T (suc zero) = U ℕ
Estou feliz por ter indicações para a literatura relevante.
Desde já, obrigado.
fonte
Ty is not strictly positive, because it occurs in an index of the target type of the constructor c2 in the definition of Ty.
Respostas:
A questão parece ser confusão resultante de uma confluência de dois fatores:
É claro que essa leitura mais próxima é consistente com a verificação que a Coq e (versões recentes) da Agda executam, que proíbem qualquer aparência de T em seus próprios índices.
fonte
Uma possível razão para a diferença, como sugerem seus próprios comentários, é a impredicatividade. Coq historicamente tinha um conjunto impredicativo (ainda disponível como uma bandeira, acredito!)
Citando o livro de Adam Chlipala http://adam.chlipala.net/cpdt/html/Universes.html
fonte