McCarthy 91 : le variant n'est pas un argument

let rec f n = if n > 100 then n - 10 else f (f (n + 11))

Elle termine, et $f(n)=91$ pour tout $n\le 100$ — vérifié par le calcul pour tous les entiers de $-1000$ à $100$. Au-delà, $f(n)=n-10$.

La difficulté est double, et il faut la nommer avant de la résoudre. L'argument augmente de $11$ à chaque appel interne : aucun variant décroissant ne peut porter sur $n$ tel quel. Et l'appel externe porte sur une valeur calculée : on ne connaît son argument qu'après avoir exécuté l'appel interne.

Le variant. On pose

$$\mu (n)=\{\begin{array}{ll}101-n& \text{si }n\le 100,\\ 0& \text{sinon,}\end{array}$$

à valeurs dans $\mathbb{N}$, muni de $\le$, qui est bien fondé.

L'appel interne $f(n+11)$ avec $n\le 100$ : si $n+11\le 100$, alors $\mu (n+11)=90-n<101-n=\mu (n)$ ; sinon $\mu (n+11)=0\le \mu (n)$, et l'appel se termine en une étape puisque $n+11>100$. Le variant décroît, ou l'appel est immédiat.

L'appel externe $f(v)$ où $v=f(n+11)$ : il faut savoir que $v\ge 91$ pour tout $n$, ce qui est précisément le résultat qu'on démontre. Terminaison et valeur ne se séparent pas ici, et c'est ce qui rend cette fonction célèbre : on prouve les deux simultanément, par récurrence sur $\mu (n)$.

La preuve, en deux temps. Pour $91\le n\le 100$ : $n+11$ est entre $102$ et $111$, donc $f(n+11)=n+1$, et $f(n)=f(n+1)$. Une récurrence descendante depuis $f(101)=91$ donne $f(n)=91$ sur tout cet intervalle. Pour $n<91$ : $n+11\le 101$, l'hypothèse de récurrence sur $\mu$ donne $f(n+11)=91$, donc $f(n)=f(91)=91$.

Les mesures qui accompagnent. Nombre d'appels : $1$ pour $f(101)$, $3$ pour $f(100)$, $5$ pour $f(99)$, $29$ pour $f(87)$, $103$ pour $f(50)$, $201$ pour $f(1)$. On lit la structure : deux appels de plus par unité en dessous de $100$, tant qu'on reste au-dessus de $90$ ; puis un régime plus lent.

La leçon. Un variant n'est pas « l'argument », ni « un des arguments » : c'est n'importe quelle fonction des arguments à valeurs dans un ensemble bien fondé, et c'est au programmeur de l'inventer. Ici il fallait le chercher dans la distance à $101$, une quantité qui n'apparaît nulle part dans le code.