the correctness proof of Euclid's GCD
/ YOO-klid /
Euclid's algorithm finds the greatest common divisor (gcd) of two numbers — the largest integer dividing both — by a strikingly simple rule: replace the pair (a, b) with (b, a mod b), and repeat until the second number is 0; the first number is then the answer. It is over two thousand years old and still the standard method. Its correctness rests on one clean number-theory fact plus a termination measure, making it a perfect small example of a full (total) correctness proof for a recursive procedure.
The key lemma: for b > 0, gcd(a, b) = gcd(b, a mod b). Why? Write a = q*b + r where r = a mod b. Any number that divides both a and b also divides r = a - q*b; and any number dividing both b and r also divides a = q*b + r. So the pair (a, b) and the pair (b, r) have exactly the same set of common divisors, hence the same greatest one. The base case is gcd(a, 0) = a, since every number divides 0, so the common divisors of a and 0 are just the divisors of a, the largest being a itself. Correctness then follows by induction on the recursive calls: the lemma says each step preserves the gcd, and the base case returns it correctly, so the value the algorithm returns equals gcd of the original inputs.
Termination needs the second argument as a well-founded measure: a mod b is always a non-negative integer strictly less than b, so the second component strictly decreases at every step and cannot go below 0. A strictly decreasing sequence of non-negative integers must reach 0 in finitely many steps, at which point the base case fires. Partial correctness (the lemma + base case) plus termination (the decreasing measure) together give total correctness. Honest caveat: this argument assumes b > 0 to apply the mod step, and that the inputs are non-negative integers; the gcd of two zeros, or of negatives, needs a separate convention.
gcd(252, 105): 252 mod 105 = 42 -> gcd(105, 42); 105 mod 42 = 21 -> gcd(42, 21); 42 mod 21 = 0 -> gcd(21, 0) = 21. The lemma keeps the gcd equal to 21 at every step, while the second argument 105, 42, 21, 0 strictly decreases — correctness and termination, both visible.
Lemma gcd(a,b)=gcd(b, a mod b) keeps the answer fixed; the shrinking second arg forces a stop.
The whole proof hinges on the lemma that (a,b) and (b, a mod b) share the same set of common divisors — not merely the same gcd value by coincidence. Termination relies on a mod b being strictly less than b (a non-negative integer measure).