Ordres bien fondés et induction structurelle

(* Précondition : m >= 0 et n >= 0. *)
let rec ackermann m n =
  if m = 0 then n + 1
  else if n = 0 then ackermann (m - 1) 1
  else ackermann (m - 1) (ackermann m (n - 1))

Aucun des deux arguments ne décroît à chaque appel : dans le dernier cas, $m$ reste égal à $m$ dans l'appel interne. Mais le couple $(m,n)$ décroît strictement pour l'ordre lexicographique :

• $(m-1,1){\prec }_{\text{lex}}(m,n)$ car $m-1<m$ ;
• $(m,n-1){\prec }_{\text{lex}}(m,n)$ car $m=m$ et $n-1<n$ ;
• $(m-1,\cdot ){\prec }_{\text{lex}}(m,n)$ pour l'appel externe.

Et l'ordre lexicographique sur ${\mathbb{N}}^2$ est bien fondé. La fonction termine donc — pour tout $(m,n)$, bien qu'elle croisse plus vite que toute fonction exprimable par une composition finie d'exponentielles.

Le programme demande de « faire le lien avec la notion d'accessibilité dans un graphe orienté acyclique ». Un ordre bien fondé sur un ensemble fini se lit comme un graphe orienté acyclique : les sommets sont les éléments, un arc va de $y$ vers $x$ quand $x$ est un prédécesseur immédiat de $y$. « Bien fondé » y devient « sans cycle », et les éléments minimaux sont les sommets sans arc sortant. Le tri topologique du chapitre chap:parcours exploitera exactement cette correspondance.

$$\begin{array}{ll}\text{Les entiers naturels}& \frac{}{0\in \mathbb{N}}\frac{n\in \mathbb{N}}{S(n)\in \mathbb{N}}\\ \text{Les arbres binaires}& \frac{}{\text{Vide}\in \mathcal{A}}\frac{g\in \mathcal{A}d\in \mathcal{A}}{\text{Nœud}(g,e,d)\in \mathcal{A}}\\ \text{Les formules}& \frac{}{p\in \mathcal{F}}(p\text{ variable})\frac{\phi \in \mathcal{F}\psi \in \mathcal{F}}{(\phi \wedge \psi )\in \mathcal{F}}\end{array}$$

Une barre de fraction se lit « si le dessus, alors le dessous » ; une barre sans rien au-dessus est une assertion. Ces trois systèmes se traduisent mot pour mot en types OCaml, et c'est ce qui rend le langage si adapté :

type nat = Zero | S of nat
type 'a arbre = Vide | Noeud of 'a arbre * 'a * 'a arbre
type formule = Var of string | Et of formule * formule

Le programme y insiste : « on insiste sur les aspects pratiques : construction de structure de données et filtrage par motif ».

Pour $a=\text{Nœud}(g,e,d)$, on a $g\prec a$ et $d\prec a$ : un sous-arbre est strictement plus petit que l'arbre. Les éléments minimaux sont les Vide. C'est ce qui fait terminer toutes les fonctions récursives sur les arbres du chapitre chap:arbres — sans qu'aucun entier n'ait à décroître.

Soit $E$ un ensemble inductif engendré par des assertions et des règles, et $P$ une propriété sur $E$. Si :

• $P$ est vraie pour chaque assertion ;
• pour chaque règle, si $P$ est vraie de tous les arguments, alors elle l'est du résultat ;

alors $P$ est vraie sur $E$ tout entier.

Pour un arbre binaire $a$, notons $n(a)$ son nombre de nœuds et $f(a)$ son nombre de feuilles — les nœuds dont les deux fils sont vides. Notons $d(a)$ le nombre de nœuds ayant deux fils non vides. Montrons

$$f(a)=d(a)+1\text{pour tout arbre non vide }a.$$

let rec feuilles = function
  | Vide -> 0
  | Noeud (Vide, _, Vide) -> 1
  | Noeud (g, _, d) -> feuilles g + feuilles d

Remarquez la correspondance : trois cas de preuve, trois motifs de filtrage. Le compilateur qui vérifie l'exhaustivité de votre match vérifie, littéralement, que votre preuve n'oublie aucun cas.