Comment décrire les algorithmes, les prouver et les analyser?

Avant de lire L'Art de la programmation informatique (TAOCP) , je n'ai pas approfondi ces questions. J'utiliserais un pseudo-code pour décrire des algorithmes, les comprendre et estimer le temps d'exécution uniquement sur les ordres de croissance. Le TAOCP change complètement d'avis.

TAOCP utilise un anglais mélangé avec des étapes et goto pour décrire l'algorithme, et utilise des organigrammes pour visualiser l'algorithme plus facilement. Cela semble de bas niveau, mais je trouve qu'il y a certains avantages, en particulier avec l'organigramme, que j'ai beaucoup ignoré. Nous pouvons étiqueter chacune des flèches avec une assertion sur l'état actuel des choses au moment où le calcul traverse cette flèche, et faire une preuve inductive pour l'algorithme. L'auteur dit:

Selon l'auteur, nous comprenons vraiment pourquoi un algorithme n'est valable que lorsque nous atteignons le point où nos esprits ont implicitement rempli toutes les affirmations, comme cela a été fait dans la Fig.4.

Je n'ai pas connu de telles choses. Un autre avantage est que nous pouvons compter le nombre de fois que chaque étape est exécutée. Il est facile de vérifier avec la première loi de Kirchhoff. Je n'ai pas analysé exactement le temps de fonctionnement, donc certains $\pm1$ pourraient avoir été omis lors de l'estimation du temps de fonctionnement.

L'analyse des ordres de croissance est parfois inutile. Par exemple, nous ne pouvons pas distinguer le tri rapide du tri actif car ils sont tous $E(T(n))=\Theta(n\log n)$ , où $EX$ est le nombre attendu de variable aléatoire $X$ , nous devons donc analyser la constante, disons, $E(T_1(n))=A_1n\lg n+B_1n+O(\log n)$et $E(T_2(n))=A_2\lg n+B_2n+O(\log n)$ , nous pouvons donc mieux comparer $T_1$ et $T_2$ . Et aussi, parfois, nous devons comparer d'autres quantités, telles que les variances. Seule une analyse grossière des ordres de croissance du temps de course ne suffit pas. Comme TAOCP traduit les algorithmes en langage assembleur et calcule le temps d'exécution, c'est trop difficile pour moi, donc je veux connaître quelques techniques pour analyser le temps d'exécution un peu plus approximativement, ce qui est également utile, pour les langages de plus haut niveau tels que C, C ++ ou pseudo-codes.

Et je veux savoir quel style de description est principalement utilisé dans les travaux de recherche et comment traiter ces problèmes.

Il existe une grande variété d'approches possibles. Ce qui convient le mieux dépend de

• ce que vous essayez de montrer,
• combien de détails vous voulez ou avez besoin.

Si l'algorithme est largement connu et que vous utilisez comme sous-programme, vous restez souvent à un niveau supérieur. Si l'algorithme est l'objet principal étudié, vous voudrez probablement être plus détaillé. La même chose peut être dite pour les analyses: si vous avez besoin d'une limite d'exécution supérieure approximative, vous procédez différemment de lorsque vous voulez un décompte précis des instructions.

Je vais vous donner trois exemples pour l'algorithme bien connu Mergesort qui, espérons-le, illustrent cela.

Haut niveau

L'algorithme Mergesort prend une liste, la divise en deux parties (à peu près) également longues, revient sur ces listes partielles et fusionne les résultats (triés) afin que le résultat final soit trié. Sur des listes singleton ou vides, il renvoie l'entrée.

Cet algorithme est évidemment un algorithme de tri correct. Le fractionnement de la liste et sa fusion peuvent chacun être mis en œuvre dans le temps , ce qui nous donne une récurrence pour le pire cas d'exécution T ( n ) = 2 T ( $\Theta(n)$. Par le théorème maître, cela équivaut àT(n)∈Θ(nlogn).$T(n) = 2T\left(\frac{n}{2}\right) + \Theta(n)$$T(n) \in \Theta(n\log n)$

Niveau moyen

L'algorithme Mergesort est donné par le pseudo-code suivant:

procedure mergesort(l : List) {
  if ( l.length < 2 ) {
    return l
  }

  left  = mergesort(l.take(l.length / 2)
  right = mergesort(l.drop(l.length / 2)
  result = []

  while ( left.length > 0 || right.length > 0 ) {
    if ( right.length == 0 || (left.length > 0 && left.head <= right.head) ) {
      result = left.head :: result
      left = left.tail
    }
    else {
      result = right.head :: result
      right = right.tail
    }
  }

  return result.reverse
}

Nous prouvons l'exactitude par induction. Pour les listes de longueur zéro ou un, l'algorithme est trivialement correct. Comme hypothèse d'induction, supposons qu'il mergesortfonctionne correctement sur des listes de longueur au plus pour certains n naturels arbitraires mais fixes n > 1 . Soit maintenant L une liste de longueur n + 1 . Par hypothèse d'induction, et maintenez (sans diminution) les versions triées du premier resp. seconde moitié de L après les appels récursifs. Par conséquent, la boucle sélectionne à chaque itération le plus petit élément non encore étudié et l'ajoute à ; est donc une liste non triée de plus en plus contenant tous les éléments de$n$$n>1$$L$$n+1$leftright$L$whileresultresultleftet right. L'inverse est une version triée de façon non décroissante de , qui est le résultat renvoyé - et souhaité -.$L$

Quant à l'exécution, comptons les comparaisons d'éléments et listons les opérations (qui dominent l'exécution de manière asymptotique). Les listes de longueur inférieure à deux ne provoquent ni l'un ni l'autre. Pour les listes de longueur , nous avons ces opérations causées par la préparation des entrées pour les appels récursifs, celles des appels récursifs eux-mêmes plus la boucle et une . Les deux paramètres récursifs peuvent être calculés avec au plus n opérations de liste chacune. La boucle est exécutée exactement n fois et chaque itération provoque au plus une comparaison d'éléments et exactement deux opérations de liste. La finale peut être implémentée pour utiliser 2 $n>1$whilereverse$n$while$n$reverse$2n$opérations de liste - chaque élément est supprimé de l'entrée et placé dans la liste de sortie. Par conséquent, le nombre d'opérations remplit la récurrence suivante:

$\qquad \begin{align}T(0) = T(1) &= 0 \\ T(n) &\leq T\left(\left\lceil\frac{n}{2}\right\rceil\right) + T\left(\left\lfloor\frac{n}{2}\right\rfloor\right) + 7n\end{align}$

Comme est clairement non décroissant, il suffit de considérer n = 2 k pour une croissance asymptotique. Dans ce cas , la récurrence se simplifie pour$T$$n=2^k$

$\qquad \begin{align}T(0) = T(1) &= 0 \\ T(n) &\leq 2T\left(\frac{n}{2}\right) + 7n\end{align}$

Par le théorème maître, nous obtenons qui s'étend à l'exécution de .$T \in \Theta(n \log n)$mergesort

Niveau ultra bas

Considérez cette implémentation (généralisée) de Mergesort dans Isabelle / HOL :

types dataset  =  "nat * string"

fun leq :: "dataset \<Rightarrow> dataset \<Rightarrow> bool" where
   "leq (kx::nat, dx) (ky, dy) = (kx \<le> ky)"

fun merge :: "dataset list \<Rightarrow> dataset list \<Rightarrow> dataset list" where
"merge [] b = b" |
"merge a [] = a" |
"merge (a # as) (b # bs) = (if leq a b then a # merge as (b # bs) else b # merge (a # as) bs)"

function (sequential) msort :: "dataset list \<Rightarrow> dataset list" where
  "msort []  = []" |
  "msort [x] = [x]" |
  "msort l   = (let mid = length l div 2 in merge (msort (take mid l)) (msort (drop mid l)))"
by pat_completeness auto
  termination
  apply (relation "measure length")
by simp+

Cela comprend déjà des preuves de bonne définition et de résiliation. Trouvez ici une preuve d'exactitude (presque) complète .

Pour le "runtime", c'est-à-dire le nombre de comparaisons, une récurrence similaire à celle de la section précédente peut être mise en place. Au lieu d'utiliser le théorème maître et d'oublier les constantes, vous pouvez également l'analyser pour obtenir une approximation qui est asymptotiquement égale à la vraie quantité. Vous pouvez trouver l'analyse complète dans [1]; voici un aperçu (il ne correspond pas nécessairement au code Isabelle / HOL):

Comme ci-dessus, la récurrence du nombre de comparaisons est

$\qquad \begin{align}f_0 = f_1 &= 0 \\ f_n &= f_{\left\lceil\frac{n}{2}\right\rceil} + f_{\left\lfloor\frac{n}{2}\right\rfloor} + e_n\end{align}$

$e_n$$n$

$\qquad \displaystyle \begin{cases} f_{2m} &= 2f_m + e_{2m} \\ f_{2m+1} &= f_m + f_{m+1} + e_{2m+1} \end{cases}$

Utilisation de différences imbriquées avant / arrière$f_n$$e_n$

$\qquad \displaystyle \sum\limits_{k=1}^{n-1} (n-k) \cdot \Delta\kern-.2em\nabla f_k = f_n - nf_1$

$\Delta\kern-.2em\nabla f_k$

$\qquad \displaystyle W(s) = \sum\limits_{k\geq 1} \Delta\kern-.2em\nabla f_k k^{-s} = \frac{1}{1-2^{-s}} \cdot \underbrace{\sum\limits_{k \geq 1} \frac{\Delta\kern-.2em\nabla e_k}{k^s}}_{=:\ \boxminus(s)}$

qui, avec la formule de Perron, nous amène à

$\qquad \displaystyle f_n = nf_1 + \frac{n}{2\pi i} \int\limits_{3-i\infty}^{3+i\infty} \frac{\boxminus(s)n^s}{(1-2^{-s})s(s+1)}ds$

Évaluation de $\boxminus(s)$

$\qquad \displaystyle f_n \sim n \cdot \log_2(n) + n \cdot A(\log_2(n)) + 1$

$A$$[-1,-0.9]$

1. Transformées de Mellin et asymptotiques: la récurrence de fusion-fusion par Flajolet et Golin (1992)
2. Meilleur cas: $e_n = \left\lfloor\frac{n}{2}\right\rfloor$
   $e_n = n-1$
   $e_n = n - \frac{\left\lfloor\frac{n}{2}\right\rfloor}{\left\lceil\frac{n}{2}\right\rceil + 1} - \frac{\left\lceil\frac{n}{2}\right\rceil}{\left\lfloor\frac{n}{2}\right\rfloor + 1}$

Dijkstra's«Une discipline de programmation» de consiste à analyser et à prouver des algorithmes et à concevoir pour la prouvabilité. Dans la préface de ce livre, Dijkstra explique comment un mini-langage construit très simple et correctement conçu pour être analysé suffit pour expliquer formellement de nombreux algorithmes:

Lorsque l'on démarre un livre comme celui-ci, on se retrouve immédiatement face à la question: "Quel langage de programmation vais-je utiliser?", Et ce n'est pasune simple question de présentation! Un aspect le plus important, mais aussi le plus insaisissable de tout outil est son influence sur les habitudes de ceux qui se forment à son utilisation. Si l'outil est un langage de programmation, cette influence est - que cela nous plaise ou non - une influence sur nos habitudes de pensée. Ayant analysé cette influence au mieux de mes connaissances, j'étais parvenu à la conclusion qu'aucun des langages de programmation existants, ni un sous-ensemble d'entre eux, ne conviendrait à mon objectif; d'un autre côté, je me connaissais tellement mal préparé pour la conception d'un nouveau langage de programmation que j'avais fait le vœu de ne pas le faire pendant les cinq prochaines années, et j'avais le sentiment le plus net que cette période ne s'était pas encore écoulée! (Avant cela, entre autres choses, cette monographie devait être écrite.

Plus tard, il explique à quel point il a réussi à obtenir sa mini-langue.

Je dois au lecteur d'expliquer pourquoi j'ai gardé le mini-langage si petit qu'il ne contient même pas de procédures et de récursivité. ... Le fait est que je n'en ressentais pas le besoin pour faire passer mon message, à savoir. comment une séparation soigneusement choisie des préoccupations est essentielle pour la conception de programmes de haute qualité à tous égards; les outils modestes de la mini-langue nous donnaient déjà plus que suffisamment de latitude pour des conceptions non triviales, mais très satisfaisantes.