Intuition hinter verschachtelter Positivität und Gegenbeispielen
Ich betrachte die verschachtelten Positivitätsbedingungen für induktive Typen, die im Coq-Handbuch angegeben sind . Gibt es zunächst andere Referenzen (nicht unbedingt für Coq, sondern allgemein für abhängige Typentheorien) für die verschachtelten Positivitätsbedingungen und wie sie entstehen? Ich habe ältere Artikel wie Dybjers Inductive Families und Coquand sowie Paulins Inductive Defined Types gefunden , aber ich glaube, diese erwähnen nur die strenge Positivitätsbedingung, und neuere Artikel wie der pCuIC One und A Comprehensible Guide to CIC erwähnen auch keine verschachtelte Positivität.
Jetzt versuche ich ein intuitives Verständnis dafür zu erlangen, warum verschachtelte Positivität erforderlich ist. Im Wesentlichen besagt die verschachtelte Positivität, dass beim Definieren eines Konstruktors C für einen induktiven Typ$D$, wenn der Typ eines Arguments zu $C$ ist so etwas wie $I ~ \vec{p} ~ \vec{t}$, dann $D$ kann nur streng positiv in erscheinen $\vec{p}$und nur wenn $I \neq D$. Ich verstehe das erlauben$D$ in negativen Positionen von $\vec{p}$ erlaubt grundsätzlich Beweise von $(D \to \bot) \to \bot$und erlauben $D$in anderen positiven Positionen ermöglicht im Wesentlichen die Eliminierung der doppelten Negation (und einige inkonsistente Dinge mit improvisiertem Prop). Was ich nicht verstehe, sind diese:
Warum kann nicht $D$ erscheinen streng positiv in $\vec{p}$ wenn $I = D$(entweder als Konstruktorargument oder als Rückgabetyp)? Zum Beispiel für einen Konstruktor$C$ von einem induktiven Typ $D ~ (A: \textrm{Type}): \textrm{Type}$ (mit $A$ als einziger Parameter), warum ist $C: D ~ (D ~ A) \to D ~ A$ nicht erlaubt?
EDIT: Dies wird nicht nur in Agda 2.6.1.2 akzeptiert, $C: D ~ (D ~ A \to \bot) \to D ~ A$ wird auch akzeptiert, was mir verdächtig erscheint.
Warum können $D$ansonsten erscheinen die Parameter streng positiv $\vec{p}$, aber nicht in den Indizes $\vec{t}$?
Betrachten Sie zum Beispiel den (ziemlich dummen) Konstruktor $C: (D =_{\textrm{Type}} D) \to D$ für den induktiven Typ $D: \textrm{Type}$, wo $=$ ist der übliche Gleichheitstyp.BEARBEITEN: Es stellt sich heraus, dass dies aus Gründen, die nicht mit dem Universum zusammenhängen, keine Prüfung in Agda eingibt. Betrachten Sie stattdessen Folgendes, das Agda aus Gründen der Positivität ablehnt:
data Box : (A : Set) → Set where box : (A : Set) → Box A data D : Set where C : Box D → DDies wird von Agda akzeptiert, wenn
Aes sich stattdessen um einen Parameter handelt, wie dies von den verschachtelten Positivitätsregeln erwartet wird.
Ich bin besonders daran interessiert, Beispiele zu finden, bei denen die Verletzung verschachtelter Positivitätsbedingungen (insbesondere der beiden von mir aufgelisteten) zu Inkonsistenzen und Beweisen führt $\bot$, die persönlich leichter zu verstehen wären als Argumente über Monotonie.
Antworten
Hier ist ein Beispiel, bei dem die Positivität eines Index ausgenutzt wird, um sich als falsch zu erweisen:
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)
Technisch wird auch die Tatsache genutzt, dass Induktionsrekursion kleine Universen erzeugen kann und dass die Typgleichheit kleiner sein kann als die allgemeine Gleichheit, die auf das Universum angewendet wird, aber diese sind meines Wissens ansonsten nicht wirklich problematisch (Coq hat ohnehin eine improvisierte Gleichheit, ich glauben). Es ist möglich, dass die gleichzeitige Definition ebenfalls beseitigt wird, aber es ist zumindest nicht einfach.
Bearbeiten: Ich habe nach Ihrem ersten Aufzählungspunkt gefragt. Ich wurde darauf hingewiesen, dass ein verschachtelter Typ, der in sich selbst verschachtelt ist, im Wesentlichen nichts Besonderes ist. Dieser Artikel zeigt, wie eine nicht native Übersetzung verschachtelter Typen in indizierte Typen gleicher Größe verwendet wird. Wenn Sie dies tun, ist es nicht schwierig, die Übersetzung auf einen streng positiv indizierten Typ anzuwenden, solange die Verschachtelung streng positiv ist.
Oder die Beispielübersetzung, die mir gezeigt wurde, verwendet eine verschachtelte $ℕ$ Parameter statt Selbstverschachtelung:
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
Wo ich den tKonstruktor hinzugefügt habe , um etwas tatsächlich zu verwenden A, und D Adas äquivalent zu sein soll D' A 0. Ich denke, eine andere Art, dies zu schreiben, wäre:
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
Im Wesentlichen die $ℕ$ ist ein Baum, der verfolgt, wie viel Verschachtelung wir zum Entfalten benötigen.
Ich werde hier Punkt 2 teilweise beantworten. Wenn Sie zulassen, dass der induktive Typ im Index eines anderen induktiven Typs sogar streng positiv erscheint, und Sie einen Impredikativ-Prop hatten , können Sie eine Inkonsistenz durch einen Gleichheitstyp mit einem Typ ableiten, der negativ auftritt, wie Dan in den Kommentaren angegeben hat. Hier ist ein Beispiel in Coq, wobei der induktive Typ als Axiome angegeben ist.
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.
Ich bin mir nicht sicher, ob Sie dasselbe tun können, wenn Sie nur prädikative Universen haben, ohne auf Tricks des Universumspolymorphismus oder dergleichen zurückzugreifen.