L'algorithme d'Euclide

let rec pgcd a b =
  if b = 0 then a
  else pgcd b (a mod b)

Déroulé de pgcd 30 12 : $\to$ pgcd 12 6 (car $30\mathrm{mod}12=6$) $\to$ pgcd 6 0 (car $12\mathrm{mod}6=0$) $\to$ renvoie 6. Le cas de base b = 0 est atteint car le reste a mod b décroît strictement et reste positif : la suite des seconds arguments est une suite d'entiers naturels strictement décroissante, donc finie.