Problème algorithmique et preuve d'algorithme

Un algorithme est censé faire quelque chose : à partir de données passées en entrée (ses paramètres) il va produire une sortie. Cette sortie dépend de ses paramètres et répond à une question ou plus généralement résout un problème. Définissons ceci sous la forme de "problème" à résoudre via un algorithme.

Problème algorithmique

Par exemple :

Comme tout problème n'admet pas forcément un algorithme pour le résoudre (par exemple la complexité de Kolmogorov, "quand est-ce qu'on mange ?" ou encore "le sens de la vie ?"), on se restreindra ici aux problèmes algorithmiques :

Il est clair qu'un problème algorithmique est une propriété, il n'existe donc aucun moyen automatique de savoir si un algorithme donné résout un problème : il faut le prouver à chaque fois.

Preuve d'algorithme

À chaque fois que l'on nous demandera de créer un algorithme pour résoudre un problème il nous faudra :

1. s'assurer que l'on écrit un programme
2. s'assurer que ce programme s'arrête pour toute entrée (et donc que c'est un algorithme)
3. montrer qu'il résout le problème demandé.

Si l'étape 2, prouver qu'un programme s'arrête, fait partie des problèmes indécidables en général, il est souvent facile en pratique de montrer qu'un programme donné est un algorithme. En particulier les algorithmes qui résolvent des problèmes sont censés s'arrêter et il sera (normalement) facile de le voir.

En revanche l'étape 3, la preuve que l'algorithme fait bien ce qu'on attend de lui, est parfois plus délicate. On peut cependant donner des règles générales de preuve qui fonctionnent (souvent) pour des algorithmes récursifs ou itératifs.

Pour expliciter la différence entre les deux approches nous allons utiliser le calcul de la factorielle définie pour tout entier $n\geq 1$ telle que :

$$ n! \coloneqq \prod\limits_{1\leq i \leq n} i = 1 \times 2 \times \dots \times (n-1)\times n $$

Preuve d'algorithmes récursifs

Pour le calcul de la factorielle, si $(n-1)!$ est connu, $n! = n \times ((n-1)!)$, et en remarquant que l'on connaît $1!$ qui vaut $1$, on peut écrire l'équation de récurrence :

Qui permet d'écrire l'algorithme récursif suivant :

algorithme factorielle(n: int     # n ≥ 1
                      ) → int:
    si n == 1:                    # condition d'arrêt
        rendre 1
    ref f ← factorielle(n-1)      # récursion
    rendre n * f

def factorielle(n):
    if n == 1:
        return 1
    f = factorielle(n - 1)
    return n * f

Finitude

Un programme récursif est un algorithme s'il n'existe pas de récursion infinie :

Notre programme factorielle est bien un algorithme puisque la récursion va se rapprocher strictement de sa condition d'arrêt ($n = 1$). On peut le prouver rapidement par récurrence sur $n$.

1. initialisation de la preuve : si $n=1$, l'algorithme va se finir sans exécuter la ligne 4, il y a un nombre fini de récursions.
2. hypothèse de récurrence : pour tout entier plus petit que $n-1\geq 1$, l'algorithme va avoir un nombre fini de récursions.
3. pour $n$ : factorielle(n) va exécuter la ligne 4 (ref f ← factorielle(n-1)) qui, par hypothèse de récurrence, va se terminer au bout d'un nombre fini de récursions : le programme factorielle(n) va également se terminer.

La preuve précédente donne un moyen simple de prouver qu'un algorithme récursif va s'arrêter :

Ceci fonctionne même s'il y a plus d'un appel récursif. On peut donc simplement écrire pour prouver la convergence :

Correction

Ne vous lancez pas dans des démonstrations par récurrence interminables et besogneuses si la récursion est évidente ! Notre algorithme récursif retranscrit directement la définition récurrente de la factorielle, il est donc évidemment correct.

Preuve d'algorithmes itératifs

Pour le calcul de la factorielle, on va commencer par calculer $1!$ puis remarquer que $(n + 1)! = (n!) \cdot (n + 1)$ :

algorithme factorielle(n: int) → int:
    ref r ← 1  # initialisation
    ref i ← 1
    tant que i ≤ n:  # condition d'arrêt
        r ← r * i
        i ← i + 1
    rendre r

def factorielle(n):
    r = 1
    i = 1
    while i <= n:
        r *= i
        i += 1
    return r

On voit que la forme d'un algorithme itératif est inversée par rapport à un algorithme récursif.

Finitude

Un programme itératif est un algorithme s'il n'existe pas de boucle infinie :

Notre algorithme va forcément s'arrêter puisque $i$ croît strictement à chaque itération.

Correction

Démontrer la correction d'un algorithme itératif est souvent plus compliqué que celle d'un algorithme récursif. Une méthode qui se révèle souvent efficace consiste à trouver des propriétés qui sont conservées à chaque itération.

À part les recommandations ci-dessus, il n'existe pas vraiment de règles à appliquer pour prouver un algorithme. Seules l'expérience et l'étude des algorithmes classiques vous permettront de trouver facilement comment prouver un algorithme.

Nous allons montrer les 3 façons de faire avec notre algorithme.

Correction par relation évidente

L'algorithme suivant est une réécriture directe de la version tant que de factorielle précédente :

algorithme factorielle(n: int) → int:  # n ≥ 1
    ref produit ← 1
    pour chaque i de [2 .. n]:
        produit ← produit * i

    rendre produit

La preuve d'exactitude est alors évidente puisque l'on a juste réécrit la définition de $n!$.

Correction par une équation de récurrence

Nous allons montrer que l'on peut prouver notre algorithme par récurrence. Il peut en effet se réécrire de cette façon :

algorithme factorielle(n: int) → int:
    ref r ← 1                 
    ref i ← 1

    tant que i ≤ n - 1:        # boucle de factorielle(n - 1)
        r ← r * i
        i ← i + 1
    
    # ici r et i sont égaux à ceux de la sortie de la boucle de factorielle(n - 1)

    r ← r * i
    i ← i + 1

    rendre r

On retrouve la boucle de factorielle(n-1) dans factorielle(n) ce qui montre que si factorielle(n-1) fonctionne et rend $(n-1)!$ alors factorielle(n) rendra bien $n\cdot (n-1)! = n!$. On est ramené à une preuve par récurrence, comme pour le cas récursif.

Correction par invariant

Lorsque l'on ne peut pas clairement et rapidement faire une preuve par récurrence, on peut chercher un invariant à la boucle : quelque chose qui est conservé à chaque itération. Cette technique de preuve n'est pas très éloignée des preuves par récurrence, elle est juste plus générale et (de l'avis des informaticiens) plus élégante.

Refaisons la preuve précédente en utilisant un invariant de boucle pour montrer comment tout ceci peut se faire :

algorithme factorielle(n: int) → int:
    ref r ← 1
    ref i ← 1

    tant que i ≤ n:
        r ← r * i
        i ← i + 1
    rendre r

Un invariant possible est :

L'invariant étant vérifié à la fin de chaque itération, il est donc aussi vrai à la fin de la dernière itération. À ce moment-là on a $i=n+1$ et donc $r = n!$ : notre algorithme calcule bien la factorielle de son entrée.

Trouver des invariants de boucles

Trouver un invariant de boucle est souvent intimidant pour des débutants. Nous allons nous entraîner un peu pour acquérir quelques automatismes. L'idée principale pour trouver un invariant est de procéder par étapes :

1. comprendre l'algorithme
2. comprendre l'intérêt de la boucle le constituant (s'il y a plusieurs boucles on refait l'analyse pour chaque boucle)
3. voir comment on pourrait prouver l'algorithme
4. utiliser cette idée de preuve pour créer un invariant
5. prouver l'invariant
6. prouver la correction de l'algorithme

Appliquons ces recommandations sur l'algorithme itératif suivant :

algorithme maximum(t: []int) → int:
    ref m ← t[0]
    pour chaque x de t:
        si m < x:
            m ← x
    rendre m

def maximum(t):
    m = t[0]
    for x in t:
        if m < x:
            m = x
    return m

1. Comprendre l'algorithme

L'algorithme va itérer sur chaque élément du tableau et conserver dans la variable m la plus grande des valeurs vues jusqu'à présent.

2. Comprendre l'intérêt de la boucle le constituant (s'il y a plusieurs boucles on refait l'analyse pour chaque boucle)

Il faut parcourir tous les éléments du tableau pour connaître la plus grande des valeurs.

3. Voir comment on pourrait prouver l'algorithme

Il faut montrer que la variable m contient la valeur maximale pour tous les éléments de t vus jusqu'à présent. Comme à la fin de l'algorithme on aura vu toutes les valeurs de t on aura prouvé que m est bien le maximum.

4. Utiliser cette idée de preuve pour créer un invariant

Notre invariant doit lier, à la $i$ème itération, $m$ aux $i$ premiers éléments du tableau (il vaut le maximum). Pour que cela fonctionne facilement il faut pouvoir expliciter le numéro de l'itération actuelle de la boucle pour chaque. On modifie alors notre algorithme pour rendre $i$ explicite :

algorithme maximum(t: []int) → int:
    ref m ← t[0]
    ref x int
    pour chaque i de [0 .. t.longueur[:
        x ← t[i]
        si m < x:
            m ← x
    rendre m

def maximum(t):
    m = t[0]
    for i in range(len(t)):
        x = t[i]
        if m < x:
            m = x
    return m

Ce qui permet d'écrire l'invariant :

Invariant de boucle : à la fin d'une itération, $m$ vaut le maximum des $i+1$ premiers éléments du tableau.

5. Prouver l'invariant

Après la première itération de la boucle, comme $m$ vaut initialement le premier élément du tableau, on a que $m=t[0]$ qui est bien le maximum des $0+1=1$ premiers éléments du tableau. L'invariant est vérifié à la fin de la première itération où $i=0$.

On suppose l'invariant vrai à la fin d'une itération. À la fin de l'itération suivante, $m'$ (la valeur de $m$ à l'issue de cette itération) vaut soit $m$ (la valeur de $m$ au début de l'itération) soit $x'=t[i']$ ($i'$ étant la valeur de $i$ pour cette nouvelle itération). Comme $i' = i+1$ et que l'invariant est vrai à la fin de l'itération précédente :

• $m$ vaut le maximum du tableau sur les $i+1$ premiers éléments (hypothèse de récurrence)
• $m' = \max(m, x') = \max(m, t[i']) = \max(m, t[i + 1])$ (ce qui se passe dans l'itération suivante)

On en conclut que $m'$ vaut bien le maximum du tableau sur les $i + 2$ premiers éléments.

Notre invariant est vérifié.

6. Prouver la correction de l'algorithme

Cette partie-là est facile si on a le bon invariant. Il suffit de regarder la valeur de l'invariant à la fin de la boucle. Dans notre cas $m$ vaut le maximum de tous les éléments du tableau, c'est le maximum.