Интуиция за вложенным позитивом и контрпримерами
Я смотрю на вложенные условия положительности для индуктивных типов, указанные в руководстве Coq . Во-первых, есть ли какие-либо другие ссылки (не обязательно для Coq, но в теориях зависимых типов в целом) для условий вложенной положительности и как они возникают? Я нашел более старые статьи, такие как Inductive Families Dybjer's и Coquand и Inductively Defined Types Паулина , но я считаю, что в них упоминается только условие строгой положительности, а в более новых статьях, таких как pCuIC one и A Compoughtible 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$в других положительных позициях, по существу, позволяет исключить двойное отрицание (и некоторые несоответствия с непредсказуемой опорой). Вот чего я не понимаю:
Почему не может $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$, что лично было бы легче понять, чем рассуждения о монотонности.
Ответы
Вот пример использования положительности индекса для доказательства ложности:
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. Если вы позволили индуктивному типу появляться даже строго положительно в другом индуктивном индексе, и у вас было непредсказуемое свойство , вы могли бы получить несогласованность через тип равенства с типом, который действительно встречается отрицательно, как сказал Дэн в комментариях. Вот пример в 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.
Я не уверен, сможете ли вы сделать то же самое, когда у вас есть только предикативные вселенные, не прибегая к трюкам с полиморфизмом вселенных и т.п.