Le test local ne suffit pas

let rec est_abr_naif = function
  | Vide -> true
  | Noeud (g, e, d) ->
      let ok_g = match g with Vide -> true | Noeud (_, eg, _) -> eg < e in
      let ok_d = match d with Vide -> true | Noeud (_, ed, _) -> ed > e in
      ok_g && ok_d && est_abr_naif g && est_abr_naif d

Sur l'arbre $8(3(1,9),10)$, est_abr_naif rend true : chaque nœud pris avec ses deux fils immédiats respecte la condition. Et pourtant $9$ est dans le sous-arbre gauche de $8$.

Pourquoi le test local ne peut pas marcher. L'invariant d'ABR est global : il porte sur tout le sous-arbre, pas sur les deux fils. Un test qui n'examine qu'un nœud et ses fils regarde une fenêtre de profondeur $1$ ; l'invariant, lui, contraint des nœuds arbitrairement éloignés. Aucune fenêtre bornée ne peut le décider.

Le test correct, par le parcours infixe. Le théorème du chapitre donne une caractérisation : $a$ est un ABR si et seulement si infixe a est strictement croissante.

(* Renvoie la liste infixe de a suivie de acc. Complexité : Theta(n). *)
let rec infixe_acc a acc = match a with
  | Vide -> acc
  | Noeud (g, e, d) -> infixe_acc g (e :: infixe_acc d acc)

let rec croissante = function
  | [] | [_] -> true
  | a :: (b :: _ as r) -> a < b && croissante r

(* Renvoie true ssi a est un arbre binaire de recherche. *)
let est_abr a = croissante (infixe_acc a [])

Spécification : entrée un arbre binaire d'entiers, sortie un booléen valant vrai exactement quand l'invariant d'ABR tient. Terminaison : infixe_acc descend structurellement, croissante raccourcit sa liste. Complexité : $\Theta (n)$ en temps — on emploie l'accumulateur du chapitre chap:arbres, pas la version à @ qui serait quadratique — et $O(n)$ en espace pour la liste.

La variante par encadrement, qui évite de construire la liste :

(* Vrai ssi toutes les étiquettes de a sont dans l'intervalle ouvert (bmin, bmax). *)
let est_abr_bornes a =
  let rec aux a bmin bmax = match a with
    | Vide -> true
    | Noeud (g, e, d) ->
        (match bmin with None -> true | Some m -> m < e)
        && (match bmax with None -> true | Some m -> e < m)
        && aux g bmin (Some e) && aux d (Some e) bmax
  in aux a None None

Elle est aussi en $\Theta (n)$, en $O(h)$ d'espace seulement. Mesuré : les deux rendent false sur le contre-exemple, où la version naïve rend true. Noter le type int option pour les bornes : écrire min_int et max_int marcherait presque, et échouerait sur un arbre contenant précisément ces valeurs — le piège du chapitre chap:langage-c, transposé.