สัญชาตญาณเบื้องหลังความเป็นบวกซ้อนและตัวอย่างการตอบโต้

Jan 04 2021

ฉันกำลังมองหาที่เงื่อนไข positivity ซ้อนกันชนิดอุปนัยที่ระบุไว้ในคู่มือ Coq ก่อนอื่นมีการอ้างอิงอื่น ๆ (ไม่จำเป็นสำหรับ Coq แต่โดยทั่วไปแล้วจะขึ้นอยู่กับทฤษฎีประเภท) สำหรับเงื่อนไขเชิงบวกที่ซ้อนกันและเกิดขึ้นได้อย่างไร? ฉันพบเอกสารที่เก่ากว่าเช่น Dybjer's Inductive Familiesและ Coquand และประเภทที่กำหนดโดยอุปนัยของ Paulin แต่ฉันเชื่อว่าสิ่งเหล่านี้กล่าวถึงเงื่อนไขเชิงบวกที่เข้มงวดเท่านั้นและเอกสารใหม่กว่าเช่น pCuIC one และA Comprehensive Guide to CICไม่ได้กล่าวถึงความเป็นบวกที่ซ้อนกัน

ตอนนี้ฉันกำลังพยายามทำความเข้าใจโดยสังหรณ์ใจว่าเหตุใดจึงต้องมีความคิดเชิงบวกแบบซ้อนกัน ในสาระสำคัญความเป็นบวกซ้อนกันระบุว่าเมื่อกำหนดตัวสร้าง C สำหรับประเภทอุปนัยบางประเภท$D$ถ้าประเภทของอาร์กิวเมนต์ถึง $C$ เป็นสิ่งที่ชอบ $I ~ \vec{p} ~ \vec{t}$แล้ว $D$ สามารถปรากฏในเชิงบวกอย่างเคร่งครัดเท่านั้น $\vec{p}$และเฉพาะในกรณีที่ $I \neq D$. ฉันเข้าใจว่าการอนุญาต$D$ ในตำแหน่งลบของ $\vec{p}$ โดยทั่วไปจะช่วยให้สามารถพิสูจน์ได้ $(D \to \bot) \to \bot$และการอนุญาต $D$ในตำแหน่งบวกอื่น ๆ โดยพื้นฐานแล้วจะช่วยให้สามารถกำจัดการปฏิเสธสองครั้งได้ (และบางสิ่งที่ไม่สอดคล้องกันกับ Prop ที่ไม่สามารถรับรองได้) สิ่งที่ฉันไม่เข้าใจคือ:

  • ทำไมไม่ได้ $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}$, ที่ไหน $=$ เป็นประเภทความเท่าเทียมกันตามปกติ

    แก้ไข: ปรากฎว่าสิ่งนี้ไม่ได้พิมพ์ check in Agda ด้วยเหตุผลระดับจักรวาลที่ไม่เกี่ยวข้องดังนั้นให้พิจารณาสิ่งต่อไปนี้ที่ Agda ปฏิเสธด้วยเหตุผลด้านบวกแทน:

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

    นี้เป็นที่ยอมรับจาก AGDA ถ้าAเป็นแทนพารามิเตอร์ตามที่คาดไว้จากกฎ positivity ซ้อนกัน

ฉันสนใจเป็นพิเศษในการค้นหาตัวอย่างที่การละเมิดเงื่อนไขด้านบวกซ้อนกัน (โดยเฉพาะสองสิ่งนี้ที่ฉันได้ระบุไว้) ทำให้เกิดความไม่สอดคล้องกันและการพิสูจน์ $\bot$ซึ่งโดยส่วนตัวแล้วจะเข้าใจได้ง่ายกว่าข้อโต้แย้งเกี่ยวกับความน่าเบื่อ

คำตอบ

1 DanDoel Jan 07 2021 at 02:15

นี่คือตัวอย่างการใช้ประโยชน์จากดัชนีเชิงบวกเพื่อพิสูจน์เท็จ:

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

โดยพื้นฐานแล้ว $ℕ$ เป็นต้นไม้ที่ติดตามว่าเราต้องเปิดรังมากแค่ไหน

ionathanch Jan 07 2021 at 02:18

ผมจะตอบประเด็นที่ 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.

ฉันไม่แน่ใจว่าคุณจะทำเช่นเดียวกันได้หรือไม่เมื่อคุณมีเพียงจักรวาลที่คาดเดาได้โดยไม่ต้องใช้กลอุบายของความหลากหลายของจักรวาลหรือสิ่งที่คล้ายกัน