Intuición detrás de positividad anidada y contraejemplos

Jan 04 2021

Estoy viendo las condiciones de positividad anidadas para los tipos inductivos indicadas en el manual de Coq . En primer lugar, ¿existen otras referencias (no necesariamente para Coq, pero en las teorías de tipos dependientes en general) para las condiciones de positividad anidadas y cómo se producen? Encontré artículos más antiguos como Familias inductivas de Dybjer y Coquand y Tipos definidos inductivamente de Paulin , pero creo que estos solo mencionan la condición de positividad estricta, y los artículos más nuevos como pCuIC one y A Comprehensible Guide to CIC tampoco mencionan la positividad anidada.

Ahora, estoy tratando de obtener una comprensión intuitiva de por qué se requiere la positividad anidada. En esencia, la positividad anidada establece que al definir un constructor C para algún tipo inductivo$D$, si el tipo de argumento para $C$ es algo como $I ~ \vec{p} ~ \vec{t}$, entonces $D$ sólo puede aparecer de forma estrictamente positiva en $\vec{p}$, y solo si $I \neq D$. Entiendo que permitiendo$D$ en posiciones negativas de $\vec{p}$ básicamente permite pruebas de $(D \to \bot) \to \bot$y permitiendo $D$en otras posiciones positivas esencialmente permite la eliminación de la doble negación (y algunas cosas de inconsistencia con Prop impredicativo). Lo que no entiendo son estos:

Porque no puedo $D$ aparecen estrictamente positivamente en $\vec{p}$ Si $I = D$(ya sea como argumento de constructor o tipo de retorno)? Por ejemplo, para un constructor$C$ de tipo inductivo $D ~ (A: \textrm{Type}): \textrm{Type}$ (con $A$ como único parámetro), ¿por qué $C: D ~ (D ~ A) \to D ~ A$ no permitido?

EDITAR: No solo se acepta esto en Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ también se acepta, lo que me parece sospechoso.
¿Por qué puede $D$de lo contrario, aparecerán estrictamente positivamente en los parámetros $\vec{p}$, pero no en los índices $\vec{t}$? ~~Considere, por ejemplo, el constructor (bastante tonto) $C: (D =_{\textrm{Type}} D) \to D$ para el tipo inductivo $D: \textrm{Type}$, dónde $=$ es el tipo de igualdad habitual.~~

EDITAR: Resulta que esto no escribe verificación en Agda por razones de nivel de universo no relacionadas, así que considere lo siguiente que Agda rechaza por razones de positividad:
```
data Box : (A : Set) → Set where
  box : (A : Set) → Box A

data D : Set where
  C : Box D → D
```
Esto es aceptado por Agda si en Acambio es un parámetro, como se esperaba de las reglas de positividad anidadas.

Estoy particularmente interesado en encontrar ejemplos donde violar las condiciones de positividad anidadas (específicamente estas dos que he enumerado) causa inconsistencias y pruebas de $\bot$, que personalmente sería más fácil de entender que los argumentos sobre la monotonicidad.

Respuestas

1 DanDoel Jan 07 2021 at 02:15

Aquí hay un ejemplo que aprovecha la positividad de un índice para probar que es falso:

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)

Técnicamente, también hace uso del hecho de que la inducción-recursión puede crear pequeños universos, y que la igualdad de tipos puede ser menor que la igualdad general aplicada al universo, pero por lo demás no son realmente problemáticos que yo sepa (Coq tiene igualdad impredicativa de todos modos, yo creer). Es posible que la definición simultánea también se elimine, pero al menos no es sencillo.

Editar: Pregunté sobre tu primer punto. Se me señaló que esencialmente no hay nada especial en un tipo anidado que está anidado en sí mismo. Este artículo muestra cómo utilizar una traducción no nativa de tipos anidados en tipos indexados de tamaño equivalente. Al hacerlo, siempre que el anidamiento sea estrictamente positivo, no es difícil aplicar la traducción a un tipo indexado estrictamente positivo.

O, por ejemplo, la traducción de ejemplo que me mostraron usa un $ℕ$ parámetro en lugar de autoanidado:

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

Donde agregué el tconstructor para hacer que algo realmente se use A, y D Aestá destinado a ser equivalente a D' A 0. Creo que otra forma de escribir esto sería:

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

Esencialmente, el $ℕ$ es un árbol que rastrea la cantidad de anidación que necesitamos desplegar.

ionathanch Jan 07 2021 at 02:18

Voy a responder parcialmente al punto 2 aquí. Si permitido tipo inductivo que aparezca incluso estrictamente positiva en el índice de otra inductiva, y que tenía impredicativo Prop , se podría derivar una inconsistencia a través de un tipo de igualdad con un tipo que no se producen negativamente, como Dan se indica en los comentarios. Aquí hay un ejemplo en Coq, con el tipo inductivo expresado como axiomas.