Intuição por trás da positividade aninhada e contra-exemplos
Estou olhando para as condições de positividade aninhadas para tipos indutivos declaradas no manual do Coq . Em primeiro lugar, existem outras referências (não necessariamente para Coq, mas em teorias de tipo dependente em geral) para as condições de positividade aninhadas e como elas surgem? Encontrei artigos mais antigos como Inductive Families and Coquand, de Dybjer, e Inductively Defined Types , de Paulin , mas acredito que eles mencionam apenas a condição de positividade estrita, e artigos mais recentes como o pCuIC e A Comprehensible Guide to CIC também não mencionam positividade aninhada.
Agora, estou tentando obter uma compreensão intuitiva de por que a positividade aninhada é necessária. Em essência, a positividade aninhada afirma que ao definir um construtor C para algum tipo indutivo$D$, se o tipo de um argumento para $C$ é algo como $I ~ \vec{p} ~ \vec{t}$, então $D$ só pode aparecer estritamente positivamente em $\vec{p}$, e somente se $I \neq D$. Eu entendo que permitir$D$ em posições negativas de $\vec{p}$ basicamente permite provas de $(D \to \bot) \to \bot$, e permitindo $D$em outras posições positivas, essencialmente permite a eliminação de negação dupla (e algumas coisas de inconsistência com Prop impredicativo). O que eu não entendo são estes:
Porque não pode $D$ aparecem estritamente positivamente em $\vec{p}$ E se $I = D$(como argumento do construtor ou tipo de retorno)? Por exemplo, para um construtor$C$ de um tipo indutivo $D ~ (A: \textrm{Type}): \textrm{Type}$ (com $A$ como o único parâmetro), por que é $C: D ~ (D ~ A) \to D ~ A$ não permitido?
EDITAR: Isso não é apenas aceito na Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ também é aceito, o que me parece suspeito.
Por que pode $D$caso contrário, aparecem estritamente positivamente nos parâmetros $\vec{p}$, mas não nos índices $\vec{t}$?
Considere, por exemplo, o (bastante bobo) construtor $C: (D =_{\textrm{Type}} D) \to D$ para o tipo indutivo $D: \textrm{Type}$, Onde $=$ é o tipo de igualdade usual.EDIT: Acontece que isso não digita a verificação em Agda por razões de nível de universo não relacionadas, então considere o seguinte que Agda rejeita por razões de positividade:
data Box : (A : Set) → Set where box : (A : Set) → Box A data D : Set where C : Box D → DIsso é aceito pela Agda se, em
Avez disso, for um parâmetro, conforme esperado das regras de positividade aninhadas.
Estou particularmente interessado em encontrar exemplos em que violar as condições de positividade aninhadas (especificamente essas duas que listei) causa inconsistências e provas de $\bot$, o que pessoalmente seria mais fácil de entender do que argumentos sobre a monotonicidade.
Respostas
Aqui está um exemplo que explora a positividade de um índice para provar que é falso:
module Whatever where
open import Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Data.Empty
variable
ℓ : Level
A B : Set ℓ
data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where
trefl : A ≅ A
Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B
Subst P trefl PA = PA
data U : Set where
d : U
El : U → Set
data D : Set
El d = D
{-# NO_POSITIVITY_CHECK #-}
data D where
neg : ∀(c : U) → El c ≅ D → (El c → ⊥) → D
¬D : D → ⊥
¬D v@(neg c eq f) = Subst (λ D → D → ⊥) eq f v
spin : ⊥
spin = ¬D (neg d trefl ¬D)
Tecnicamente, também faz uso do fato de que a indução-recursão pode criar pequenos universos, e que a igualdade de tipo pode ser menor do que a igualdade geral aplicada ao universo, mas isso não é realmente problemático para o meu conhecimento (Coq tem igualdade impredicativa de qualquer maneira, I acreditam). É possível que a definição simultânea também possa ser eliminada, mas não é direto, pelo menos.
Edit: Eu perguntei sobre seu primeiro ponto de bala. Foi apontado para mim que não há essencialmente nada de especial sobre um tipo aninhado que é aninhado em si mesmo. Este artigo mostra como usar uma tradução não nativa de tipos aninhados em tipos indexados de tamanho equivalente. Ao fazer isso, contanto que o aninhamento seja estritamente positivo, não é difícil aplicar a tradução a um tipo indexado estritamente positivo.
Ou, por exemplo, a tradução de exemplo que me foi mostrada usa um aninhado $ℕ$ parâmetro em vez de autoaninhamento:
data D' (A : Set) (n : ℕ) : Set where
c : D' A (suc n) → D' A n
t : (case n of λ where
zero → A
(suc m) → D' A m
) → D' A n
Onde eu adicionei o tconstrutor para fazer algo realmente usar Ae D Adeve ser equivalente a D' A 0. Acho que outra maneira de escrever isso seria:
data D' (A : Set) : ℕ → Set where
c : D' A (suc n) → D' A n
t : D' A n → D' A (suc n)
t' : A → D' A zero
Essencialmente, o $ℕ$ é uma árvore rastreando quanto aninhamento precisamos desdobrar.
Vou responder parcialmente ao ponto 2 aqui. Se você permitiu que o tipo indutivo para aparecer mesmo estritamente positivamente no índice do outro indutivo, e você tinha impredicativa Prop , você pode derivar uma inconsistência através de um tipo de igualdade com um tipo que não ocorrem de forma negativa, como Dan afirmou nos comentários. Aqui está um exemplo em Coq, com o tipo indutivo declarado como axiomas.
Inductive Equal (A: Prop) : Prop -> Prop :=
| refl : Equal A A.
(** These axioms correspond to the following inductive definition:
* Inductive D : Prop :=
* | C : forall (E: Prop) (p: Equal D E), (E -> False) -> D. *)
Axiom D : Prop.
Axiom introD: forall (E: Prop) (p: Equal D E), (E -> False) -> D.
Axiom matchD: forall (E: Prop) (p: Equal D E), D -> (E -> False).
Definition DnotD (d: D): (D -> False) := matchD D (refl D) d.
Definition notD (d: D): False := (DnotD d) d.
Definition isD: D := introD D (refl D) notD.
Definition bottom: False := notD isD.
Não tenho certeza se você pode fazer o mesmo quando você só tem universos predicativos, sem recorrer a truques de polimorfismo de universo ou semelhantes.