Récurrence et correction algorithmique

1. Preuve de Correction des Algorithmes Récursifs

Prouver la correction d'une fonction récursive f(n) revient presque toujours à effectuer une preuve par récurrence sur le paramètre n. La propriété P(n) que l'on cherche à démontrer est généralement : "la fonction f(n) termine et renvoie la valeur correcte".

La structure de la preuve est celle que vous connaissez :

1. Cas de base (Initialisation) : Montrer que P(n_0) est vraie, où n_0 est le cas d'arrêt de la récursion. On vérifie que pour cette valeur, la fonction termine et renvoie le bon résultat.
2. Hérédité : Supposer que la propriété est vraie pour n-1 (récurrence simple) ou pour tous les k < n (récurrence forte). Ensuite, montrer que sous cette hypothèse, f(n) termine (car elle fait un appel sur une valeur plus petite) et que le résultat qu'elle calcule à partir de l'appel récursif est correct.

L'exemple le plus canonique est celui de la fonction factorielle.

Pour une formulation en français et parfaitement rigoureuse, vous pouvez consulter l'exercice 6 du document "Rappels : Preuves des algorithmes", qui formalise la même preuve pour la fonction factorielle(n).

2. Preuve de Correction des Algorithmes Itératifs : L'Invariant de Boucle

Comment appliquer un raisonnement par récurrence à une boucle while ? L'induction se fait sur le nombre de passages dans la boucle. Pour formaliser cela, on introduit la notion d'invariant de boucle.

Un invariant de boucle est une propriété des variables de l'algorithme qui est :

1. Vraie avant d'entrer dans la boucle.
2. Reste vraie après chaque itération.
3. Lorsque la boucle se termine, la propriété (jointe à la condition d'arrêt de la boucle) implique que l'algorithme a produit le résultat attendu.

Ceci établit une analogie parfaite avec la récurrence :

La preuve de correction à l'aide d'un invariant se déroule en trois temps :

• Initialisation : Démontrer que l'invariant est vrai avant la première itération de la boucle. (Le cas de base de notre récurrence)
• Conservation (Hérédité) : Démontrer que si l'invariant est vrai au début d'une itération, il le reste à la fin de cette itération. (L'étape d'hérédité)
• Conclusion : Démontrer que lorsque la boucle termine (c'est-à-dire que sa condition devient fausse), l'invariant implique la correction de l'algorithme.

Notez qu'un invariant ne prouve que la correction partielle : si l'algorithme termine, le résultat est correct. Pour prouver la correction totale, il faut aussi prouver la terminaison, ce qui se fait généralement en exhibant un variant de boucle : une quantité entière positive qui décroît strictement à chaque itération.

La vidéo suivante met en œuvre cette méthode de A à Z sur un exemple simple.

3. Application : L'Algorithme d'Euclide

Mettons maintenant en pratique cette méthode sur un algorithme fondamental que vous connaissez bien : l'algorithme d'Euclide pour le calcul du plus grand commun diviseur (PGCD).

Considérez l'algorithme suivant pour calculer le PGCD de deux entiers naturels a et b.

fonction euclide(a, b):
  x ← a
  y ← b
  tant que y ≠ 0 faire
    r ← x mod y
    x ← y
    y ← r
  retourner x

Votre tâche est de prouver sa correction totale.

1. Preuve de terminaison (Variant de boucle)

Pouvez-vous identifier une quantité qui est un entier, reste positive et décroît strictement à chaque itération ?

2. Preuve de correction partielle (Invariant de boucle)

L'étape la plus difficile est de trouver le bon invariant. L'invariant doit capturer l'essence de l'algorithme. Ici, l'algorithme d'Euclide repose sur la propriété que $\text{pgcd}(x,y)=\text{pgcd}(y,x(\mathrm{mod}y))$.

Quel invariant reliant x, y aux entrées initiales a, b pourrait-on utiliser ?

Maintenant, essayez de dérouler les trois étapes de la preuve.

Conclusion

Félicitations, vous avez maintenant une méthode systématique pour aborder la preuve de correction des deux grandes familles d'algorithmes. Cette compétence est absolument centrale.

À retenir :

• Algorithmes récursifs : La correction se prouve par récurrence (simple ou forte) sur le paramètre de la récursion. La propriété P(n) englobe à la fois la terminaison et la validité du résultat.
• Algorithmes itératifs : La correction se prouve via un invariant de boucle, qui est lui-même une forme de raisonnement par récurrence sur le nombre d'itérations.
• Une preuve par invariant comporte trois étapes cruciales : Initialisation, Conservation, Conclusion.
• Pour une preuve de correction totale d'un algorithme itératif, il faut également prouver la terminaison à l'aide d'un variant de boucle.

Nous avons achevé notre premier module sur la logique et les méthodes de preuve. Vous disposez désormais des outils formels pour raisonner de manière rigoureuse sur les algorithmes. Dans le prochain module, nous aborderons les Mathématiques Discrètes pour l'Informatique, en commençant par les techniques de dénombrement et de combinatoire, qui sont indispensables pour analyser la complexité de nombreux algorithmes et structures de données.