Computing remainders by doubling

I'm going through Stepanov and Rose's From Mathematics to Generic Programming, and on page 48 they present a fast algorithm for computing remainders without using either division or multiplication. Unfortunately, there's not much in terms of proof [1], so this post is to document my understanding of the algorithm.

The algorithm relies on the following lemma: For , given , we have:

To prove this, consider the standard quotient and remainder representation of a's and b's relation: , with q the quotient and r the remainder. q can be either even or odd. If it's even, we can say that there exists such that , so:

In this case, the remainder of a divided by 2b is trivially r (the same as the remainder divided by b). If q is odd, we can say that , so:

In this case, the remainder of a divided by 2b is b+r. Now it's obvious why the lemma is true. Without explicitly distinguishing q as even or odd, it just examines the remainder of a divided by 2b. If this remainder is smaller than b, then that's also the remainder of dividing by b because q must be even. On the other hand, if the remainder is larger than b, q must be odd and we have b+r as the remainder, in which case we subtract b to get to r.

Now, the algorithm itself, as Python code [2]:

def fast_remainder(a, b):
    if a < b: return a
    if a - b < b: return a - b
    r = fast_remainder(a, b + b)
    if r < b: return r
    return r - b

It starts by covering base cases of a being up to 2b. Then it recurses to find the remainder of a divided by 2b. This is a curious recursive pattern, as the parameters grow rather than shrink! Therefore, it's important to prove that this recursion terminates (if it does, its correctness stems from the lemma).

We keep doubling b in every recursive invocation, and the base cases break the recursive cycle once b outgrows a. It will take at most steps to reach that point. Therefore, the recursion terminates.