Tester si une preuve arbitraire est circulaire?

13

Je pensais aux preuves et suis tombé sur une observation intéressante. Les preuves sont donc équivalentes aux programmes via l'isomorphisme de Curry-Howard, et les preuves circulaires correspondent à une récursion infinie. Mais nous savons par le problème de l'arrêt qu'en général, tester si un programme arbitraire se reproduit pour toujours est indécidable. Par Curry-Howard, cela signifie-t-il qu'aucun «vérificateur d'épreuves» ne peut déterminer si une épreuve utilise un raisonnement circulaire?

J'ai toujours pensé que les preuves sont censées être composées d'étapes facilement vérifiables (qui correspondent à des applications de règles d'inférence), et vérifier toutes les étapes vous donne la certitude que la conclusion suit. Mais maintenant je me demande: peut-être qu'il est en fait impossible d'écrire un tel correcteur d'épreuves, car il n'y a aucun moyen de contourner le problème d'arrêt et de détecter le raisonnement circulaire?

logic curry-howard hewasonlyacat
la source

Réponses:

15

La grande majorité des systèmes de preuve ne permettent pas de preuves circulaires infinies, mais ils le font en rendant leurs langages non-Turing complets.

Dans un langage fonctionnel normal, la seule façon de faire durer un programme pour toujours est avec la récursivité, et en termes de théorie, nous considérons généralement la récursivité comme le combinateur , un programme de type : c'est-à-dire qu'il prend une fonction qui fait des appels à un autre argument "self" et le transforme en une seule fonction récursive.Oui∀une.(une→une)→une

Maintenant, appliquez l'isomorphisme de Curry-Howard à ceci: nous avons maintenant une preuve que, pour toute proposition , si s'implique, alors nous pouvons prouver . Nous pouvons tout prouver de cette façon!uneuneune

La clé ici est que le combinateur Y est intégré à un langage, il est considéré comme un axiome. Donc, si vous voulez que cela ne vous cause pas de problèmes, débarrassez-vous-en simplement comme un axiome!

La plupart des systèmes de preuve formels, pour cette raison, nécessitent que votre récursivité soit bien fondée. Ils n'acceptent que les fonctions dont ils peuvent prouver qu'ils s'arrêteront. Et en conséquence, ils rejettent certains programmes qui s'arrêtent, mais pour lesquels ils ne peuvent pas le prouver.

Coq le fait d'une manière assez limitée: il suffit que toutes les fonctions récursives aient un argument où tout appel récursif n'utilise que des versions strictement plus petites de cet argument. Agda fait quelque chose de similaire, mais avec un peu plus de contrôle pour accepter quelques programmes supplémentaires.

jmite
la source
1
Coq exclut-il certains théorèmes légitimes que vous pourriez autrement prouver? Ou existe-t-il toujours des solutions de contournement lorsque le vérificateur de totalité est trop conservateur? (Je suppose que la réponse est la même pour les autres assistants de preuve basés sur la théorie des types dépendants?)
Stovetop
1
@boyers FWIW, dans Coq on peut utiliser Functionou des Program Fixpointconstructions pour prouver qu'une fonction est totale si le vérificateur de totalité échoue. Un exemple simple est la fonction de fusion-tri sur les listes. Il faut prouver manuellement que nous avons divisé les listes (de longueur> 1) en sous-listes strictement plus petites.
Anton Trunov
@boyers Oui, il doit y avoir des choses que vous ne pouvez pas prouver dans Coq, selon le premier théorème de Gödel. En pratique, il est rare de les rencontrer, mais il y a toujours l'argument diagonal: Coq ne peut pas prouver Coq lui-même, il ne peut prouver qu'un sous-ensemble (un très grand sous-ensemble, l'esprit, y compris toutes les fonctionnalités, mais avec une limite inférieure sur la quantité de récursivité il peut gérer). Je me souviens avoir lu que la théorie de Coq est équivalente aux axiomes de Peano plus l'existence d'un certain ordinal grand (et donc les preuves qui supposent un ordinal encore plus grand ne peuvent pas tenir), mais je ne peux pas trouver la référence maintenant.
Gilles 'SO- arrête d'être méchant'
@AntonTrunov Dans ce contexte, Programet similaires sont un hareng rouge. Ils ne changent pas la théorie. Ce qu'ils font, c'est du sucre syntaxique pour utiliser une mesure dans une preuve: plutôt que de raisonner que l'objet qui vous intéresse devient plus petit, vous ajoutez un niveau d'indirection: calculer un autre objet devient plus petit (par exemple une certaine taille) et prouver qu'il devient plus petit. Voir la Wfbibliothèque.
Gilles 'SO- arrête d'être méchant'
@Gilles J'ai supposé que le contexte concernait le côté pratique (concret), comme lorsque l'heuristique de Coq échoue ... Pourriez-vous s'il vous plaît essayer de trouver l'article que vous avez mentionné? Un lien serait très apprécié.
Anton Trunov