Euclid’s Algorithm for GCD: A Generic Loop-Invariant

[This page is auto-generated; please prefer to read the article’s PDF Form.]

[Prev] [Up] [Next]

A Generic Loop-Invariant

Suppose, there is a predicate R(x) over non-negative integers x with the property that, for any x and y with x ≥ y > 0, whenever R(x) ∧ R(y) holds, then R(x mod y) must also hold. This can be denoted as:

(x ≥ y > 0) ∧ R (x ) ∧ R(y) ⇒ R (x mod y)

(1)

Say, one such predicate R holds true for variables a and b (R(a) ∧ R(b)) in Euclid’s Algorithm just before the loop starts, i.e. when a = A,b = B. Any iteration of this loop simply modiﬁes a (or b) to a mod b (or b mod a), thus maintaining R(a) ∧ R(b) due to property (1). Hence, we have found a generic loop-invariant, R(a) ∧ R(b), in the Euclid’s Algorithm.

Now, upon loop termination, when a = gcd(A,B) and b = 0 (the other case is similar), R(a) ∧ R(b) must still hold, implying R(gcd(A,B)) ∧ R(0). Thus, Euclid’s Algorithm has helped us prove the following theorem.

Theorem 3. Suppose R(x) is a predicate over non-negative integers x with the property (1). Then, for any non-negative integers A and B:

R (A)∧ R (B) ⇒ R (gcd(A,B ))

Now, say there is a predicate R′(x) over non-negative integers x with a slightly diﬀerent property:

′ ′ ′ (x ≥ y > 0) ∧ R (x ) ∧ R (y) ⇒ R (x − y)

(2)

Then, repeated application of this property shows that for any integer i ≥ 1 such that x ≥ iy, R′(x − iy) must also hold. Also, x = qy + (x mod y) for some integer q (Division Theorem) and here q ≥ 1, x ≥ qy. This implies that R′(x − qy) = R′(x mod y) must also hold. In other words, R′ also satisﬁes property (1), and hence can beneﬁt from theorem 3.

Corollary 4. Suppose R′(x) is a predicate over non-negative integers x with the property (2). Then, for any non-negative integers A and B:

R ′(A )∧ R′(B) ⇒ R′(gcd (A, B ))

We can use the above theorem to help us prove other relations which deal with integers and their gcd. Two such examples are presented below.

[Prev] [Up] [Next]