¿Cuáles son las consecuencias negativas de extender CIC con axiomas?

¿Es cierto que agregar axiomas al CIC podría tener influencias negativas en el contenido computacional de definiciones y teoremas? Entiendo que, en el comportamiento normal de la teoría, cualquier término cerrado se reducirá a su forma canónica normal, por ejemplo, si es verdadero, entonces debe reducirse a un término de la forma . Pero cuando postulamos un axioma, digamos la función axioma de extensionalidad , simplemente agregamos una nueva constante al sistema$n : \mathbb{N}$$n$$(succ ... (succ (0)))$funext

eso solo "mágicamente" produce una prueba de de cualquier prueba de , sin ningún significado computacional ( en el sentido de que no podemos extraer ningún código de ellos? )$f = g$$\Pi_{x : A} f (x) = g (x)$

Pero, ¿por qué es esto "malo"?

Porque funext, leí en esta entrada de coq y en esta pregunta de mathoverflow que hará que el sistema pierda la canonicidad o la verificación decidible. La entrada de coq parece presentar un buen ejemplo, pero todavía me gustaría obtener más referencias al respecto, y de alguna manera no puedo encontrar ninguna.

¿Cómo es que agregar axiomas adicionales podría causar que CIC tenga un comportamiento peor? Cualquier ejemplo práctico sería genial. (Por ejemplo, ¿el axioma de la univalencia?) Me temo que esta pregunta es demasiado blanda, pero si alguien pudiera arrojar algo de luz sobre esos temas o darme algunas referencias, ¡sería genial!

PD: La entrada de Coq menciona que "Thierry Coquand ya observó que la coincidencia de patrones sobre familias intensivas es inconsistente con la extensionalidad a mediados de los años 90". ¿Alguien sabe en qué papel o algo?

Una primera razón para rechazar axiomas es que pueden ser inconsistentes. Incluso para los axiomas que se prueban consistentes, algunos de ellos tienen una interpretación computacional (sabemos cómo extender la igualdad de definición con un principio de reducción para ellos) y otros no, eso rompe la canonicidad. Esto es "malo" por diferentes razones:

• En teoría, la canonicidad le permite probar cosas sobre los valores de su idioma, sin tener que recurrir a un modelo específico. Es una propiedad muy satisfactoria pensar en su sistema; en particular, respalda las afirmaciones sobre el mundo real: podemos considerar el nattipo formalizado en el sistema como realmente "números naturales" porque podemos demostrar que sus habitantes normales cerrados realmente son números naturales. De lo contrario, es fácil pensar que modeló algo correctamente en su sistema, pero en realidad está trabajando con diferentes objetos.

• En la práctica, la reducción es un activo importante de las teorías de tipo dependiente, porque facilita la prueba. Probar una igualdad proposicional puede ser arbitrariamente difícil, mientras que probar una igualdad definicional es (con menos frecuencia posible) pero mucho más fácil, ya que el término de prueba es trivial. En términos más generales, el cómputo es un aspecto central de la experiencia del usuario de un asistente de pruebas, y es común definir las cosas solo para que se reduzcan correctamente como se espera. (No necesita axiomas para dificultar el cálculo; por ejemplo, usar el principio de conversión en igualdades proposicionales ya puede bloquear las reducciones). Todo el negocio de la prueba por reflexión.se basa en el uso de la computación para ayudar a las pruebas. Esta es una diferencia importante en potencia y conveniencia con respecto a otros asistentes de prueba basados ​​en lógica (por ejemplo, HOL-light, que solo admite razonamiento de igualdad; o vea Zombie para un enfoque diferente), y el uso de axiomas no controlados u otros estilos de programación, puede sacarte de esta zona de confort.

Para entender por qué extender un probador de teoremas con algunos axiomas puede causar problemas, también es interesante ver cuándo es benigno hacerlo. Se me ocurren dos casos y ambos tienen que ver con el hecho de que no nos importa el comportamiento computacional de los postulados.

• En la teoría de tipo observacional, es posible postular una prueba de cualquier coherencia Propsin perder la canonicidad. De hecho, todas las pruebas se consideran iguales y el sistema hace cumplir esto al negarse por completo a mirar los términos. Como consecuencia, el hecho de que una prueba fue construida a mano o simplemente postulada no tiene ninguna consecuencia. Un ejemplo típico sería la prueba de la "cohesión": si tenemos una prueba de eqque A = B : Typea continuación, para cualquier ttipo A, t == coerce A B eq tdonde coercesimplemente transporta a lo largo de un período de prueba de una igualdad.

• En MLTT, uno puede postular cualquier axioma negativo constante sin pérdida de canonicidad . La intuición detrás de esto es que los axiomas negativos (axiomas de la forma A -> False) solo se usan para descartar ramas irrelevantes. Si el axioma es consistente, entonces solo se puede usar en ramas que de hecho son irrelevantes y, por lo tanto, nunca se tomarán al evaluar los términos.

Un ejemplo práctico de un axioma que se comporta mal se pregunta, ¿qué pasa con esto?

 0 = 1

El documento de Coquand mencionado podría ser [1], donde muestra que la ITT dependiente (teoría de tipo intuicionista de Martin-Löf) extendida con coincidencia de patrones le permite probar UIP (axioma de unicidad de las pruebas de identidad ). Más tarde, Streicher y Hoffmann [2] presentan un modelo de ITT que falsifica UIP. Por lo tanto, la coincidencia de patrones no es una extensión conservadora de ITT.

1. T. Coquand, coincidencia de patrones con tipos dependientes .

2. M. Hofmann, T. Streicher, La interpretación grupal de la teoría de tipos .