Preuves de programme

À la fin de la partie du cours concernant la récursivité, on a énoncé les vérifications minimum à faire lorsqu'on écrit une fonction récursive, à savoir :

1.

Vérifier qu'on a un critère d'arrêt et qu'on renvoie la bonne solution pour la taille minimale du problème

2.

Vérifier qu'on fait bien tendre le problème vers la solution triviale, i.e. qu'on atteindra bien le critère d'arrêt

3.

Vérifier la cohérence du nombre d'arguments et du type des expressions lors de l'appel récursif

Nous avons vu aussi que la définition de fonctions récursives est liée au principe de récurrence. C'est aussi ce principe que l'on va utiliser pour raisonner sur des fonctions récursives.

17. Principe général

Étant donnée une fonction récursive f dont le résultat doit vérifier une propriété P, soit n la taille qui caractérise le problème à résoudre (par exemple la longueur de la liste pour une fonction manipulant une liste).

Supposons, sans perte de généralité, que la plus petite taille du problème est 0 et notons f(n) le résultat de la fonction f pour le problème à la taille n.

Les preuves de la correction et de l'arrêt de f se font de la manière suivante :

Correction :

Prouver que le résultat f(0) vérifie la propriété P.

Prouver que si le résultat f(n-1) vérifie la propriété P alors le résultat f(n) la vérifie aussi.

Le principe de récurrence nous permet alors de dire que la propriété P est vraie pour toutes les tailles.

Arrêt :

Prouver que le calcul de f(0) se termine.

Prouver que si le calcul de f(n-1) se termine alors le calcul de f(n) se termine.

18. Étude d'un cas

Considérons le problème suivant : étant donnés une liste L de nombres triée en ordre croissant, et un nombre e, on veut écrire une fonction qui insère e dans L à sa place, c'est à dire telle que le résultat soit une liste triée en ordre croissant.

On propose la fonction suivante :

         (define insere 
            (lambda (e L)
               (cond ((null? L) (liste e))
                     ((<= e (car L)) (cons e L))
                     (else (cons (car L) (insere e (cdr L)))) )))

On va montrer que cette fonction se termine et qu'elle rend bien le résultat voulu. Pour cela nous raisonnerons par récurrence sur la longueur de la liste dans laquelle on insère un élément.

18.1 Preuve de l'arrêt

1.

Montrons que la fonction se termine si L est une liste de longueur nulle.

Si L est une liste vide alors le calcul de (insere e '()) se résume à l'évaluation de l'expression (cons e l) qui se termine.

2.

Supposons maintenant que, pour $n\geqslant 1$, le calcul de (insere e L) se termine pour toute liste de longueur n-1 et montrons alors qu'il se termine pour toute liste de longueur n.

Deux cas se présentent :

a)

soit e est plus petit que le premier élément de L et dans ce cas, le résultat est donné par l'évaluation de (cons e L) qui se termine

b)

soit e est plus grand que le premier élément, et dans ce cas le calcul revient à évaluer l'expression (cons (car L) (insere e (cdr L)). Dans cette expression, la liste (cdr L) est de longueur n-1, donc par hypothèse l'appel (insere e (cdr L)) se termine.

On a ainsi montré que, quelque soit la longueur de la liste L, la fonction insere s'arrête.

18.2 Preuve de la correction

La propriété que la fonction doit vérifier est la suivante : <<le résultat de (insere e L) doit être une liste triée en ordre croissant et à laquelle appartient e.>>.

Plus précisément, étant donnée une liste $L=(e_1\ldots e_n)$ de longueur n et une entier e:

Pt :   L est triée en ordre croissant ssi $\forall i=1 .. n-1\quad e_i\leqslant e_{i+1}$

Pe :   e est élément de l ssi $\exists i, 1\leqslant i\leqslant n \mbox{ tel que } e_i=e$

Il faut donc montrer que (insere e L) vérifie Pt et Pe, quelque soit la liste L.

1.

Montrons que si L est de longueur nulle alors (insere e L) vérifie Pt et Pe.

Si L est de longueur nulle alors L est la liste vide et le résultat de (insere e '()) est la liste (e) qui, de manière évidente, est triée en ordre croissant et contient e.

2.

Étant donné $n\geqslant 1$, supposons que pour toute liste L de longueur n-1, (insere e L) vérifie les propriétés Pt et Pe.

Soit $L=(e_1\ldots e_n)$ une liste triée en ordre croissant de longueur n. Pour le calcul de (insere e L)1, deux cas se présentent :

a)

si $e\leqslant e_1$ alors le résultat de (insere e L) est le résultat de (cons e l) c'est à dire la liste $(e\, e_1 ... e_n)$ qui contient bien l'élément e et qui est triée en ordre croissant puisque $(e_1 \ldots e_n)$ est triée et $e\leqslant e_1$.

b)

si e > e₁ alors le résultat est donné par l'évaluation de (cons (car L) (insere e (cdr L))). Appelons L' ce résultat.

(cdr L) étant une liste de longueur n-1, par hypothèse e appartient à la liste (insere e (cdr L)) et a fortiori à la liste L'. La propriété Pe est bien vérifiée.

Il faut encore vérifier que L' est triée en ordre croissant.

Le résultat de (insere e (cdr L)) s'écrit:

-

soit $(e\, e_2 \ldots e_n)$ si $e \leqslant e_2$

-

soit $(e_2 \ldots e\ldots e_n)$ si e > e₂

Dans le premier cas, on a alors $L'=(e_1\, e\, e_2 \ldots e_n)$. Comme $e_1\leqslant e$ et que par hypothèse la liste $(e\, e_2 \ldots e_n)$ est triée en ordre croissant, la liste L' est donc triée.

Dans le second cas, par hypothèse la liste $(e_2 \ldots e\ldots e_n)$ est triée en ordre croissant et comme $L=(e_1\, e_2 \ldots e_n)$ est triée, on a $e_1 \leqslant e_2$ donc la liste L' est triée en ordre croissant.

On a donc montré que si le résultat de la fonction insere vérifie les propriétés Pe et Pt pour toute liste de longueur n-1 alors elle les vérifie pour toute liste de longueur n.

Cela clos la démonstration par récurrence sur la longueur de la liste L de la correction de la fonction insere.

19. Indécidabilité du problème de l'arrêt

Le problème de l'arrêt a été posé par Alan Turing en 1936; on peut l'énoncer de la manière suivante :

Faisons l'hypothèse qu'on peut programmer un tel prédicat.

Et définissons les fonctions :

      (define boucle
         (lambda () (boucle)))

      (define test 
         (lambda (f)
            (if (arret? f f)
                (boucle)
                1)))

Considérons alors l'appel : (test test)

-

si l'évaluation de (test test) se termine,
alors par définition du prédicat arret?, (arret? test test) rend vrai
et l'évaluation de (test test) revient à évaluer (boucle) qui ne se termine pas.

Il y a donc contradiction.

-

et si (test test) ne se termine pas,
alors (arret test test) rend faux
et l'évaluation de (test test) rend 1 donc (test test) se termine.

Il y a encore contradiction.

Dans les deux cas, on aboutit à une contradiction, ce qui montre que l'hypothèse de départ est fausse.

Que penser de la définition suivante ?

      (define arret? 
         (lambda (f n)
            (if (number? (f n))
                #t
                #f)))