Recherche dichotomique récursive, prouvée

(* cherche t x renvoie un indice i tel que t.(i) = x, ou -1 si x est absent.
   Precondition : t est trie par ordre croissant.
   La fonction auxiliaire travaille sur la tranche t.(g .. d-1). *)
let cherche t x =
  let rec aux g d =
    if g >= d then -1
    else
      let m = g + (d - g) / 2 in
      if t.(m) = x then m
      else if t.(m) < x then aux (m + 1) d
      else aux g m
  in aux 0 (Array.length t)

Terminaison. Variant : $d-g$, entier positif (l'appel n'a lieu que si $g<d$). Comme $g\le m<d$, la tranche $[m+1,d[$ a pour largeur $d-m-1<d-g$, et la tranche $[g,m[$ a pour largeur $m-g\le (d-g)/2<d-g$. Le variant décroît strictement, et il est minoré par $0$ : la récursion s'arrête.

Correction. Invariant, au sens de la récurrence sur le variant : si $x$ figure dans $t$, alors il figure dans la tranche $t[g..d-1]$. Il tient à l'appel initial (la tranche est le tableau entier). Il se conserve : le tableau étant trié, si $t[m]<x$ tout indice $\le m$ porte une valeur $\le t[m]<x$, donc $x$ ne peut être qu'à droite ; symétriquement à gauche. À l'arrêt, ou bien on a trouvé $x$ en $m$, ou bien la tranche est vide et l'invariant dit alors que $x$ n'est nulle part.

Complexité. La largeur est au moins divisée par deux à chaque appel : $T(n)=T(n/2)+O(1)$, deuxième récurrence du cours avec $a=1$, donc $\Theta (\log n)$ comparaisons. Mesuré : le nombre maximal d'appels vaut exactement $\lfloor {\log }_{2}n\rfloor +2$.

n :                     1    7   15   1000   1000000
appels au pire :        2    4    5     11        21
floor(log2 n) + 2 :     2    4    5     11        21

En espace, la profondeur de pile est $\Theta (\log n)$ — soit $21$ blocs pour un million d'éléments. C'est l'exemple annoncé par la mise en garde du cours : une récursion sur $n$ éléments un par un coûte $O(n)$ en pile, la même en dichotomie coûte $O(\log n)$.

Deux fautes classiques que la preuve écarte. Écrire aux m d au lieu de aux (m+1) d : le variant ne décroît plus quand $m=g$, et la fonction boucle. Écrire (g + d) / 2 : correct en OCaml, où les entiers font $63$ bits, mais générateur de dépassement en C sur de grands indices — on y écrit g + (d - g) / 2, comme au chapitre chap:langage-c.