नेस्टेड सकारात्मकता और प्रतिकार के पीछे अंतर्ज्ञान

Question

मैं Coq मैनुअल में बताए गए आगमनात्मक प्रकारों के लिए नेस्टेड सकारात्मकता स्थितियों को देख रहा हूं । सबसे पहले, नेस्ट पॉजिटिविटी स्थितियों के लिए कोई अन्य संदर्भ (जरूरी नहीं कि कोक के लिए, लेकिन निर्भर प्रकार के सिद्धांतों में आम तौर पर) हैं और वे कैसे आते हैं? मुझे डाइबज़र इंडक्टिव फैमिलीज एंड कोक्वैंड और पॉलिन के इंडक्टिवली डिफाइंड टाइप्स जैसे पुराने पेपर मिल गए हैं , लेकिन मेरा मानना ​​है कि ये केवल सख्त सकारात्मकता की स्थिति का उल्लेख करते हैं, और नए कागजात जैसे कि PCuIC एक और A Comprehensens Guide to CIC जैसे नेस्टेड पॉजिटिविटी का भी उल्लेख नहीं करते।

अब, मैं नेस्टेड सकारात्मकता की आवश्यकता क्यों है की एक सहज समझ हासिल करने की कोशिश कर रहा हूं। संक्षेप में, नेस्टेड सकारात्मकता बताती है कि कुछ प्रेरक प्रकार के लिए एक कंस्ट्रक्टर सी को परिभाषित करते समय$D$, यदि तर्क का प्रकार $C$ कुछ ऐसा है $I ~ \vec{p} ~ \vec{t}$, तब फिर $D$ केवल सख्ती से सकारात्मक रूप से प्रकट हो सकते हैं $\vec{p}$, और केवल अगर $I \neq D$। मैं समझता हूँ कि अनुमति$D$ के नकारात्मक पदों में $\vec{p}$ मूल रूप से के सबूत के लिए अनुमति देता है $(D \to \bot) \to \bot$, और अनुमति $D$अन्य सकारात्मक स्थितियों में अनिवार्य रूप से दोहरे निषेध उन्मूलन (और कुछ अप्रभावी प्रोप के साथ कुछ असंगतता) के लिए अनुमति देता है। मुझे समझ में नहीं आता ये क्या हैं:

• क्यों नहीं कर सकते $D$ में सख्ती से सकारात्मक दिखाई देते हैं $\vec{p}$ अगर $I = D$(या तो निर्माता तर्क या वापसी प्रकार)? उदाहरण के लिए, एक कंस्ट्रक्टर के लिए$C$ एक आगमनात्मक प्रकार का $D ~ (A: \textrm{Type}): \textrm{Type}$ (साथ से $A$ एकमात्र पैरामीटर के रूप में), क्यों है $C: D ~ (D ~ A) \to D ~ A$ अस्वीकृत

  संपादित करें: यह न केवल Agda 2.6.1.2 में स्वीकार किया जाता है, $C: D ~ (D ~ A \to \bot) \to D ~ A$ भी स्वीकार किया जाता है, जो मुझे संदेहास्पद लगता है।

• क्यों नहीं $D$अन्यथा मापदंडों में सख्ती से सकारात्मक रूप से दिखाई देते हैं $\vec{p}$, लेकिन सूचकांकों में नहीं $\vec{t}$? उदाहरण के लिए (बल्कि मूर्खतापूर्ण) कंस्ट्रक्टर पर विचार करें $C: (D =_{\textrm{Type}} D) \to D$ आगमनात्मक प्रकार के लिए $D: \textrm{Type}$, कहां है $=$ सामान्य समानता प्रकार है।

  संपादित करें: यह पता चला है कि यह असंबंधित ब्रह्मांड स्तर के कारणों के लिए Agda में चेक टाइप नहीं करता है, इसलिए निम्नलिखित पर विचार करें जो Agda सकारात्मक कारणों के लिए अस्वीकार करता है:

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

  यह है AGDA द्वारा स्वीकार कर लिया है, तो A, बजाय एक पैरामीटर है नेस्टेड सकारात्मकता नियमों से अपेक्षा के अनुरूप।

मैं उन उदाहरणों को खोजने में विशेष रूप से रुचि रखता हूं जहां नेस्टेड पॉज़िटिविटी स्थितियों का उल्लंघन हो रहा है (विशेष रूप से इन दोनों को मैंने सूचीबद्ध किया है) असंगति और प्रमाण का कारण बनता है $\bot$, जो व्यक्तिगत रूप से एकरसता के बारे में तर्कों की तुलना में समझना आसान होगा।

Answer 1

यहाँ एक उदाहरण है कि गलत साबित करने के लिए एक सूचकांक की सकारात्मकता का शोषण किया जाता है:

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)

तकनीकी रूप से यह इस तथ्य का भी उपयोग करता है कि प्रेरण-पुनरावृत्ति छोटे ब्रह्मांडों का निर्माण कर सकती है, और उस प्रकार की समानता ब्रह्मांड पर लागू सामान्य समानता से छोटी हो सकती है, लेकिन वे वास्तव में मेरे ज्ञान के लिए समस्याग्रस्त नहीं हैं (Coq के पास वैसे भी समतावादी समानता है, मैं विश्वास करते हैं)। यह संभव है कि एक साथ परिभाषा को समाप्त किया जा सकता है, भी, लेकिन यह सीधे आगे नहीं है, कम से कम।

---

संपादित करें: मैंने आपके पहले बुलेट पॉइंट के बारे में पूछा। यह मेरे लिए इंगित किया गया था कि अनिवार्य रूप से एक नेस्टेड प्रकार के बारे में कुछ खास नहीं है जो अपने आप में नेस्टेड है। यह लेख दर्शाता है कि कैसे नस्टेड प्रकारों के गैर-देशी अनुवाद को अनुक्रमित प्रकार के समकक्ष आकार में उपयोग किया जाए। जब आप ऐसा करते हैं, तब तक जब तक नेस्टिंग सख्ती से सकारात्मक है, तब तक अनुवाद को सख्ती से सकारात्मक अनुक्रमित प्रकार में लागू करना मुश्किल नहीं है।

या उदाहरण के लिए, उदाहरण मैं दिखाया गया था एक नेस्टेड का उपयोग करता है $ℕ$ स्व-नेस्टिंग के बजाय पैरामीटर:

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

जहाँ मैंने tकुछ वास्तव में उपयोग करने के लिए कंस्ट्रक्टर को जोड़ा A, और D Aइसका अर्थ बराबर होना चाहिए D' A 0। मुझे लगता है कि इसे लिखने का एक और तरीका होगा:

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

अनिवार्य रूप से, $ℕ$ एक पेड़ पर नज़र रखना है कि हमें कितना घोंसला बनाना है।

Answer 2

मैं यहाँ आंशिक रूप से उत्तर 2 बिंदु पर जा रहा हूँ। यदि आपने आगमनात्मक प्रकार को दूसरे प्रेरक सूचकांक में सख्ती से सकारात्मक रूप से प्रकट होने की अनुमति दी थी , और आपके पास impredicative Prop था , तो आप एक असंगति के माध्यम से एक असंगति को एक प्रकार से प्राप्त कर सकते हैं जो नकारात्मक रूप से होता है, जैसा कि दान ने टिप्पणियों में कहा है। यहाँ Coq में एक उदाहरण है, जिसमें आगमनात्मक प्रकार को स्वयंसिद्ध कहा गया है।

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.

मुझे यकीन नहीं है कि क्या आप भी ऐसा कर सकते हैं जब आपके पास केवल ब्रह्मांड बहुरूपता चाल या इस तरह का सहारा लिए बिना विधेय ब्रह्मांड है।