L'intuition derrière la positivité imbriquée et les contre-exemples
Je regarde les conditions de positivité imbriquées pour les types inductifs indiqués dans le manuel Coq . Tout d'abord, existe-t-il d'autres références (pas nécessairement pour Coq, mais dans les théories des types dépendants en général) pour les conditions de positivité imbriquées et comment elles se produisent? J'ai trouvé des articles plus anciens comme Dybjer Inductive Families et Coquand and Paulin's Inductively Defined Types , mais je crois que ceux-ci ne mentionnent que la condition de positivité stricte, et les articles plus récents comme pCuIC one et A Comprehensible Guide to CIC ne mentionnent pas non plus la positivité imbriquée.
Maintenant, j'essaie d'acquérir une compréhension intuitive de la raison pour laquelle la positivité imbriquée est nécessaire. En substance, la positivité imbriquée indique que lors de la définition d'un constructeur C pour un type inductif$D$, si le type d'un argument à $C$ est quelque chose comme $I ~ \vec{p} ~ \vec{t}$, puis $D$ ne peut apparaître strictement positivement dans $\vec{p}$, et seulement si $I \neq D$. Je comprends que permettre$D$ en position négative de $\vec{p}$ permet essentiellement des preuves de $(D \to \bot) \to \bot$et permettant $D$dans d'autres positions positives permet essentiellement l'élimination de la double négation (et certaines incohérences avec Prop imprédicatif). Ce que je ne comprends pas, ce sont:
Pourquoi ne peut pas $D$ apparaissent strictement positivement dans $\vec{p}$ si $I = D$(soit en tant qu'argument constructeur ou type de retour)? Par exemple, pour un constructeur$C$ de type inductif $D ~ (A: \textrm{Type}): \textrm{Type}$ (avec $A$ comme seul paramètre), pourquoi $C: D ~ (D ~ A) \to D ~ A$ refusé?
EDIT: Non seulement cela est accepté dans Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ est également acceptée, ce qui me semble suspect.
Pourquoi peut $D$sinon apparaissent strictement positivement dans les paramètres $\vec{p}$, mais pas dans les indices $\vec{t}$?
Considérons par exemple le constructeur (plutôt idiot) $C: (D =_{\textrm{Type}} D) \to D$ pour le type inductif $D: \textrm{Type}$, où $=$ est le type d'égalité habituel.EDIT: Il s'avère que cela ne tape pas check dans Agda pour des raisons non liées au niveau de l'univers, alors considérez plutôt ce qui suit qu'Agda rejette pour des raisons de positivité:
data Box : (A : Set) → Set where box : (A : Set) → Box A data D : Set where C : Box D → DCeci est accepté par Agda s'il
As'agit plutôt d'un paramètre, comme prévu par les règles de positivité imbriquées.
Je suis particulièrement intéressé à trouver des exemples où la violation des conditions de positivité imbriquées (en particulier les deux que j'ai énumérées) provoque des incohérences et des preuves de $\bot$, ce qui serait personnellement plus facile à comprendre que les arguments sur la monotonie.
Réponses
Voici un exemple exploitant la positivité d'un index pour prouver faux:
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)
Techniquement, il utilise également le fait que l'induction-récursivité peut créer de petits univers, et que l'égalité de type peut être plus petite que l'égalité générale appliquée à l'univers, mais celles-ci ne sont pas vraiment problématiques à ma connaissance (Coq a de toute façon l'égalité imprédicative, je croyez). Il est possible que la définition simultanée soit également éliminée, mais ce n'est pas simple, du moins.
Edit: J'ai posé des questions sur votre premier point. On m'a fait remarquer qu'il n'y a essentiellement rien de spécial dans un type imbriqué qui est imbriqué en lui-même. Cet article montre comment utiliser une traduction non native de types imbriqués en types indexés de taille équivalente. Lorsque vous faites cela, tant que l'imbrication est strictement positive, il n'est pas difficile d'appliquer la traduction à un type indexé strictement positif.
Ou par exemple, l'exemple de traduction qui m'a été montré utilise un $ℕ$ paramètre au lieu de l'auto-imbrication:
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
Où j'ai ajouté le tconstructeur pour que quelque chose utilise réellement A, et D Aest censé être équivalent à D' A 0. Je pense qu'une autre façon d'écrire cela serait:
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
Essentiellement, le $ℕ$ est un arbre qui suit la quantité de nidification que nous devons déplier.
Je vais répondre en partie au point 2 ici. Si vous avez autorisé le type inductif apparaisse même strictement positive dans l'index d' une autre induction, et vous aviez imprédicative Prop , vous pouvez déduire une incohérence par un type d'égalité avec un type qui ne se produit négativement, comme Dan a déclaré dans les commentaires. Voici un exemple en Coq, avec le type inductif indiqué comme axiomes.
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.
Je ne sais pas si vous pouvez faire la même chose lorsque vous n'avez que des univers prédicatifs sans recourir à des astuces de polymorphisme d'univers ou similaires.