The Karatsuba Square Root Algorithm

Manuel Eberl 📧

September 18, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This formalisation provides an executable version of Zimmerman's “Karatsuba Square Root” algorithm, which, given an integer $n \geq 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.

License

BSD License

Topics

Session Karatsuba_Sqrt