Trực giác đằng sau sự tích cực và phản bác lồng ghép

Jan 04 2021

Tôi đang xem xét các điều kiện tích cực lồng nhau cho các loại quy nạp được nêu trong sổ tay Coq . Trước hết, có bất kỳ tài liệu tham khảo nào khác (không nhất thiết cho Coq, nhưng trong các lý thuyết kiểu phụ thuộc nói chung) cho các điều kiện tích cực lồng nhau và chúng ra đời như thế nào? Tôi đã tìm thấy các bài báo cũ hơn như Gia đình quy nạp và Coquand của Dybjer và Các loại xác định tự nhiên của Paulin , nhưng tôi tin rằng những bài báo này chỉ đề cập đến điều kiện tích cực nghiêm ngặt và các bài báo mới hơn như pCuIC và Hướng dẫn dễ hiểu về CIC cũng không đề cập đến tính tích cực lồng nhau.

Bây giờ, tôi đang cố gắng hiểu một cách trực quan về lý do tại sao cần có sự tích cực lồng ghép. Về bản chất, tính tích cực lồng nhau nói rằng khi xác định hàm tạo C cho một số kiểu quy nạp$D$, nếu loại đối số $C$ là một cái gì đó giống như $I ~ \vec{p} ~ \vec{t}$, sau đó $D$ chỉ có thể xuất hiện hoàn toàn tích cực trong $\vec{p}$và chỉ khi $I \neq D$. Tôi hiểu rằng cho phép$D$ ở vị trí tiêu cực của $\vec{p}$ về cơ bản cho phép bằng chứng về $(D \to \bot) \to \bot$và cho phép $D$ở các vị trí tích cực khác về cơ bản cho phép loại bỏ phủ định kép (và một số nội dung không nhất quán với Prop hàm ý). Những gì tôi không hiểu là:

Tại sao không thể $D$ xuất hiện nghiêm túc tích cực trong $\vec{p}$ nếu $I = D$(dưới dạng đối số của hàm tạo hoặc kiểu trả về)? Ví dụ, đối với một hàm tạo$C$ thuộc loại quy nạp $D ~ (A: \textrm{Type}): \textrm{Type}$ (với $A$ là tham số duy nhất), tại sao $C: D ~ (D ~ A) \to D ~ A$ không được phép?

CHỈNH SỬA: Điều này không chỉ được chấp nhận trong Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ cũng được chấp nhận, điều này có vẻ đáng ngờ đối với tôi.
Tại sao có thể $D$nếu không thì xuất hiện hoàn toàn tích cực trong các tham số $\vec{p}$, nhưng không có trong các chỉ số $\vec{t}$? ~~Hãy xem xét ví dụ về hàm tạo (khá ngớ ngẩn) $C: (D =_{\textrm{Type}} D) \to D$ cho loại quy nạp $D: \textrm{Type}$, Ở đâu $=$ là kiểu bình đẳng thông thường.~~

CHỈNH SỬA: Hóa ra điều này không nhập kiểm tra trong Agda vì lý do cấp vũ trụ không liên quan, vì vậy hãy xem xét điều sau đây mà Agda từ chối vì lý do tích cực:
```
data Box : (A : Set) → Set where
  box : (A : Set) → Box A

data D : Set where
  C : Box D → D
```
Điều này được chấp nhận bởi Agda nếu Athay vào đó là một tham số, như mong đợi từ các quy tắc tích cực lồng nhau.

Tôi đặc biệt quan tâm đến việc tìm các ví dụ trong đó vi phạm các điều kiện tích cực lồng nhau (cụ thể là hai điều kiện tôi đã liệt kê này) gây ra sự mâu thuẫn và bằng chứng về $\bot$, về mặt cá nhân sẽ dễ hiểu hơn các lập luận về tính đơn điệu.

Trả lời

1 DanDoel Jan 07 2021 at 02:15

Đây là một ví dụ khai thác tính tích cực của một chỉ mục để chứng minh là sai:

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)

Về mặt kỹ thuật, nó cũng sử dụng thực tế rằng quy nạp-đệ quy có thể tạo ra các vũ trụ nhỏ và bình đẳng kiểu đó có thể nhỏ hơn bình đẳng chung được áp dụng cho vũ trụ, nhưng những điều đó không thực sự có vấn đề với kiến thức của tôi (Dù sao thì Coq cũng có bình đẳng ngầm định, tôi tin). Có thể định nghĩa đồng thời cũng có thể bị loại bỏ, nhưng ít nhất thì nó không thẳng tiến.

Chỉnh sửa: Tôi đã hỏi xung quanh về gạch đầu dòng đầu tiên của bạn. Nó đã được chỉ ra cho tôi rằng về cơ bản không có gì đặc biệt về một kiểu lồng nhau được lồng vào chính nó. Bài viết này hướng dẫn cách sử dụng bản dịch không phải bản địa của các kiểu lồng nhau thành các kiểu được lập chỉ mục có kích thước tương đương. Khi bạn làm điều đó, miễn là lồng ghép là tích cực hoàn toàn, không khó để áp dụng bản dịch cho loại được lập chỉ mục tích cực nghiêm ngặt.

Hoặc ví dụ: bản dịch ví dụ mà tôi được hiển thị sử dụng $ℕ$ tham số thay vì tự lồng:

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

Nơi tôi đã thêm hàm ttạo để làm cho một thứ gì đó thực sự sử dụng Avà D Acó nghĩa là tương đương với D' A 0. Tôi nghĩ một cách khác để viết điều này sẽ là:

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

Về cơ bản, $ℕ$ là một cây theo dõi số lượng tổ mà chúng ta cần mở ra.

ionathanch Jan 07 2021 at 02:18

Tôi sẽ trả lời một phần điểm 2 ở đây. Nếu bạn cho phép các loại quy nạp xuất hiện thậm chí chặt chẽ một cách tích cực trong chỉ mục của quy nạp khác, và bạn có impredicative Prop , bạn có thể lấy được một sự mâu thuẫn thông qua một loại bình đẳng với một loại mà không xảy ra tiêu cực, như Dan nói trong các ý kiến. Đây là một ví dụ trong Coq, với kiểu quy nạp được nêu dưới dạng tiên đề.

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.

Tôi không chắc liệu bạn có làm được như vậy không khi bạn chỉ có các vũ trụ dự đoán mà không cần dùng đến các thủ thuật đa hình vũ trụ hay những thứ tương tự.