No, en este caso, la predicatividad y la monotonicidad no están estrechamente relacionadas.
La verificación de positividad en Coq / Adga sirve para asegurarse de que está tomando el punto menos fijo de una cosa monótona, aproximadamente.
Aquí le mostramos cómo pensar en tipos inductivos en términos de redes y operadores monótonos. Recuerde que el teorema de Knaster-Tarski dice que en una red completa , cada operador monótono f : L → L tiene un punto fijo mínimo μ ( f ) . A continuación, podemos pensar en los tipos en una teoría de tipos como formando una red bajo capacidad de prueba. Es decir, el tipo S es inferior a T si la verdad de S implica la de T . Ahora, lo que nos gustaría hacer es tomar un operador monótono F μ ( F ) . Lf:L→Lμ(f)STSTF en tipos y usar Knaster-Tarski para obtener una interpretación del punto menos fijo de este operadorμ(F)
Sin embargo, los tipos en la teoría de tipos no son solo una red: forman una categoría. Es decir, dado dos tipos y T , potencialmente hay muchas maneras para que S por debajo de T , con una forma para cada prueba e : S → T . Por lo tanto, un operador tipo F también tiene que hacer algo sensato en estas pruebas. La generalización apropiada de la monotonicidad es la functorialidad . Es decir, queremos que F tenga un operador en los tipos, y también que tenga una acción en las pruebas, de modo que si e : S → T , entonces F (STSTe:S→TFFe:S→T .F(e):F(S)→F(T)
Ahora, la funcionalidad se conserva mediante sumas y productos (es decir, si y G son endofunctores en los tipos, entonces F + G y F × G (actuando puntualmente) también son functores en los tipos (suponiendo que tengamos sumas y productos en nuestro álgebra de tipos). Sin embargo, el espacio de funciones no lo conserva, ya que el bifunctor exponencial F → G es contravariante en su argumento izquierdo. Entonces, cuando escribe una definición de tipo inductivo, está definiendo un functor para tomar un punto menos fijo. Para asegurarse de que realmente es un functor, debe descartar las ocurrencias del parámetro recursivo en el lado izquierdo de los espacios de funciones, de ahí la verificación de positividad.FGF+GF×GF→G
La impredicatividad (en el sentido del Sistema F) generalmente se evita, porque es un principio que te obliga a elegir entre la lógica clásica y los modelos de teoría de conjuntos. No puede interpretar tipos como conjuntos en la teoría de conjuntos clásica si tiene indexación de estilo F. (Ver el famoso "Polimorfismo de Reynolds no es teórico").
Categóricamente, la impredicatividad de estilo F dice que la categoría de tipos y términos forma una pequeña categoría completa (es decir, homs y objetos son conjuntos y existen límites de todos los diagramas pequeños). Clásicamente, esto obliga a una categoría a ser un poset. Muchos constructivistas son constructivos porque quieren que sus teoremas mantengan más sistemas que la lógica clásica, por lo que no quieren probar nada que sea clásicamente falso. Por lo tanto, desconfían del polimorfismo impredecible.
Sin embargo, el polimorfismo le permite decir muchas condiciones que son clásicamente "grandes" internamente para su teoría de tipos, ¡y la positividad es una de ellas! Un operador tipo es functorial, si puede producir un término polimórfico:F
Fmap:∀α,β.(α→β)→(F(α)→F(β))
¿Ves cómo esto corresponde a la functorialidad? En mi opinión, esta sería una muy buena opción para tener en Coq, ya que le permitiría hacer una programación genérica mucho más fácilmente. La naturaleza sintáctica de la verificación de positividad es un gran obstáculo para la programación genérica, y me complacería cambiar la posibilidad de axiomas clásicos por programas funcionales más flexibles.
EDITAR: La pregunta que está haciendo sobre la diferencia entre Prop y Set surge del hecho de que los desarrolladores de Coq quieren permitirle pensar sobre los teoremas de Coq en términos ingenuos de teoría de conjuntos si lo desea, sin forzar a hacerlo. Técnicamente, dividen Prop y Set, y luego prohíben que los sets dependan del contenido computacional de Prop.
Por lo tanto, puede interpretar Prop como valores de verdad en ZFC, que son los booleanos verdadero y falso. En este mundo, todas las pruebas de proposiciones son iguales, por lo que obviamente no debería poder ramificarse en la prueba de una proposición. Por lo tanto, la prohibición de conjuntos que dependen del contenido computacional de las pruebas de Prop es totalmente sensata. Además, la red booleana de 2 elementos es obviamente una red completa, por lo que debe admitir la indexación impredecible, ya que existen reuniones arbitrarias con valores establecidos. La restricción de predicatividad en los conjuntos surge del hecho (mencionado anteriormente) de que la indexación de estilo F es degenerada en los modelos clásicos de teoría de conjuntos.
Coq tiene otros modelos (¡es una lógica constructiva!), Pero el punto es que nunca probará nada por lo que un matemático clásico se sorprendería.
Inductive Blah : Prop := Foo : (Blah -> Blah) -> Blah
mismo que cualquier otra cosa?Inductive prop : Prop := prop_intro : Prop -> prop.
vsInductive set : Set := set_intro: Set -> set.
. ¿Por qué la distinción si la predicatividad no es de interés para la definición inductiva?Type@{i}
, debe vivir en un universo más grande, al menosType@{i+1}
.Existe una conexión muy profunda entre las definiciones inductivas y la impredicatividad, pero entiendo que en el contexto de lo que estás hablando la (im) predicatividad no es particularmente relevante y la prueba es puramente para garantizar la monotonicidad, de modo que la teoría del punto fijo puede ser aplicado, a saber, que el principio de inducción está bien definido. (Estoy dispuesto a ser corregido en este punto).
La relación entre impredicatividad y definiciones inductivas se explora en esta charla de Coquand. Se remonta a algunos resultados de los años 50 por G. Takeuti de que las definiciones impredecibles pueden reducirse a definiciones inductivas. El libro
da un buen análisis del tema, si puede tenerlo en sus manos. Estas diapositivas dan una visión general.
fuente
Solo para completar la excelente explicación de Neil, la impredicatividad tiene un sentido "suave": la definición de conjuntos o colecciones utilizando una referencia a sí mismos. En ese sentido:
es una definición impredecible, ya que define un tipo inductivo, Lam usa un espacio de funciones (Lam -> Lam) que se refiere a la colección misma. En esta situación, la impredicatividad es dañina : es posible usar el teorema de Cantor para probar Falso. De hecho, esta es la misma marca de impredicatividad que descarta la ingenua teoría de conjuntos como una base consistente para las matemáticas. Por lo tanto, no está permitido en Coq. Otra forma de impredicatividad es permitida, como saben:
La definición de Unidad como propuesta hace referencia a la colección de todas las Propuestas de las cuales es miembro. Sin embargo, por razones algo oscuras para mí, esta impredicatividad no es dañina ya que está presente en ZFC (en forma de comprensión ilimitada ) que no se sabe que sea inconsistente.
En conclusión, las ocurrencias negativas de los tipos inductivos en las definiciones es una forma de impredicatividad, pero no a la que generalmente se hace referencia cuando se habla de CoC como marco de referencia impredecible .
fuente
-impredicative-set
en su libro: adam.chlipala.net/cpdt/html/Universes.html , y menciona algunas restricciones sobre la eliminación, pero esto también es oscuro para mí.