1158

A bagatelle on Euclid’s Algorithm

EWD1158 · 1991–1995 · PDF · Source language: English. · Local OCR-derived source needs manual review.

A bagatelle on Euclid's Algorithm

If $x$ gcd $Y = 1$ ,the Diophantine equation

(a) $a,b : aX + bY = 1$

is solvable. I am almost certain that the first proof I saw of this theorem was non-constructive and of the following structure.

Consider the $Y$ remainders $(0\leq i < Y)$

$$ r _ {i} = (i. X) \mod Y \quad (0 \leq r _ {i} < Y). $$

$$ \begin{array}{l} \begin{array}{r l} {\mathrm {S i n c e}} & {= \left{ \begin{array}{l l} r _ {i} = r _ {j} \ \mathrm {d e f . a n d a r i t h m e t i c} \end{array} \right}} \ & {Y \mid (i, X) - (j, X)} \end{array} \ = \begin{array}{l} {{a r i t h m e t i c }} \ {Y | (i - j). X} \end{array} \ \Rightarrow \quad {X _ {g c d} Y = 1 } \ Y \vert (i - j) \ = {0 \leq i, j < Y } \ i = j \ \end{array} $$

all the $r_i$ are distinct; because of $0 \leq r_i < Y$ , each value occurs once, in particular, one of the remainders, $r_n$ say, equals 1, i.e. for some $k$ , we have

$$ n X = k Y + r _ {n} = k Y + 1 $$

Thus $\begin{array}{l} a,b \end{array} \mathrel{\text{:=}} n, - k\;$ yields a solution of (0)

My first step is to generalize the theorem

by removal of the constant 1 : the Diophan-

(1) $a,b : \;aX + bY = q\;$ where $q = X\gcd Y$

is solvable. This time we give a constructive proof by actually solving equation (1). On Euclid's Algorithm we superpose the additional invariant

$\left( 2\right) \;{aX} + {bY} = x\; \land \;{cX} + {dY} = y\;\therefore$

[\left\lbrack \begin{matrix} \text{var} & x,y,a,b,c,d \ \text{ }} & \end{matrix}\right\rbrack \text{.}]

$\therefore x,y,{a}^{2},{b}^{2},c,d$ ② $= {x}^{2} + {y}^{2} + {z}^{2}$

$\left{ \begin{matrix} \frac{d}{dt}x > y \rightarrow x,a,b \mathrel{\text{:=}} x - y,a - c,b - d \ y > x \rightarrow y,c,d \mathrel{\text{:=}} y - x,c - a,d - b \end{matrix}\right.$

$\left{ \left( 2\right) \land x = q,hence\;\left( 1\right) }$

It is just another example of "Proving

The above is so elementary that I hesitated to devote an EWD to it. But I think the con-structive proof interesting for a number of reasons.

We should not complain about what I believe to be the general state of affairs that, for the same existence theorem, the constructive proof tends to be longer than the nonconstructive one: after all, it delivers more.

Here, however, the constructive argument seems to me as short-if not shorter-as the nonconstructive argument.

The constructive argument is beautifully forced. Upon completion the goal (1) $aX + bY = q$ has to follow from $x = q$ and the invariant What else than $aX + bY = x$ could that be? The second conjunct in (2) is added to maintain the symmetry.

  • The Diophantine equation

(3) $\begin{array}{l} a,b,c : aX + bY + cZ = q \ q = X\gcd Y\gcd Z \end{array}$ where

is solvable. This theorem can be proved from the program for the gcd of 3 positive numbers

$$ \begin{array}{l} \begin{array}{l} \left[ \begin{array}{l l l l} \operatorname {v a r} & x, y, z: & \mathrm {i n t} \ \vdots & x, y, z := & X, Y, \end{array} \right. \end{array} \ \begin{array}{r l}{; \quad \underline {{d o}} x > y}&{\rightarrow x := x - y}\{\mathrm {I} y > z}&{\rightarrow y := y - z}\{\mathrm {I} z > x}&{\rightarrow z := z - 1}\end{array} \ \end{array} $$

$$ ] 1 \stackrel {o d} {\longrightarrow}, $$

and now the constructive proof is much more elegant than the nonconstructive argument I could come up with (which suffers from an even more severe destruction of the symmetry).

Remark To satisfy my curiosity, I looked this theorem up in Courant/Robbins "What is mathematics?". They gave -a sketch of- a constructive argument! One up for them. But their text vividly shows that half a century ago, there was no tradition of an adequate style of describing algorithms. Consequently, the prevailing style of reasoning about algorithms was no better. It is nice to see that there has been progress since 1941. (End of Remark.)

[0] A.J. M. van Gasteren "On the shape of mathematical arguments", LNCS 445, Springer-Verlag

Austin, 10 Sep. 1993

prof. dr. Edsger W. Dyrksha Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA