Abstract

This formalisation provides an executable version of Zimmerman’s Karatsuba Square Root algorithm, which, given an integer m, computes the integer square root floor(sqrt(m)) and the remainder m – floor(sqrt(m))². 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 into four parts and recursively calls itself once on an input with roughly half as many bits as, 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.

BibTeX

@article{Karatsuba_Sqrt-AFP,
  author  = {Manuel Eberl},
  title   = {The {K}aratsuba Square Root Algorithm},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Karatsuba_Sqrt.html},
             Formal proof development},
  ISSN    = {2150-914x},
}