Mes lecteurs le savent peut être : je fais une fixette sur les invariants inductifs polyédriques et notamment la décidabilité de leur existence. Je vais donc tenter d'expliquer ceci en termes assez simples.

Les programmes informatiques ont (dans certaines limites mais cela nous entraînerait loin) un comportement mathématiquement défini.

On peut donc envisager de prouver mathématiquement qu'un programme fait bien ce qu'il est censé faire. On a d'un côté le programme, de l'autre la définition mathématique de ce qu'il doit faire, et on prouve un théorème.

Malheureusement, on sait depuis Alan Turing (avant l'invention des ordinateurs) que la recherche de cette preuve est difficile. Plus précisément, on montre qu'il n'existe pas de méthode automatique qui permette de la trouver à coup sûr si le théorème est vrai. Il s'agit d'une impossibilité mathématique fondamentale et non d'une faiblesse de l'état de l'art scientifique.

On peut en revanche se poser la question de l'existence d'une preuve dans une certaine classe de preuves. Autrement dit, on va se restreindre aux preuves ayant une certaine forme. Bien entendu, un théorème peut admettre une preuve mais aucune de la forme considérée !

Pour certaines classes de preuves, il existe un algorithme (une méthode automatique) qui dira si une preuve existe ou non dedans.

Pour d'autres classes de preuve, on montre qu'il n'existe pas d'algorithme.

Pour d'autres encore, par exemple les polyèdres convexes et pour une certaine classe de programmes (transitions d'arithmétique linéaire réelle), on ne sait pas à ma connaissance et c'est là ma fixette. J'ai essayé de montrer sans succès qu'il n'y a pas d'algorithme (j'y arrive mais avec des hypothèses changées, j'ai besoin d'au moins une transition non linéaire).

Une telle démonstration d'absence de véritable algorithme permettrait de justifier près de 40 ans de recherches sur des méthodes heuristiques, qui, même si une preuve existe dans la classe considérée, ne sont pas assurées de la trouver.

Et même pour les classes de preuves où il y a un algorithme de recherche, se pose la question de son coût. Parce que quand le coût d'un algorithme double à chaque fois qu'on augmente la taille du problème d'entrée de 1, très vite il devient prohibitif.

PS : Dans une optique delenda est Carthago, je me demande si je ne vais pas caser ce problème ouvert à la fin de chaque exposé que je fais et qui a vaguement un rapport. Un jour, quelqu'un de plus sérieux que moi s'y mettra bien !

PS² : En pratique, ça donne chez moi : médite, gratte gratte sur papier, médite, « oh flûte ».