Email Gateway (Oct 09 2024 at 13:33): Email Gateway (Oct 09 2024 at 13:33):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce yet another contribution by Manuel Eberl: The Karatsuba Square Root Algorithm
Abstract:
This formalisation provides an executable version of Zimmerman's “Karatsuba Square Root” algorithm, which, given an integer n≥0, computes the integer square root and remainder. 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, 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.
It’s online at https://www.isa-afp.org/entries/Karatsuba_Sqrt.html
Larry
Last updated: Jan 04 2025 at 20:18 UTC