= Greedy Egyptian fraction expansion
For a positive proper residual <fraction> $n/d$, with $0<n<d$, choose $q=\lceil d/n\rceil$, append the <unit fraction> $1/q$, and replace the residual by $(nq-d)/(dq)$ in lowest terms. This is a <greedy algorithm>: the chosen <unit fraction> is the largest one not exceeding the residual.
The inequalities $q-1<d/n\leq q$ imply $0\leq nq-d<n$. Thus the numerator of the reduced residual strictly decreases while positive, proving <algorithm termination> by a nonnegative-<integer> <loop variant>. The <loop invariant> is that the accumulated <sum> plus the residual is the original <rational number>. Since $q\geq2$ and $n/d<1/(q-1)$, the new residual is less than $1/(q(q-1))\leq1/q$. If it remains positive, its next chosen denominator is therefore strictly greater than $q$; this expansion also satisfies the distinct-denominator convention. The proof does not bound the denominators by the input's fixed-width range. <Arbitrary-precision arithmetic>, checked conversion, or a different representable expansion can therefore be necessary in code.
Back to article page
