Prouver un algorithme

Le but d'un algorithme est de résoudre un problème algorithmique. Prouver un algorithme signifie qu'il fait bien ce qu'il est sensé faire :

A chaque fois que l'on nous de 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écidable 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 sensé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. Le problème étant souvent (toujours ?) concentré dans les boucles ou les récursions de l'algorithme, on cherchera à trouver des propriétés qui sont conservées avant et après une itération ou une récursion ce qui permet de caractériser formellement à quoi elle sert :

Notez que bien souvent prouver un algorithme et le créer est la même chose. Comprendre comment on peut résoudre un problème donné nous donnera l'algorithme et réciproquement.

A part la recommandation ci-dessus, il n'existe pas vraiment de règles à appliquer pour prouver un algorithme. Seule l'expérience et l'étude des algorithmes classiques vous permettra de trouver facilement comment prouver un algorithme.

Factorielle

Algorithme récursif

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

Finitude

Si $n$ est un entier, l'algorithme précédent va s'arrêter car $n$ décroît strictement de 1 à chaque appelle récursif et on stoppe si $n \leq 1$.

Preuve

Par récurrence sur $n$, avec $n$ entier positif.

Pour $n \leq 1$ factorielle(0) et factorielle(1) valent bien bien $1 = 0! = 1!$. On suppose notre hypothèse de récurrence vraie pour $n-1 \geq 1$. Pour $n > 1$, le retour de factorielle(n) est n * factorielle(n-1) qui vaut donc $n \cdot (n-1)! = n!$ par hypothèse de récurrence.

Algorithme itératif

On va voir ici 2 versions du même algorithme. L'un qui construit la factorielle en montant, et l'autre qui la construit en descendant. On prouvera ces 2 algorithmes en utilisant des invariants de boucles :

Un invariant doit résumer ce que fait la boucle avec une équation qui est toujours vérifiées, même si on modifie des variables.

Première version

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

Finitude

Si $n$ est un entier non nul, l'algorithme va s'arrêter car l'entier $i$ croît strictement de 1 à chaque itération de la boucle while.

Preuve

Par invariant de boucle !

Allons-y :

1. l'algorithme retourne $r$ à la fin : ce doit donc être le résultat et il doit valoir $n!$
2. $r$ est multiplié par $i$ à chaque itération
3. $i$ est incrémenté de 1 à chaque itération et commence à 1.

On doit donc avoir un invariant du type $r \simeq i!$ à la fin de chaque itération à plus ou moins 1 près. Pour en être sur regardons ce que valent nos variables à la fin de la première itération :

• $r = 1$
• $i = 2$ (on a modifié $i$ après l'avoir multiplié par $r$)

Notre invariant doit donc être :

Invariant : $r = (i-1)!$ à la fin de chaque itération.

1. c'est vrai à la fin de la 1ère itération (on a tout fait pour)
2. si c'est vrai à la fin de la $k$ème itération, à la fin de la $k+1$ème itération on a :
   • $r'=r \cdot i$ (le $r$ de la fin de la $k+1$ème boucle est égal à celui de la fin de la $k$ème boucle fois le $i$ de la fin de $k$ème boucle)
   • $i' = i + 1$ (le $i$ de la fin de la $k+1$ème boucle est le $i$ de la fin de la $k$ème boucle plus 1)
   • $r = (i-1)!$ (c'est notre invariant, vrai à la fin de l'itération $k$ ar hypothèse)
3. on a donc : $r' = (i-1)! \cdot i = i! = (i'-1)!$ : notre invariant est vérifié.

L'invariant étant vérifié à la fin de chaque itération, il est donc aussi vrai à la fin de la dernière itération. A ce moment là, on a $i=n+1$ et donc $r = n!$

Seconde version

def factorielle(n):
    r = 1
    i = n
    while i > 1:
        r *= i
        i -= 1
    return r

Finitude

Si $n$ est un entier non nul, l'algorithme va s'arrêter car $n$ décroît strictement à chaque itération de la boucle while.

Preuve

par invariant de boucle (et oui).

Maximum d'un tableau

On va voir 2 algorithmes pour calculer la valeur maximum d'un tableau de réels.

Algorithme récursif

def maximum(tab):
    if len(tab) == 1:
        return tab[0]
    x = maximum(tab[1:])
    if tab[0] > x
        return tab[0]
    else:
        return x

Finitude

À chaque récursion, la taille du tableau diminue strictement. La récursion s'arrêtera donc forcément lorsque le tableau sera de taille 1.

Preuve

Par récurrence sur la longueur d'un tableau. On vérifie que l'algorithme fonctionne pour une longueur de tableau valant 1, puis on effectue preuve par récurrence sur la longueur du tableau.

Algorithme itératif

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

Finitude

Clair car une unique boucle for.

Preuve

Par invariant de boucle.

Pour trouver l'invariant, on remarque que si $t'$ est le tableau des $n-1$ premiers éléments de $t$ (t'= t[:-1]), l'algorithme va :

1. faire exactement pareil que pour $t'$
2. vérifiera $m$ avec le dernier élément de $t$.

Notre invariant doit donc lier les $i$ premiers éléments du tableaux à la $i$ème itération : $m$ doit être le plus grand éléments des $i$ premiers éléments du tableaux pour que notre algorithme puisse fonctionner et avec $t'$ et avec $t$.

Lorsque l'on étudie des algorithmes avec des boucles for il est parfois plus simple d'exhiber directement le nombre d'itérations pour formaliser l'invariant. On utilise alors l'algorithme suivant (qui est strictement équivalent à l'algorithme maximum) :

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

L'invariant est alors :

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

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. A 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 qu'il 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é.

L'invariant est donc aussi vrai à la fin des itérations : $m$ vaut le maximum du tableau à la fin de la boucle for : $m$ est le maximum des valeurs du tableau.

Division euclidienne

Prouvons l'algorithme de la division euclidienne ci-après :

def division_euclidienne(a, b):
    r = a
    q = 0
    while r >= b:
        r -= b
        q += 1
    return (q, r)

Finitude

le programme s'arrête ? : Oui si a et b sont des entiers positifs. Car

• r est un entier
• r après une itération est strictement plus petit que le r avant itération
• on s'arrête si r est strictement plus petit que b.

Preuve

On veut montrer que l'on obtient bien une division euclidienne de $a$ par $b$. C'est à dire que $a = bq + r$ avec $r < b$. Pour cela on va s'aider de l'invariant de boucle :

Invariant : a = r + q * b

Prouvons l'invariant :

1. l'invariant est bien vrai à la fin de la première boucle puisque $q=1$ et $r=a-b$ à ce moment là.
2. on doit prouver que a' = r' + q' * b' à la fin de la $i+1$ème itération.
3. si l'on est passé dans la boucle on a a'=a, r' = r - b, b' = b et q' = q + 1
4. donc r' + q' * b' = r-b + (q+1) * b = r + q * b = a = a' puisque l'invariant est vrai à la fin de la $i$ème itération. On a bien a' = r' + q' * b', l'invariant est démontré.

L'invariant étant juste tout le temps, il l'est en particulier à l'issue de la dernière boucle. A ce moment là on a a = r + qb avec r < b ce qui est bien ce qu'il fallait démontrer.