Intuicja kryjąca się za zagnieżdżoną pozytywnością i kontrprzykładami
Patrzę na zagnieżdżone warunki pozytywności dla typów indukcyjnych określone w podręczniku Coq . Po pierwsze, czy są jakieś inne odniesienia (niekoniecznie dla Coq, ale ogólnie w teoriach typów zależnych) dla zagnieżdżonych warunków pozytywności i jak powstają? Znalazłem starsze artykuły, takie jak Inductive Families and Coquand firmy Dybjer oraz Inductively Defined Types Paulin , ale uważam, że wspomina się w nich tylko o warunku ścisłej pozytywności, a nowsze artykuły, takie jak pCuIC i A Comprehensive Guide to CIC , również nie wspominają o zagnieżdżonej pozytywności.
Teraz próbuję uzyskać intuicyjne zrozumienie, dlaczego wymagana jest zagnieżdżona pozytywność. W istocie, zagnieżdżona pozytywność stwierdza, że podczas definiowania konstruktora C dla jakiegoś typu indukcyjnego$D$, jeśli typ argumentu do $C$ jest czymś w rodzaju $I ~ \vec{p} ~ \vec{t}$, następnie $D$ może pojawiać się wyłącznie pozytywnie w $\vec{p}$i tylko wtedy, gdy $I \neq D$. Rozumiem, że pozwalając$D$ na ujemnych pozycjach $\vec{p}$ w zasadzie pozwala na dowody $(D \to \bot) \to \bot$i przyzwalając $D$w innych pozytywnych pozycjach zasadniczo pozwala na eliminację podwójnej negacji (i niektórych niezgodności z impredykatywną propozycją). To, czego nie rozumiem, to:
Dlaczego nie mogę $D$ wyglądają ściśle pozytywnie w $\vec{p}$ Jeśli $I = D$(jako argument konstruktora lub typ zwracany)? Na przykład dla konstruktora$C$ typu indukcyjnego $D ~ (A: \textrm{Type}): \textrm{Type}$ (z $A$ jako jedyny parametr), dlaczego tak jest $C: D ~ (D ~ A) \to D ~ A$ niedozwolone?
EDYCJA: nie tylko jest to akceptowane w Agdzie 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ jest również akceptowana, co wydaje mi się podejrzane.
Dlaczego tak $D$w przeciwnym razie pojawiają się w parametrach ściśle pozytywnie $\vec{p}$, ale nie w indeksach $\vec{t}$?
Rozważmy na przykład (raczej głupiutki) konstruktor $C: (D =_{\textrm{Type}} D) \to D$ dla typu indukcyjnego $D: \textrm{Type}$, gdzie $=$ jest typowym typem równości.EDYCJA: Okazuje się, że nie jest to typ sprawdzania w Agdzie z powodów niezwiązanych z poziomem wszechświata, więc zamiast tego rozważ następujące, które Agda odrzuca z powodów pozytywnych:
data Box : (A : Set) → Set where box : (A : Set) → Box A data D : Set where C : Box D → D
To jest akceptowane przez Agda jeśli
A
jest natomiast parametrem, jak oczekiwano od zagnieżdżonych zasad pozytywny.
Jestem szczególnie zainteresowany znalezieniem przykładów, w których naruszenie zagnieżdżonych warunków pozytywności (szczególnie tych dwóch, które wymieniłem) powoduje niespójności i dowody $\bot$, co osobiście byłoby łatwiejsze do zrozumienia niż spory o monotonię.
Odpowiedzi
Oto przykład wykorzystania pozytywności indeksu do udowodnienia fałszu:
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)
Technicznie wykorzystuje również fakt, że rekurencja indukcyjna może tworzyć małe wszechświaty i że równość typów może być mniejsza niż ogólna równość zastosowana do wszechświata, ale poza tym nie są one tak naprawdę problematyczne dla mojej wiedzy (Coq i tak ma impredykatywną równość, ja uwierzyć). Możliwe, że można by również wyeliminować równoczesną definicję, ale przynajmniej nie jest to proste.
Edycja: zapytałem o twój pierwszy punktor. Wskazano mi, że w zasadzie nie ma nic specjalnego w typie zagnieżdżonym, który jest sam w sobie zagnieżdżony. W tym artykule pokazano, jak używać obcej translacji zagnieżdżonych typów na indeksowane typy o równoważnym rozmiarze. Kiedy to robisz, o ile zagnieżdżanie jest ściśle dodatnie, nietrudno jest zastosować tłumaczenie do ściśle indeksowanego typu dodatniego.
Lub, na przykład, przykładowe tłumaczenie, które mi pokazano, używa pliku zagnieżdżonego $ℕ$ parametr zamiast samozagnieżdżenia:
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
Gdzie dodałem t
konstruktora, aby coś faktycznie używać A
i D A
ma być równoważne D' A 0
. Myślę, że innym sposobem napisania tego byłoby:
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
Zasadniczo $ℕ$ to drzewo śledzące, ile gniazd potrzebnych jest do rozwinięcia.
Zamierzam częściowo odpowiedzieć na punkt 2 tutaj. Jeśli pozwolisz , aby typ indukcyjny pojawiał się nawet ściśle pozytywnie w indeksie innej indukcyjnej, a miałeś impredykatywną wartość Prop , możesz wyprowadzić niespójność z typu równości z typem, który występuje negatywnie, jak stwierdził Dan w komentarzach. Oto przykład w Coq, z typem indukcyjnym określonym jako aksjomaty.
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.
Nie jestem pewien, czy możesz zrobić to samo, mając tylko wszechświaty predykatywne bez uciekania się do sztuczek polimorfizmu wszechświata lub tym podobnych.