Intuisi di balik kepositifan dan contoh tandingan

Question

Saya melihat kondisi positif bersarang untuk jenis induktif yang dinyatakan dalam manual Coq . Pertama, apakah ada referensi lain (tidak harus untuk Coq, tetapi dalam teori tipe dependen secara umum) untuk kondisi kepositifan bersarang dan bagaimana hal itu terjadi? Saya telah menemukan makalah lama seperti Keluarga Induktif Dybjer dan Coquand serta Jenis yang Ditentukan Secara Induktif Paulin , tetapi saya percaya ini hanya menyebutkan kondisi kepositifan yang ketat, dan makalah yang lebih baru seperti pCuIC dan Panduan yang Dapat Dipahami untuk CIC juga tidak menyebutkan kepositifan bersarang.

Sekarang, saya mencoba untuk mendapatkan pemahaman intuitif tentang mengapa kepositifan bersarang diperlukan. Intinya, kepositifan bersarang menyatakan bahwa ketika mendefinisikan konstruktor C untuk beberapa tipe induktif$D$, jika jenis argumen untuk $C$ adalah sesuatu seperti $I ~ \vec{p} ~ \vec{t}$, kemudian $D$ hanya dapat terlihat sangat positif dalam $\vec{p}$, dan hanya jika $I \neq D$. Saya mengerti bahwa mengizinkan$D$ dalam posisi negatif dari $\vec{p}$ pada dasarnya memungkinkan untuk bukti $(D \to \bot) \to \bot$, dan memungkinkan $D$di posisi positif lainnya pada dasarnya memungkinkan untuk eliminasi negasi ganda (dan beberapa hal yang tidak konsisten dengan Prop impredikatif). Yang tidak saya mengerti adalah ini:

• Kenapa tidak bisa $D$ tampil sangat positif dalam $\vec{p}$ jika $I = D$(baik sebagai argumen konstruktor atau tipe kembalian)? Misalnya, untuk konstruktor$C$ dari tipe induktif $D ~ (A: \textrm{Type}): \textrm{Type}$ (dengan $A$ sebagai parameter tunggal), mengapa $C: D ~ (D ~ A) \to D ~ A$ tidak diizinkan?

  EDIT: Ini tidak hanya diterima di Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ juga diterima, yang tampaknya mencurigakan bagi saya.

• Kenapa bisa $D$jika tidak, tampil sangat positif dalam parameter $\vec{p}$, tapi tidak di indeks $\vec{t}$? Pertimbangkan misalnya konstruktor (agak konyol) $C: (D =_{\textrm{Type}} D) \to D$ untuk tipe induktif $D: \textrm{Type}$, dimana $=$ adalah jenis persamaan yang biasa.

  EDIT: Ternyata ini tidak mengetik cek di Agda untuk alasan tingkat alam semesta yang tidak terkait, jadi pertimbangkan hal berikut yang ditolak Agda karena alasan positif:

  data Box : (A : Set) → Set where
    box : (A : Set) → Box A
  
  data D : Set where
    C : Box D → D
  

  Ini adalah diterima oleh Agda jika Aadalah bukan parameter, seperti yang diharapkan dari aturan positif bersarang.

Saya sangat tertarik untuk menemukan contoh di mana melanggar kondisi kepositifan bersarang (khususnya dua yang telah saya sebutkan) menyebabkan ketidakkonsistenan dan bukti dari $\bot$, yang secara pribadi lebih mudah dipahami daripada argumen tentang monotonisitas.

Answer 1

Berikut adalah contoh mengeksploitasi kepositifan indeks untuk membuktikan salah:

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)

Secara teknis itu juga memanfaatkan fakta bahwa induksi-rekursi dapat menciptakan alam semesta kecil, dan persamaan jenis itu bisa lebih kecil dari persamaan umum yang diterapkan pada alam semesta, tetapi itu tidak benar-benar bermasalah bagi pengetahuan saya (Coq memiliki persamaan impredikatif pula, saya percaya). Mungkin saja definisi simultan bisa dihilangkan juga, tapi itu tidak langsung, setidaknya.

---

Edit: Saya bertanya tentang poin pertama Anda. Telah ditunjukkan kepada saya bahwa pada dasarnya tidak ada yang istimewa tentang tipe bersarang yang bertingkat itu sendiri. Artikel ini menunjukkan cara menggunakan terjemahan non-native dari tipe bertingkat menjadi tipe terindeks dengan ukuran setara. Saat Anda melakukannya, selama penumpukan benar-benar positif, tidak sulit untuk menerapkan terjemahan ke jenis indeks yang sangat positif.

Atau misalnya, terjemahan contoh yang saya tunjukkan menggunakan file bersarang $ℕ$ parameter alih-alih bertumpuk sendiri:

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

Di mana saya menambahkan tkonstruktor untuk membuat sesuatu benar-benar digunakan A, dan D Adimaksudkan untuk setara dengan D' A 0. Saya pikir cara lain untuk menulis ini adalah:

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

Pada dasarnya, file $ℕ$ adalah pohon yang melacak seberapa banyak sarang yang perlu kita buka.

Answer 2

Saya akan menjawab sebagian poin 2 di sini. Jika Anda membiarkan tipe induktif muncul bahkan ketat positif dalam indeks lain induktif ini, dan Anda memiliki impredicative Prop , Anda bisa memperoleh inkonsistensi melalui tipe kesetaraan dengan jenis yang tidak terjadi secara negatif, sebagai Dan dinyatakan dalam komentar. Berikut adalah contoh di Coq, dengan tipe induktif dinyatakan sebagai aksioma.

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.

Saya tidak yakin apakah Anda dapat melakukan hal yang sama jika Anda hanya memiliki alam semesta predikatif tanpa menggunakan trik polimorfisme alam semesta atau sejenisnya.