Un variant qui ne décroît pas assez

let rec pair n = if n = 0 then true else pair (n - 2)

Pour $n=8$, la suite des arguments est $8,6,4,2,0$ : le cas de base est atteint en quatre appels et la fonction rend true. Pour $n=7$, elle est $7,5,3,1,-1,-3,-5,\dots$ : le cas de base n'est jamais atteint.

Le diagnostic est plus fin que « le variant ne décroît pas ». L'argument décroît parfaitement, de $2$ à chaque appel. Ce qui manque, c'est la minoration : un variant est un entier positif qui décroît strictement. Ici $n$ décroît sans plancher, et la définition n'est donc pas bien fondée sur les impairs.

Un second fait, mesuré, et il surprend. On attend un débordement de pile ; il ne vient pas. L'appel pair (n-2) est terminal, donc OCaml réutilise le bloc d'activation : le programme boucle indéfiniment en espace constant, sans jamais rien signaler. La même faute écrite sans appel terminal se dénonce aussitôt :

let rec pair_nt n = if n = 0 then 0 else 1 + pair_nt (n - 2)
(* pair_nt 7 : Exception: Stack_overflow *)

Retenir cette dissymétrie : la récursion terminale, qui protège du débordement, prive aussi du seul symptôme qui aurait dénoncé une définition mal fondée.

La correction donne deux cas de base, un par classe de reste modulo $2$ :

(* pair n dit si n est pair. Precondition : n >= 0.
   Variant : n, entier positif -- et 0 comme 1 arretent la descente. *)
let rec pair n = if n = 0 then true else if n = 1 then false else pair (n - 2)