The Karatsuba Square Root Algorithm

This formalisation provides an executable version of Zimmerman's “Karatsuba Square Root” algorithm, which, given an integer $n\ge 0$, computes the integer square root $\lfloor \sqrt{n}\rfloor$ and the remainder $n-\lfloor \sqrt{n}{\rfloor }^2$. This is the algorithm used by the GNU Multiple Precision Arithmetic Library (GMP).

Similarly to Karatsuba multiplication, the algorithm is a divide-and-conquer algorithm that works by repeatedly splitting the input number $n$ into four parts and recursively calls itself once on an input with roughly half as many bits as $n$, leading to a total running time of $O(M(n))$ (where $M(n)$ is the time required to multiply two $n$-bit numbers). This is significantly faster than the standard Heron method for large numbers (i.e. more than roughly 1000 bits).

As a simple application to interval arithmetic, an executable floating-point interval extension of the square-root operation is provided. For high-precision computations this is considerably more efficient than the interval extension method in the Isabelle distribution.