ネストされた積極性と反例の背後にある直感

Jan 04 2021

Coqマニュアルに記載されている帰納型のネストされた陽性条件を見ています。まず、ネストされた陽性条件とそれらがどのように発生するかについて、他の参照（Coqである必要はありませんが、一般に依存型理論で）はありますか？DybjerのInductiveFamiliesやCoquandやPaulinのInductivelyDefinedTypesのような古い論文を見つけましたが、これらは厳密な陽性条件についてのみ言及していると思います。pCuICやA Comprehensible Guide toCICのような新しい論文もネストされた陽性については言及していません。

今、私はネストされたポジティブが必要な理由を直感的に理解しようとしています。本質的に、ネストされた陽性は、ある帰納型のコンストラクターCを定義するときに$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
```
ネストされたポジティブルールから予想されるように、これはA代わりにパラメータである場合、Agdaによって受け入れられます。

私は、ネストされた陽性条件（特に私がリストしたこれら2つ）に違反すると、矛盾と証明が生じる例を見つけることに特に興味があります。 $\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に部分的に答えます。ダンがコメントで述べたように、帰納型が別の帰納的インデックスに厳密に正に現れることを許可し、非叙述的な提案があった場合、負に発生する型との等式型によって矛盾を導き出すことができます。これが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.

ユニバースポリモーフィズムのトリックなどに頼らずに、述語ユニバースしかない場合に同じことができるかどうかはわかりません。