중첩 된 긍정 성과 반례 뒤에 숨겨진 직감

Jan 04 2021

Coq 매뉴얼에 명시된 유도 유형에 대한 중첩 된 양성 조건을 살펴보고 있습니다 . 우선 중첩 된 긍정 성 조건과 그 결과에 대한 다른 참조가 있습니까 (Coq에 반드시 필요한 것은 아니지만 일반적으로 종속 유형 이론에 있음)? 나는 Dybjer의 Inductive Families 및 Coquand 및 Paulin의 Inductively Defined Types 와 같은 오래된 논문을 찾았 지만, 이들은 엄격한 양성 조건 만 언급하고 pCuIC 1 및 A Comprehensible 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}$, 어디 $=$ 일반적인 평등 유형입니다.~~

편집 : 이것은 관련되지 않은 우주 수준의 이유로 Agda에서 유형 검사를하지 않는 것으로 밝혀 졌으므로 대신 Agda가 긍정적 인 이유로 거부하는 다음을 고려하십시오.
```
data Box : (A : Set) → Set where
  box : (A : Set) → Box A

data D : Set where
  C : Box D → D
```
이것은 되는 경우 AGDA에서 허용 A하는 대신 매개 변수 중첩 양성 규칙에서 예상대로.

특히 중첩 된 양성 조건 (특히 내가 나열한이 두 가지)을 위반하면 불일치 및 증거가 발생하는 예를 찾는 데 관심이 있습니다. $\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 소유했다 , 당신은 유형 평등 형식을 통해 불일치를 도출 할 수 않습니다 댄 코멘트에 명시된 바와 같이, 부정적인 발생합니다. 다음은 유도 유형이 공리로 표시된 Coq의 예입니다.