Non terminaison et indécidabilité
Par David Monniaux le mercredi, mai 30 2012, 11:15 - Théorie - Lien permanent
Considérons le problème suivant : étant donné une logique L permettant d'exprimer l'arithmétique, est-ce que pour tout programme qui ne termine pas sur l'entrée vide, on peut exhiber une preuve de ce fait dans L ? (Pour préciser la question : à tout programme on peut associer une formule Σ1 de l'arithmétique, exprimant qu'il termine, par exemple par la construction de Cook dans son théorème de complétude relative de la logique de Hoare à coup de codage de Gödel. Il s'agit de prouver cette formule.)
La réponse est négative (sauf délire de ma part) : il existe des programmes qui ne terminent pas, mais L n'arrive pas à prouver cela car il existe des modèles non standards de L où il y a un témoin de terminaison (une instanciation des quantificateurs existentiels).
Bien entendu, on peut toujours concocter des modèles, mais existe-t-il un exemple raisonnable de programme (à part un programme qui énumère des preuves..) qui produit cela ? Ceci rejoint un domaine de recherche : pondre des problèmes indécidables dans Peano sans avoir recours à la théorie de la preuve... il me semble avoir vu un exemple de suite dont le passage à zéro (donc la terminaison du programme associé) est dans ce cas.
Commentaires
Ce n'est pas mon domaine d'expertise, mais il doit y avoir un problème de formulation dans ton premier paragraphe : si le programme termine sur une entrée fixée, on doit bien pouvoir dérouler étape par étape le déroulement de l'exécution du programme pour fabriquer une démonstration du fait qu'il termine, non ?
Le chapitre 4.10 des lecture notes de
http://users.utu.fi/jkari/automata/
répondent peut-être à la question.
(Prouver que la logique du premier ordre est non récursive grâce au Post Correspondence Problem puis en déduire Gödel.)
@Joël
En simplifiant, si une machine de Turing s'arrête, il existe une preuve qu'elle s'arrête (il suffit en effet de faire la trace).
Mais si elle ne s'arrête pas, il peut aussi y avoir une preuve du non-arrêt (boucle évidente, énumération des entiers, etc...). Hélas, ce n'est pas systématique.
@Joel: Heu oui je me suis emmêlé dans les négations.
S'il termine, il existe une preuve de cela (il suffit de dérouler) mais s'il ne termine pas, tu peux ne pas arriver à faire une preuve dans L parce que la formule qui qu'il termine est vraie dans un modèle non standard (ce qui veut dire que tu as un objet dans ce modèle qui représente le nombre d'itérations du calcul, mais qui ne s'obtient pas comme successeur de successeur de ... successeur de zéro).
@abcd: Ce genre de manips, je connais. Avec la construction de Cook / codage de Gödel dont je parlais, il y a une caractérisation par une formule arithmétique du premier ordre des programmes qui terminent. Prenons une logique L consistante (ou peut-être faut-il ω-consistante, j'ai la flemme) exprimant l'arithmétique et avec un ensemble d'axiomes récursivement énumérable. On peut énumérer ses théorèmes. Si L n'a pas d'énoncés indécidables, alors tout énoncé ou son contraire a une preuve dans L. Pour savoir si un programme termine, il suffirait alors d'énumérer tous les théorèmes de L et de chercher si on tombe sur une preuve de terminaison ou son contraire. Ceci fournirait une procédure de décision pour le problème de l'arrêt, donc il existe forcément des énoncés indécidables (d'où une forme faible du premier théorème d'incomplétude de Gödel).
Si ça termine, alors il existe une preuve par simple déroulement, donc les seuls cas d'indécidabilité sont des preuves de non-terminaison.
Pour le même genre de raisons, il existe des programmes (du style celui qui énumère les théorèmes jusqu'à tomber sur un certain théorème T) n'ayant pas de preuve de non-terminaison dans L. Ce que je soulève comme problème, c'est que cette construction a quelque chose d'artificiel : on regarde des programmes qui font de la théorie de la preuve. Bref, je réclame un programme assez « naturel » dont on n'aurait pas de preuve dans Peano. Pour le moment, le mieux que j'ai vu en la matière est une suite récurrente et calculable algorithmiquement dont on peut prouver en théorie des ensembles et à coups d'ordinaux qu'elle finira par s'annuler quelle que soit sa valeur initiale, alors que c'est non démontrable en Peano.
Flemme de rentrer dans les details, mais est-ce que c'est vraiment genant que ca ne soit pas "naturel" ?
Parce que l'air de rien, vu qu'on n'a toujours pas de generateur-de-code-qui-marche automatique, a peu pres tous les outils que tu peux rever d'analyse et d'introspection tombent vite dans du non decidable...
@Marc: Si des raisons d'impossibilité font « artificiel », c'est peut-être que les vrais programmes vérifient certains critères de simplicité (non encore identifiés) qui font que certains pires cas ne se produisent pas.
Par exemple, même si le voyageur de commerce est NP-complet, on le résout bien sur les instances pratiques, sans doute parce que les instances obtenues par réduction des problèmes NP-complets classiques sont « artificielles ».
Mouais bof... a cote de ca, les cas pathologiques reels, ca existe ! je n'ai pas d'exemple simple a expliquer sous la main, mais j'en rencontre regulierement, et c'est presque toujours dans du logiciel qui avait gere "le cas simple" et hop, on rencontre un cas plus complexe et non gere en pratique.
Et pour le voyageur de commerce, le fait de savoir qu'on a affaire au voyageur de commerce est la premiere etape pour chercher une alternative "moins couteuse" souvent.
Peut-etre que la vraie difficulte, c'est de savoir quelles batailles on peut gagner ? faudrait faire un outil pour ca. Ah zut, on sait deja que c'est perdu d'avance et que ca va etre indecidable... ;)
Ta question est, en fait, de savoir s'il existe des énoncés Π_1 de l'arithmétique qui soient à la fois « naturels », vrais, et indémontrables dans Peano. (« Naturels » au sens que leur construction ne fait pas appel à des preuves dans Peano ; sans cette condition, on a une réponse évidente, c'est Consis(Peano), et la machine de Turing correspondante — qui ne s'arrête pas mais dont Peano ne prouve pas ce fait — est celle qui énumère les démonstrations dans Peano et s'arrête si elle trouve une preuve de 0=1 ; tu cherches, donc, quelque chose de plus naturel.)
En un certain sens, je pense que la réponse est non. On a certes des façons de produire des énoncés arithmétiques « naturels », vrais et indémontrables dans Peano, voir par exemple les théorèmes de Paris-Harrington et Paris-Kirby, mais ce sont à chaque fois des énoncés Π_2 alors que tu veux du Π_1 (autrement dit, tu veux une machine de Turing « naturelle » qui ne s'arrête pas et dont Peano ne prouve pas ce fait, alors que ce qui est facile c'est de faire une machine de Peano qui s'arrête pour tout entier mais dont Peano ne prouve pas ce fait — il le prouve pour tout entier donné, bien sûr, mais pas globalement). Et je pense qu'il y a une raison à ça, c'est que tous ces énoncés proviennent de machinerie de la théorie de la démonstration qui produit des principes combinatoires équivalents au fait que certains ordinaux sont bien des ordinaux (typiquement, ces énoncés sont tous du style « ε_0 est bien un ordinal » sous différents déguisements), et ça ce sont forcément des énoncés Π_2. Donc je n'y crois pas trop.
En revanche, on peut toujours tricher. Je peux appliquer le théorème de Matiâsevič-Davis-Robinson-Putnam et trouver une équation diophantienne P=0 (où P est un polynôme en k variables entières) telle que l'existence d'une solution soit équivalente (et démontrablement dans une arithmétique faible) à l'existence d'une preuve de 0=1 dans Peano : alors P=0 n'a pas de solution, mais Peano ne prouve pas ce fait, et si j'écris une machine de Turing qui teste successivement tous les k-uplets de variables et calcule P dessus et s'arrête si elle trouve une solution, cette machine ne s'arrête jamais, mais Peano ne peut pas le prouver. Le théorème de Matiâsevič-Davis-Robinson-Putnam étant constructif, je peux (avec une certaine patience) construire explicitement ce polynôme P. C'est de la triche, parce que la machine de Turing est « en fait » en train de chercher des preuves de 0=1 dans Peano ; mais toi tu ne le sais pas forcément, tu vois juste que la machine calcule les valeurs d'un certain polynôme, et on peut prouver (dans ZFC, ou simplement dans Peano+Consis(Peano)) qu'elle ne s'arrête pas mais que Peano ne peut pas prouver ce fait.
DMx, c'est *mal* d'invoquer Ruxor comme ca.
Maintenant va falloir faire une offrande pour le calmer.