Quelles sont les conséquences négatives de l'extension du CIC aux axiomes?

Est-il vrai que l'ajout d'axiomes au CIC pourrait avoir des influences négatives sur le contenu informatique des définitions et des théorèmes? Je comprends que, dans le comportement normal, un terme fermé réduit à sa forme normale canonique de la théorie, par exemple , si est vrai, alors n doit réduire à un terme de la forme ( s u c c . . . ( S u c c ( 0 ) ) ) . Mais lorsque nous postulons un axiome - disons l'axiome d'extension de fonction - nous ajoutons simplement une nouvelle constante au système$n : \mathbb{N}$$n$$(succ ... (succ (0)))$funext

qui produira juste "par magie" une preuve de partir de n'importe quelle preuve de Π x : A f ( x ) = g ( x ) , sans aucune signification informatique ( dans le sens où nous ne pouvons pas en extraire de code? )$f = g$$\Pi_{x : A} f (x) = g (x)$

Mais pourquoi est-ce "mauvais"?

Car funext, j'ai lu dans cette entrée coq et cette question mathoverflow que cela entraînera une perte de canonicité ou une vérification décidable du système. L'entrée coq semble présenter un bon exemple, mais j'aimerais quand même avoir plus de références à ce sujet - et je ne peux pas en trouver.

Comment est-ce que l'ajout d'axiomes supplémentaires pourrait entraîner un comportement pire de CIC? Tout exemple pratique serait formidable. (Par exemple, l'Axiom Univalence?) Je crains que cette question ne soit trop douce, mais si quelqu'un pouvait faire la lumière sur ces questions ou me donner des références, ce serait génial!

PS: L'entrée du coq mentionne que "Thierry Coquand a déjà observé que la correspondance des modèles sur les familles intensionnelles est incompatible avec l'extensionnalité au milieu des années 90." Est-ce que quelqu'un sait dans quel papier ou quelque chose?

Une première raison de rejeter les axiomes est qu'ils pourraient être incohérents. Même pour les axiomes qui se sont avérés cohérents, certains d'entre eux ont une interprétation informatique (nous savons comment étendre l'égalité de définition avec un principe de réduction pour eux) et d'autres non - ceux qui cassent la canonicité. C'est "mauvais" pour différentes raisons:

• En théorie, la canonicité vous permet de prouver des choses sur les valeurs de votre langue, sans avoir à passer par un modèle spécifique. C'est une propriété très satisfaisante d'avoir à penser à votre système; en particulier, il soutient les affirmations sur le monde réel - nous pouvons penser que le nattype formalisé dans le système est vraiment des «nombres naturels» parce que nous pouvons prouver que ses habitants normaux fermés sont vraiment des nombres naturels. Sinon, il est facile de penser que vous avez modélisé quelque chose correctement dans votre système, mais que vous travaillez en fait avec différents objets.

• En pratique, la réduction est un atout majeur des théories de type dépendantes, car elle facilite la preuve. Prouver une égalité propositionnelle peut être arbitrairement difficile, tandis que prouver une égalité définitionnelle est (moins souvent possible) mais beaucoup plus facile, car le terme de preuve est trivial. Plus généralement, le calcul est un aspect central de l'expérience utilisateur d'un assistant de preuve, et il est courant de définir des choses juste pour qu'elles se réduisent correctement comme vous vous y attendez. (Vous n'avez pas besoin d'axiomes pour rendre le calcul difficile; par exemple, l'utilisation du principe de conversion sur les égalités propositionnelles peut déjà bloquer les réductions). Toute l'activité de la preuve par la réflexionest basé sur l'utilisation du calcul pour aider les preuves. Il s'agit d'une différence majeure de puissance et de commodité par rapport à d'autres assistants de preuve basés sur la logique (par exemple, HOL-light, qui ne prend en charge que le raisonnement d'égalité; ou consultez Zombie pour une approche différente), et en utilisant des axiomes non contrôlés ou d'autres styles de programmation, peut vous sortir de cette zone de confort.

Pour comprendre pourquoi l'extension d'un prouveur de théorème avec certains axiomes peut causer des problèmes, il est également intéressant de voir quand il est bénin de le faire. Deux cas me viennent à l'esprit et ils ont tous deux à voir avec le fait que nous ne nous soucions pas du comportement informatique des postulats.

• En théorie du type observationnel, il est possible de postuler une preuve de toute cohérence Propsans perdre la canonicité. En effet, toutes les preuves sont considérées comme égales et le système les applique en refusant complètement de regarder les termes. Par conséquent, le fait qu'une preuve ait été construite à la main ou simplement postulée n'a aucune conséquence. Un exemple typique serait la preuve de la « cohésion »: si nous avons une preuve eqqui A = B : Typealors pour tout tde type A, t == coerce A B eq toù coercetransporte simplement un terme le long d' une preuve de l' égalité.

• Dans MLTT, on peut postuler n'importe quel axiome négatif cohérent sans perte de canonicité . L'intuition derrière cela est que les axiomes négatifs (axiomes de la forme A -> False) ne sont utilisés que pour rejeter les branches non pertinentes. Si l'axiome est cohérent, il ne peut être utilisé que dans des branches qui sont en effet hors de propos et ne seront donc jamais prises lors de l'évaluation des termes.

Un exemple pratique d'un axiome qui se comporte mal, vous demandez quoi?

 0 = 1

L'article Coquand auquel il est fait référence pourrait être [1], où il montre que l'ITT dépendant (théorie du type intuitionniste de Martin-Löf) étendu avec la correspondance de motifs vous permet de prouver l'UIP (axiome d' unicité des preuves d'identité ). Plus tard, Streicher et Hoffmann [2] présentent un modèle d'ITT qui falsifie l'UIP. Par conséquent, la correspondance de motifs n'est pas une extension conservatrice de l'ITT.

1. T. Coquand, Correspondance de motifs avec des types dépendants .

2. M. Hofmann, T. Streicher, L'interprétation groupoïde de la théorie des types .