Projet : Écrire et prouver des algorithmes itératifs et récursifs

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

$i$ est un nombre qui décroît de 1 à chaque itération : à une itération il sera forcément plus petit ou égal à 1.

1. à la fin de la première itération $i = n - 1$ et $r = n = (i+1)$ : notre invariant est vérifié.
2. on suppose la propriété vraie à la fin de la $k$ème itération. À la fin de l'itération suivante 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 moins 1)
   • $r = (i+1) \cdot \dots n$ (c'est notre invariant, vrai à la fin de l'itération $k$ par hypothèse)
3. on a donc : $r' = ((i+1) \cdot \dots \cdot n) \cdot (i) = i \cdot \dots \cdot n = (i'+1) \cdot \dots \cdot n = \frac{n!}{i'!}$ : 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. À ce moment-là, on a $i=1$ et donc $r = 1 \cdot 2 \cdot \dots \cdot n = n!$

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

Le retour de la fonction python est un tuple à 2 éléments (c'est-à-dire un tableau à 2 éléments que l'on ne peut pas modifier).

Si a et b sont des entiers positifs le programme s'arrête 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.

Invariant de boucle : 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. À ce moment-là on a a = r + qb avec r < b ce qui est bien ce qu'il fallait démontrer.

L'algorithme rend le nombre de fois où x est présent dans T

algorithme nombre(T: []int, x: int) → int:
    ref nb ← 0

    pour chaque e de T:
        si e == x:
            nb ← nb + 1
    rendre nb

La finitude est claire puisqu'on a une unique boucle pour chaque qui a forcément un nombre fini d'itérations. On peut très bien dire que l'exactitude est claire aussi puisque l'on parcourt chaque valeur de T, mais si on veut être plus explicite on peut remarquer que :

• nombre(T, x) = nombre(T[:-1], x) + 1 si T[-1] == x,
• nombre(T, x) = nombre(T[:-1], x) si T[-1] ≠ x.

Et conclure avec une récurrence triviale sur la longueur du tableau.

algorithme maximum_rec(T: []float, n: int) → int:
    ref x int

    si n == 0:
        rendre T[0]
    sinon:
        x ← maximum_rec(T, n-1)
        si t[x] > t[n]:
            rendre x
        sinon:
            rendre n

Le paramètre n est un entier qui diminue strictement. Il sera donc à un moment égal à 0 ce qui stoppera la récursion.

La correction se fait par récurrence sur n allant de n = 0 à n = T.longueur - 1.

1. initialisation : pour n = 0, le résultat est clair.
2. hypothèse de récurrence : on suppose que l'algorithme fonctionne pour n - 1
3. preuve pour n - 1. Si l'algorithme fonctionne pour n - 1, x contient l'indice max des indices allant de 0 à n - 1 et on rend x si T[x] > T[n] et n sinon : on rend bien l'indice de la valeur maximale du tableau.

algorithme maximum(T: []int) → int
    rendre maximum_rec(t, T.longueur - 1)


fonction maximum_rec(T: []float, n: int) → int:
    ref x int

    si n == 0:
        rendre T[0]
    sinon:
        x ← maximum_rec(T, n-1)
        si t[x] > t[n]:
            rendre x
        sinon:
            rendre n

algorithme concaténation(début: []int, fin: []int) → []int
    ref T ← [longueur: début.longueur + fin.longueur]int
    ref i ← -1

    pour chaque j de [0 .. début.longueur[:
        i ← i + 1
        T[i] ← début[j]

    pour chaque j de [0 .. fin.longueur[:
        i ← i + 1
        T[i] ← fin[j]

    rendre T

La finitude est claire puisqu'il n'y a que deux boucles de type pour chaque.

On a deux boucles, il faut donc a priori 2 invariants, un pour chaque boucle. Ici il est clair que l'on va remplir tous les éléments des tableaux début et fin dans t. L'invariant peut être :

Invariant de boucle : si $i_0$ est la valeur de $i$ à la ligne 5 (resp. 9) alors à chaque fin d'itération on a $t[i_0 + 1 + k] == \mbox{début}[k]$ (resp. fin) pour tout $0\leq k \leq j$.

Démontrons l'invariant rigoureusement pour la première boucle.

À la fin de la première itération, on a bien :

• $t[i_0 + 1] == \mbox{début}[0]$
• $j = 0$
• $i = i_0 + 1 + j$

Supposons la propriété vraie après une itération donnée. Après une itération supplémentaire, les variables $i$ et $j$ ont été modifiées telles que :

• $j' = j + 1$
• $i' = i + 1 = i_0 + 1 + j'$

L'hypothèse de l'invariant de boucle stipule que $t[i_0 + k] == \mbox{début}[k]$ pour tout $0\leq k \leq j = j'-1$ et comme la boucle a effectué l'affectation : t[i'] ← début[j'], l'invariant continue d'être vérifié. Ce qui conclut la preuve.

Il faut juste faire très attention à l'endroit où l'on commence dans t. Ici c'est Ok car avant la première boucle i = -1 et i = début.longueur - 1 au début de la seconde boucle. Les éléments de début et fin ne vont pas se chevaucher dans t et se suivre sans interruption.

algorithme intersection_non_vide(T1: []int, T2: []int) → bool
    pour chaque x de T1:
        pour chaque y de T2:
            si x == y:
                rendre Vrai
    rendre Faux

La boucle 3-5 va chercher à trouver x dans T2 : trouvé ne peut valoir Vrai que si c'est le cas. Si ce n'est pas le cas, x n'est pas dans T2 et il faut chercher une autre possibilité d'égalité.

Comme on répète cette boucle intérieure pour tout x de T1, l'algorithme ne peut arriver ligne 6 que si $x \notin T2$ pour tout $x \in T1$.

Prouver cet algorithme ne nécessite pas d'invariant de boucle formel.

algorithme égalité_valeurs(T1: []int, T2: []int) → bool
    ref trouvé bool
    pour chaque x de T1:
        trouvé ← Faux
        pour chaque y de T2:
            si x == y:
                trouvé ← Vrai
        si trouvé == Faux:
            rendre Faux

    rendre Vrai

Prouver cet algorithme ne nécessite pas d'invariant de boucle formel, mais il faut faire attention à sa construction.

La boucle 4-6 va chercher à trouver x dans T2 : trouvé ne peut valoir Vrai que si c'est le cas. Si ce n'est pas le cas, on peut sortir de l'algorithme (lignes 7-8) puisque x n'est pas dans T2.

Comme on répète cette boucle intérieure pour tout x de T1, l'algorithme est bien correct.

Il faut pouvoir trouver tous les éléments de $T$ dans $T'$ autant de fois qu'ils sont dans $T$. En utilisant nombre, on a l'algorithme suivant :

algorithme égalité(T1: []int, T2: []int) → int
    pour chaque x de T1:
        si nombre(T1, x) ≠ nombre(T2, x):
            rendre Faux
    rendre Vrai

On ne peut rendre Vrai que si tous les éléments de T1 sont dans T2 avec un même nombre d'occurrences. Donc uniquement s'il existe une permutation $\sigma$ de $[0, n-1]$ telle que $T[i] = T[\sigma(i)]$ pour tout $i \in [0, n-1]$.

Pour que l'algorithme fonctionne, il faut commencer par connaître la taille du tableau à créer et donc compter le nombre d’occurrences de v dans T. Ensuite, il sera possible de remplir le tableau.

algorithme supprime(T: []int, v: int) → []int
    ref T2 ← []int{longueur: taille t.longueur - nombre(T, v)}

    ref j ← 0
    pour chaque i de [0, t.longueur[:
        si T[i] ≠ v:
            T2[j] ← t[i]
            j ← j + 1
    
    rendre T2

La finitude du programme est claire puisque l'on n'a que des boucles de type pour chaque.

On commence par créer un tableau permettant exactement de stocker tous les éléments de T différents de v. Ce que fera la boucle. On peut prouver celle-ci par l'invariant :

Invariant de boucle : à la fin de chaque itération, T2 contient la restriction des i + 1 premiers éléments de T différents de v.

La preuve de l'invariant est évidente et permet de prouver l'algorithme en se plaçant à la fin de la dernière itération.

algorithme supprime_rec(t: []int, v: int) → []int
    si t.longueur == 0:
        rendre t

    ref t2 ← []int{longueur: t.longueur - 1}
    pour i de [0, t2.longueur[:
        t2[i] ← t[i + 1]
    
    si t[0] == v:
        rendre concaténation([], supprime_rec(t2, v))
    sinon:
        rendre concaténation([t[0]], supprime_rec(t2, v))

Il n'y a qu'une seule récursion par algorithme et la taille du tableau passé en paramètre est strictement plus petite : il y a un nombre fini de récursions puisque la condition terminale est basée sur une taille nulle de tableau.

Pour la correction une récurrence immédiate sur la taille du tableau nous permet de conclure.

algorithme retournement_indice(T: []int, i: int) → ∅
    si T.longueur - 1 - i > i:
        ref temp ← T[i]
        T[i] ← T[T.longueur - 1 - i]
        T[T.longueur - 1 - i] ← temp

        retournement_indice(T, i + 1)

Les lignes 3-5 permettent d'échanger les valeurs t[i] et t[t.longueur - 1 - i] du tableau. On peut aussi écrire t[i], t[t.longueur - 1 - i] ← t[t.longueur - 1 - i], t[i], comme on le ferait en python, si l'on autorise le fait d'affecter 2 valeurs en même temps.

La finitude est claire puisque :

1. il n'y a qu'un appel récursif
2. chaque appel se rapproche strictement de la condition d'arrêt

La correction vient du fait que l'on échange bien des valeurs symétriques du tableau par rapport à l'indice du milieu du tableau qui est ici la partie entière de $t.\mbox{longueur} - 1/ 2$.

fonction retournement_indice(T: []int, i: int) → ∅
    ...  # code de la fonction récursive

algorithme retournement(T: []int) → ∅
    retournement_indice(T, 0)

algorithme retournement_indice(t: []int, i: int) → ∅
    ref temp int
    tant que (t.longueur - 1 - i > i):
        temp ← t[i]
        t[i] ← t[t.longueur - 1 - i]
        t[t.longueur - 1 - i] ← temp

        i ← i + 1

Et donc en simplifiant l'écriture :

algorithme retournement(t: []int, i: int) → ∅
    tant que (t.longueur - 1 - i > i):
        t[i], t[t.longueur - 1 - i] ← t[t.longueur - 1 - i], t[i] 
        i ← i + 1

algorithme palindrome(s: str) → bool
    pour chaque i de [0, s.longueur // 2[:
        si s[i] ≠ s[T.longueur - 1 - i]:
            rendre Faux
    rendre Vrai

La finitude et l'exactitude sont évidentes puisque l'on ne fait qu'implémenter la définition.

algorithme palindrome_rec(s: str, i: int) → bool
    si s.longueur - 1 - i ≤ i:
        rendre Vrai
    si  s[i] ≠ s[s.longueur - 1 - i]:
        rendre Faux
    
    rendre palindrome_rec(s, i + 1)

Il faut montrer que l'algorithme rend Vrai si $s[j] = s[s.\mbox{longueur} - 1 - j]$ pour tous $i \leq j < s.\mbox{longueur} - 1 - i$

La première condition est la condition d'arrêt de la récursion puisque dans ce cas-là $i$ a dépassé la moitié du tableau.

Puis on utilise l'équation de récurrence :

palindrome(s) = (s[0] == s[-1]) ET palindrome(s[1:-1])

fonction palindrome_rec(s: str, i: int) → bool
    si s.longueur - 1 - i ≤ i:
        rendre Vrai
    si  s[i] ≠ s[s.longueur - 1 - i]:
        rendre Faux
    
    rendre palindrome_rec(s, i + 1)

algorithme palindrome(T: str) → bool
    rendre palindrome_rec(s, 0)

algorithme palindrome_pas_rec(s: str, i: int) → bool
    tant que (s.longueur - 1 - i > i): 
        si  s[i] ≠ s[s.longueur - 1 - i]:
            rendre Faux
        i ← i + 1
    rendre Vrai

algorithme puissance_2(m: int, n: int) → int:
    si 2 * m ≥ n:
        rendre m
    sinon:
        rendre f(2 * m, n)

C'est bien une récursion terminale puisque le code est équivalent à :

fonction c(m: int, n: int) → bool:
    rendre 2 * m ≥ n

fonction g(m: int, n: int) → int:
    rendre m

algorithme puissance_2(m: int, n: int) → int:
    si c(m, n) == Vrai:
        rendre g(m, n)
    sinon:
        rendre f(2 * m, n)

Avec le type A étant un couple d'entiers et B le type entier.

Il est clairement sous la forme récursive terminale. Il finit car chaque récursion se rapproche strictement de la condition d'arrêt.

Enfin, acc va contenir la factorielle comme le prouve une récursion triviale sur $n$.

fonction u_n_term(n: int, 
                 u0: int, 
                 r: int, 
                 acc: int) → int:
    si n == 0:
        rendre u0 + acc
    rendre u_n_term(n-1, u0, r, r + acc)


algorithme u_n(n : int, 
               u0: int, 
               r : int
              ) → int:
    rendre u_n_term(n, u0, r, 0)

Le but de la récursion terminale est de facilement transformer un algorithme récursif en un algorithme itératif car la récursion est une boucle tant que.

algorithme u_n(n : int, 
               u0: int, 
               r : int
              ) → int:
    ref acc ← 0
    tant que n > 0:
        acc ← r + acc
        n ← n - 1
    
    rendre u0 + acc

algorithme M(n: int) → int:
    si n > 100:
        rendre n - 10
    sinon:
        ref x ← M(n + 11)
        rendre M(x)

Mais est-ce que ce programme se termine ? Rien n'est moins sûr.

algorithme M(n: int) → int:
    ref c ← 1

    tant que c ≠ 0:
        si n > 100:
            n ← n - 10
            c ← c - 1
        sinon:
            n ← n + 11
            c ← c + 1
    rendre n

Comme on peut écrire cette fonction comme une récursion terminale, l'écriture itérative est aisée : Pour $90 \leq n < 101$, on a :

On arrive à ce résultat en 1 récursion : la ligne 5 de l'algorithme en pseudocode de la question précédente.

On a $M(91) = M(92) = \dots = M(101) = 91$ et pour tout $n < 90$ il existera $k > 1$ et $91\leq n'< 101$ tels que $M(n) = M^k(n') = 91$

Comme il faut un nombre fini d'itérations pour passer de $M(n)$ à $M(n+1)$ on en déduit qu'il faut bien un nombre fini d'itérations pour calculer $M(91)$ (disons $I$), et donc également pour calculer $M^k(91)$ quel que soit $k>0$ (il en faut $k\cdot I$).

algorithme M(n: int) → int:
    si n > 100:
        rendre n - 10
    sinon:
        rendre 91

Dans le même ordre d'idées que la fonction de Takeuchi, c'est un leurre.