สัญชาตญาณเบื้องหลังความเป็นบวกซ้อนและตัวอย่างการตอบโต้
ฉันกำลังมองหาที่เงื่อนไข 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$ซึ่งโดยส่วนตัวแล้วจะเข้าใจได้ง่ายกว่าข้อโต้แย้งเกี่ยวกับความน่าเบื่อ
คำตอบ
นี่คือตัวอย่างการใช้ประโยชน์จากดัชนีเชิงบวกเพื่อพิสูจน์เท็จ:
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
โดยพื้นฐานแล้ว $ℕ$ เป็นต้นไม้ที่ติดตามว่าเราต้องเปิดรังมากแค่ไหน
ผมจะตอบประเด็นที่ 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.
ฉันไม่แน่ใจว่าคุณจะทำเช่นเดียวกันได้หรือไม่เมื่อคุณมีเพียงจักรวาลที่คาดเดาได้โดยไม่ต้องใช้กลอุบายของความหลากหลายของจักรวาลหรือสิ่งที่คล้ายกัน