Intuicja kryjąca się za zagnieżdżoną pozytywnością i kontrprzykładami

Jan 04 2021

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 Ajest 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

1 DanDoel Jan 07 2021 at 02:15

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 tkonstruktora, aby coś faktycznie używać Ai D Ama 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.

ionathanch Jan 07 2021 at 02:18

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.