Intuizione dietro positività annidata e controesempi

Jan 04 2021

Sto osservando le condizioni di positività annidate per i tipi induttivi dichiarati nel manuale Coq . Prima di tutto, ci sono altri riferimenti (non necessariamente per Coq, ma in generale nelle teorie dei tipi dipendenti) per le condizioni di positività annidate e come si verificano? Ho trovato documenti più vecchi come Inductive Families e Coquand di Dybjer e Inductively Defined Types di Paulin , ma credo che questi menzionino solo la condizione di positività rigorosa, e documenti più recenti come quello pCuIC e A Comprehensible Guide to CIC non menzionano nemmeno la positività annidata.

Ora, sto cercando di ottenere una comprensione intuitiva del motivo per cui è necessaria la positività annidata. In sostanza, la positività annidata lo afferma quando si definisce un costruttore C per un tipo induttivo$D$, se il tipo di un argomento a $C$ è qualcosa di simile $I ~ \vec{p} ~ \vec{t}$, poi $D$ può apparire solo in modo rigorosamente positivo in $\vec{p}$e solo se $I \neq D$. Lo capisco permettendo$D$ in posizioni negative di $\vec{p}$ fondamentalmente consente prove di $(D \to \bot) \to \bot$e permettendo $D$in altre posizioni positive consente essenzialmente l'eliminazione della doppia negazione (e alcune cose incoerenti con Prop impredicative). Quello che non capisco sono questi:

Perché non posso $D$ apparire rigorosamente positivamente in $\vec{p}$ Se $I = D$(come argomento del costruttore o tipo restituito)? Ad esempio, per un costruttore$C$ di tipo induttivo $D ~ (A: \textrm{Type}): \textrm{Type}$ (con $A$ come unico parametro), perché lo è $C: D ~ (D ~ A) \to D ~ A$ non consentito?

EDIT: non solo questo è accettato in Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ è anche accettato, il che mi sembra sospetto.
Perchè puoi $D$altrimenti appaiono rigorosamente positivamente nei parametri $\vec{p}$, ma non negli indici $\vec{t}$? ~~Considera ad esempio il costruttore (piuttosto stupido) $C: (D =_{\textrm{Type}} D) \to D$ per il tipo induttivo $D: \textrm{Type}$, dove $=$ è il solito tipo di uguaglianza.~~

EDIT: Si scopre che questo non digita il controllo in Agda per motivi a livello di universo non correlati, quindi considera invece quanto segue che Agda rifiuta per motivi di positività:
```
data Box : (A : Set) → Set where
  box : (A : Set) → Box A

data D : Set where
  C : Box D → D
```
Questo è accettato da Agda se Aè invece un parametro, come previsto dalle regole di positività annidate.

Sono particolarmente interessato a trovare esempi in cui la violazione delle condizioni di positività annidate (in particolare queste due che ho elencato) causa incongruenze e prove di $\bot$, che personalmente sarebbe più facile da capire rispetto agli argomenti sulla monotonia.

Risposte

1 DanDoel Jan 07 2021 at 02:15

Ecco un esempio che sfrutta la positività di un indice per dimostrare 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 fa anche uso del fatto che l'induzione-ricorsione può creare piccoli universi e che l'uguaglianza di tipo può essere più piccola dell'uguaglianza generale applicata all'universo, ma per il resto non sono realmente problematiche per la mia conoscenza (Coq ha uguaglianza impredicativa comunque, io credere). È possibile che anche la definizione simultanea venga eliminata, ma almeno non è semplice.

Modifica: ho chiesto in giro del tuo primo punto elenco. Mi è stato fatto notare che essenzialmente non c'è niente di speciale in un tipo annidato che è annidato in se stesso. In questo articolo viene illustrato come utilizzare una conversione non nativa di tipi annidati in tipi indicizzati di dimensioni equivalenti. Quando lo fai, fintanto che l'annidamento è strettamente positivo, non è difficile applicare la traduzione a un tipo indicizzato strettamente positivo.

O per esempio, la traduzione di esempio che mi è stata mostrata usa un file annidato $ℕ$ parametro invece di auto-annidamento:

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

Dove ho aggiunto il tcostruttore per fare qualcosa di effettivamente utilizzato A, e D Adovrebbe essere equivalente a D' A 0. Penso che un altro modo per scrivere questo sarebbe:

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

In sostanza, il $ℕ$ è un albero che tiene traccia di quanto annidamento abbiamo bisogno di dispiegare.

ionathanch Jan 07 2021 at 02:18

Risponderò parzialmente al punto 2 qui. Se permettessi al tipo induttivo di apparire anche strettamente positivamente nell'indice di un altro induttivo e avessi Prop impredicative , potresti derivare un'incongruenza attraverso un tipo di uguaglianza con un tipo che si verifica negativamente, come Dan ha dichiarato nei commenti. Ecco un esempio in Coq, con il tipo induttivo indicato come assiomi.