İç içe geçmiş pozitifliğin ve karşı örneklerin ardındaki sezgi
Coq kılavuzunda belirtilen endüktif tipler için iç içe geçmiş pozitiflik koşullarına bakıyorum . Öncelikle, iç içe geçmiş pozitiflik koşulları ve bunların nasıl ortaya çıktığı için başka referanslar (Coq için zorunlu değil, ancak genel olarak bağımlı tip teorilerde) var mı? Dybjer'in Endüktif Aileleri ve Coquand ve Paulin'in Endüktif Olarak Tanımlanmış Türleri gibi daha eski makaleler buldum , ancak bunların yalnızca katı pozitiflik koşulundan bahsettiğine inanıyorum ve pCuIC ve CIC için Anlaşılır Bir Kılavuz gibi daha yeni makaleler de iç içe pozitiflikten bahsetmiyor.
Şimdi, iç içe pozitifliğin neden gerekli olduğuna dair sezgisel bir anlayış kazanmaya çalışıyorum. Temelde, iç içe geçmiş pozitiflik, bazı endüktif tipler için bir yapıcı C'yi tanımlarken$D$, eğer bir argümanın türü $C$ gibi bir şey $I ~ \vec{p} ~ \vec{t}$, sonra $D$ sadece kesinlikle olumlu görünebilir $\vec{p}$ve sadece $I \neq D$. İzin vermeyi anlıyorum$D$ negatif pozisyonlarda $\vec{p}$ temelde kanıtlara izin verir $(D \to \bot) \to \bot$ve izin vermek $D$diğer pozitif konumlarda, esasen çifte olumsuzlamanın ortadan kaldırılmasına (ve impredicative Prop ile bazı tutarsızlıklara) izin verir. Anlamadığım şey bunlar:
Neden yapamıyorum $D$ kesinlikle olumlu görünüyor $\vec{p}$ Eğer $I = D$(yapıcı bağımsız değişkeni veya dönüş türü olarak)? Örneğin, bir yapıcı için$C$ endüktif tip $D ~ (A: \textrm{Type}): \textrm{Type}$ (ile $A$ tek parametre olarak), neden $C: D ~ (D ~ A) \to D ~ A$ izin verilmiyor mu?
DÜZENLEME: Bu sadece Agda 2.6.1.2'de kabul edilmiyor, $C: D ~ (D ~ A \to \bot) \to D ~ A$ da kabul edildi, bu bana şüpheli geliyor.
Neden olabilir $D$aksi halde parametrelerde kesinlikle olumlu görünür $\vec{p}$ama endekslerde değil $\vec{t}$?
Örneğin (oldukça aptalca) kurucuyu düşünün $C: (D =_{\textrm{Type}} D) \to D$ endüktif tip için $D: \textrm{Type}$, nerede $=$ olağan eşitlik türüdür.DÜZENLEME: Bunun, evren düzeyinde ilgisiz nedenlerle Agda'da denetim yazmadığı ortaya çıktı, bu nedenle, bunun yerine Agda'nın pozitiflik nedenleriyle reddettiği aşağıdakileri düşünün:
data Box : (A : Set) → Set where box : (A : Set) → Box A data D : Set where C : Box D → D
Bu , Agda tarafından
A
, iç içe yerleştirilmiş pozitiflik kurallarından beklendiği gibi, bunun yerine bir parametre ise kabul edilir .
İç içe geçmiş pozitiflik koşullarını ihlal etmenin (özellikle listelediğim bu ikisi) tutarsızlıklara ve kanıtlara neden olduğu örnekleri bulmakla özellikle ilgileniyorum. $\bot$, kişisel olarak monotonluk hakkındaki tartışmalardan daha kolay anlaşılır.
Yanıtlar
Yanlış olduğunu kanıtlamak için bir dizinin pozitifliğinden yararlanan bir örnek:
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)
Teknik olarak, aynı zamanda, tümevarım-özyinelemenin küçük evrenler yaratabileceği ve bu tip eşitliğinin evrene uygulanan genel eşitlikten daha küçük olabileceği gerçeğini de kullanır, ancak bunlar benim bilgim için gerçekten sorunlu değildir (Coq yine de ölçüsüz eşitliğe sahiptir, I inan). Eşzamanlı tanımın da ortadan kaldırılması mümkündür, ancak en azından basit değildir.
Düzenleme: Etrafa ilk madde işaretinizi sordum. İç içe geçmiş bir tipte esasen özel bir şey olmadığı bana belirtildi. Bu makale , iç içe geçmiş türlerin yerel olmayan çevirisinin, eşdeğer boyuttaki dizine alınmış türlere nasıl kullanılacağını gösterir. Bunu yaptığınızda, iç içe yerleştirme kesinlikle pozitif olduğu sürece, çeviriyi kesinlikle pozitif indekslenmiş bir türe uygulamak zor değildir.
Veya örneğin, bana gösterilen örnek çeviri iç içe geçmiş bir $ℕ$ kendi kendine yuvalama yerine parametre:
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
Eklediğim Nerede t
yapıcı bir şey aslında kullandığından emin olmak için A
, ve D A
eşdeğer olması gerekiyordu D' A 0
. Sanırım bunu yazmanın başka bir yolu da:
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
Esasen, $ℕ$ ne kadar iç içe geçmemiz gerektiğini izleyen bir ağaçtır.
Burada 2. maddeyi kısmen cevaplayacağım. Eğer endüktif tip başka endüktif dizinine bile kesinlikle olumlu görünmesine izin varsa ve siz impredicative Prop vardı , bir türüyle bir eşitlik türü aracılığıyla bir tutarsızlık elde edebileceğini gelmez Dan yorumlarda belirtildiği gibi, olumsuz ortaya çıkar. Aşağıda, aksiyomlar olarak belirtilen tümevarım tipi ile Coq'da bir örnek verilmiştir.
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.
Evren polimorfizmi hilelerine veya benzerlerine başvurmadan yalnızca öngörücü evrenleriniz olduğunda aynı şeyi yapıp yapamayacağınızdan emin değilim.