Digit Serial Methods with Applications to Division and Square Root (with mechanically checked correctness proofs)
Numerical Analysis
2017-08-02 v1
Abstract
We present a generic digit serial method (DSM) to compute the digits of a real number . Bounds on these digits, and on the errors in the associated estimates of formed from these digits, are derived. To illustrate our results, we derive such bounds for a parameterized family of high-radix algorithms for division and square root. These bounds enable a DSM designer to determine, for example, whether a given choice of parameters allows rapid formation and rounding of its approximation to . All our claims are mechanically verified using the HOL-Light theorem prover, and are included in the appendix with commentary.
Cite
@article{arxiv.1708.00140,
title = {Digit Serial Methods with Applications to Division and Square Root (with mechanically checked correctness proofs)},
author = {Warren E. Ferguson and Jesse Bingham and Levent Erkök and John R. Harrison and Joe Leslie-Hurd},
journal= {arXiv preprint arXiv:1708.00140},
year = {2017}
}
Comments
32 pages