¿Por qué Agda y Coq no están de acuerdo con la positividad estricta?

Me topé con un desacuerdo confuso entre Agda y Coq que obviamente no está relacionado con las distinciones más conocidas entre sus teorías de tipo (por ejemplo, (im) predicatividad, inducción-recursión, etc.).

En particular, Agda acepta la siguiente definición:

  data Ty : Set0 -> Set0 where
    c1 : Ty ℕ
    c2 : Ty (Ty ℕ)

mientras que la definición equivalente de Coq se rechaza porque se considera que la aparición de [Ty _] como un índice de sí mismo en c2 viola la positividad estricta.

  Inductive Ty : Set -> Set :=
    | c1 : Ty nat
    | c2 : Ty (Ty nat).

De hecho, este caso es casi literalmente un ejemplo de la Sección 14.1.2.1 de Coq'Art de violar la positividad estricta:

  Inductive T : Set -> Set := c : (T (T nat)).

Pero no veo las razones de esta diferencia entre las teorías de tipos. El ejemplo clásico de probar False usando una ocurrencia negativa de un tipo en un argumento de constructor es claro para mí, pero no puedo ver cómo uno podría derivar una contradicción de este estilo de indexación (independientemente de los argumentos de constructor estrictamente positivos).

Al revisar la literatura, el primer artículo de Indbctive Families de Dybjer hace un comentario casual sobre la solución de Paulin-Mohring en el documento del CID que tiene restricciones ligeramente diferentes, y sugiere vagamente que las diferencias podrían estar relacionadas con la impredecibilidad, pero no da más detalles. El artículo de Dybjer parece permitir esto, mientras que el de Paulin-Mohring lo prohíbe claramente.

Aparentemente, no soy el primero en notar esta diferencia de opinión, y algunos creen que esta definición no debería permitirse en ninguno de los sistemas ( https://lists.chalmers.se/pipermail/agda/2012/004249.html ), pero No he encontrado ninguna explicación de por qué está bien en un sistema pero no en el otro, o simplemente una diferencia de opinión.

Entonces supongo que tengo varias preguntas:

1. ¿Es este un ejemplo de un tipo monótono, pero no estrictamente positivo? (En Coq; claramente Agda lo considera estrictamente positivo)
2. ¿Por qué Agda permite esto mientras Coq lo rechaza? Es simplemente una diferencia idiosincrásica en la interpretación de "estrictamente positivo", ¿existe una sutil diferencia entre Coq y Agda que lo hace sonar en Agda y no es sólido en Coq, o es una cuestión de gusto impulsada por preferencias teóricas particulares?
3. ¿Existe una diferencia significativa entre la primera definición anterior y la definición inductiva-recursiva equivalente a continuación?

Definición inductiva-recursiva:

  mutual
    data U : Set0 -> Set0 where
      c : (i : Fin 2) -> U (T i)
    T : Fin 2 -> Set0
    T zero = ℕ
    T (suc zero) = U ℕ

Estoy feliz de tener consejos sobre literatura relevante.

Gracias por adelantado.

El problema parece ser la confusión resultante de una confluencia de dos factores:

1. Estaba usando una versión obsoleta de Agda (2.3.0.1). Parece que antes de 2.3.2, Agda simplemente no estaba verificando la estricta positividad de los índices de resultados del constructor (vea el error que vinculé en otra parte del hilo).
2. Una lectura más detallada del artículo de las familias inductivas de Dybjer sugiere que él pudo haber pretendido que el tipo inductivo que se define no esté vinculado al escribir los índices de un resultado de constructor . La Sección 3.2.1 proporciona el esquema para los constructores inductivos en prosa, y aparentemente leí mal el lenguaje que describe los entornos vinculantes de cada parte del esquema.

Esta lectura más cercana es, por supuesto, consistente con la verificación que realizan Coq y (versiones recientes de) Agda, que prohíben cualquier aparición de T en sus propios índices.

Una posible razón de la diferencia, como sugieren sus propias observaciones, es la impredicatividad. Históricamente, Coq tenía un conjunto impredecible (¡todavía disponible como bandera, creo!)

Citando el libro de Adam Chlipala http://adam.chlipala.net/cpdt/html/Universes.html

Las herramientas Coq admiten una marca de línea de comandos -impredicative-set, que modifica Gallina de una manera más fundamental al hacer que Set sea impredecible. Un término como forall T: Set, T tiene el tipo Set y las definiciones inductivas en Set pueden tener constructores que cuantifican los argumentos de cualquier tipo. Para mantener la coherencia, se debe imponer una restricción de eliminación, de manera similar a la restricción para la Prop. La restricción solo se aplica a los tipos inductivos grandes, donde algún constructor cuantifica sobre un tipo de tipo Tipo. En tales casos, un valor en este tipo inductivo solo puede coincidir con un patrón para producir un tipo de resultado cuyo tipo es Set o Prop. Esta regla contrasta con la regla para Prop, donde la restricción se aplica incluso a tipos inductivos no grandes, y donde el tipo de resultado solo puede tener el tipo Prop. En versiones anteriores de Coq, Set era impredecible por defecto. Las versiones posteriores hacen que Set sea predicativo para evitar inconsistencias con algunos axiomas clásicos. En particular, se debe tener cuidado cuando se utiliza un conjunto impredecible con axiomas de elección. En combinación con la extensionalidad media o predicada excluida, puede producirse una inconsistencia. El conjunto impredecible puede ser útil para modelar conceptos matemáticos inherentemente impredecibles, pero casi todos los desarrollos de Coq funcionan sin él.