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.

Types d'algorithme

Il y a essentiellement deux sortes d'algorithmes :

• de façon itérative, c'est à dire en utilisant des boucles
• de façon récursive, c'est à dire sous la forme d'une fonction qui s'appelle elle même.

Tout problème algorithmique pourra toujours s'écrire sous une forme itérative ou récursive, bien que certains problèmes se résolvent mieux sous une forme qu'une autre.

Avant de définir formellement les deux approches commençons par deux remarques d'importance :

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! = \Pi_{1\leq i \leq n} i = 1 \times 2 \times \dots \times (n-1)\times n $$

Récursif

Pour le calcul de la factorielle, on va commencer par calculer $n!$ en supposant que $(n-1)!$ est connu, $n! = n \times ((n-1)!)$, et en remarquant que l'on connaît $1!$ qui vaut $1$ :

algorithme factorielle(n: entier) → entier:
    si n == 1:
        rendre 1
    rendre n * factorielle(n-1)

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

Itératif

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

algorithme factorielle(n: entier)  → entier:
    r ← 1
    i ← 1
    tant que i ≤ n:
        r ← r * i
        i ← i + 1
    rendre r

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

Preuve

Prouver qu'un programme résout un problème algorithmique nécessite deux vérifications :

• la finitude : le programme s'arrête pour toute entrée, c'est un algorithme
• la correction : sa sortie est une solution du problème

Finitude

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

Un programme itératif est un algorithme s'il n'existe pas de boucle infinie. Ceci n'est possible que pour les boucles tant que :

Correction

Il n'existe pas de schéma général permettant de prouver qu'un algorithme résout un problème donné mais comme l'adaptation aux données d'un algorithme se fait dans les boucles ou les récursions, une méthode qui se révèle souvent efficace consiste à trouver des propriétés qui sont conservées à chaque itération ou récursion.

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.

Mise en application

Nous allons prouver que les deux algorithmes de calcul de factorielle calculent effectivement la factorielle. Cet exemple sera l'occasion de mener à bien deux types de preuves, une par récurrence l'autre pa invariant de boucle.

Algorithme récursif

Les preuves des algorithmes récursifs sont souvent les plus simples car ils sont souvent les plus proches de la définition récursive qu'ils implémentent.

algorithme factorielle(n: entier) → entier:
    si n == 1:
        rendre 1
    rendre n * factorielle(n-1)

Finitude de Factorielle récursif

Si $n\geq 1$ 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 == 1$.

Correction de Factorielle récursif

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

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

Algorithme itératif

Les preuves des algorithmes itératifs nécessitent de trouver les raisons d'être des boucles. Ceci se fait en cherchant ce qui ne va pas varier.

algorithme factorielle(n: entier) → entier:
    r ← 1
    i ← 1
    tant que i ≤ n:
        r ← r * i
        i ← i + 1
    rendre r

Finitude de Factorielle itératif

Comme $i$ va croître strictement : la condition i ≤ n sera fausse à une itération et le programme va s'arrêter.

Correction de Factorielle itératif

Trouver un invariant de boucle peut-être intimidant. Ne le cherchez donc pas tout de suite : commencez par comprendre l'algorithme.

Souvent (toujours ?), c'est dans les boucles que se forme la solution :

1. comprendre l'algorithme c'est comprendre la boucle
2. comprendre la boucle c'est comprendre comment se modifient les variables
3. la modification des variables peut s'exprimer sous la forme d'un invariant

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!$

A vous

L'algorithme suivant est une variante itérative de l'algorithme factoriel :

algorithme factorielle_variante(n: entier):
    r ← 1
    i ← n
    tant que i ≤ n:
        r ← r * i
        i ← i - 1
    rendre r

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

Vous allez démontrer que cet algorithme calcule également la factorielle.

Pour démontrer la correction du l'algorithme, on utilise un invariant de boucle.

Trouver un invariant

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 boucle 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

Ce qu'il faut retenir c'est que trouver l'invariant est à la fin du processus de création de la preuve.

Maximum d'un tableau

On considère l'algorithme itératif suivant :

algorithme maximum(t: [entier]) → entier:
    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

La finitude du programme est clair puisqu'il n'y a qu'une boucle pour chaque. Analysons le programme pour comprendre quel invariant utiliser pour la correction. Reprenons les quatre étapes.

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.

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

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

Voir comment on pourrait prouver l'algorithme

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

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 tableaux (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: [entier]) → entier:
    m ← t[0]
    pour chaque i de [0, t.longueur - 1]:
        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 : à la fin d'une itération, $m$ vaut le maximum des $i+1$ premiers élément du tableau.

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. 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é.

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 tableau, c'est le maximum.

À vous : division euclidienne

Vous trouverez ci-après une version itérative de l'algorithme de la division euclidienne que vous allez prouver par invariant de boucle.

algorithme division_euclidienne(a: entier,
                                b: entier) → [entier]:
    r ← a
    q ← 0
    
    tant que r ≥ b:
        r ← r - b
        q ← q + 1
    
    rendre [q, r]

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

Le retour de notre algorithme est un tableau à deux éléments.

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$. Regardez bien comment fonctionne la boucle de l'algorithme pour garantir ce résultat.