= Solution
Use the remainder form of the <Euclidean algorithm> to compute the <greatest common divisor>, then divide both components of the <fraction> by it:
``
def Reduce(num: Int, den: Int): (Int, Int) = {
require(0 <= num && num < den)
var a = den
var b = num
while (b != 0) {
val r = a % b
a = b
b = r
}
(num / a, den / a)
}
``
The <loop invariant> is $a>0$, $b\geq0$, and $\gcd(a,b)=\gcd(den,num)$. Initially it holds by symmetry of the <greatest common divisor>. For $b>0$, the <integer division> identity $a=qb+r$, with $0\leq r<b$, shows that $a,b$ and $b,r$ have exactly the same common <integer divisors>. Thus the update preserves the <loop invariant>. The <loop variant> is the nonnegative <integer> $b$, which strictly decreases on each iteration. At exit $b=0$, so $a=\gcd(den,num)>0$. Dividing by $a$ preserves the <rational number> and makes the returned components <coprime>. In particular, \b[zero is returned as $(0,1)$]. No multiplication is needed, and all remainders remain within the original nonnegative `Int` range.
Back to article page
