Exemple : le pgcd
let rec gcd = function n -> function m ->
if (m = 0)
then n
else gcd m (n mod m) ;;
Termine pour m et n positifs ?
-
supposons m < n.
-
Si m=0 le résultat est correct.
- Sinon on a 0 £ (nmodm) < m et
nmodm < m
et le couple (n,m) décroît strictement pour l'ordre produit.
- si m ³ n alors
m < (nmodm)3
et on utilise le point précédent.
Tout diviseur commun à n et m divise le pgcd :
Si d divise n et m alors n = d n' et m = d m' et on a :
| nmodm |
= |
(d n')mod(d m') |
| |
= |
d(n'modm') |
en supposant le bon fonctionnement de mod
et d divise (nmodm).
- 3
- sauf si m=n=0 mais le résultat reste correct