Digit Serial Methods with Applications to Division and Square Root (with mechanically checked correctness proofs)
| Autor: | Ferguson, Warren E., Bingham, Jesse, Erk��k, Levent, Harrison, John R., Leslie-Hurd, Joe |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: | |
| Popis: | We present a generic digit serial method (DSM) to compute the digits of a real number $V$ . Bounds on these digits, and on the errors in the associated estimates of $V$ 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 $V$. All our claims are mechanically verified using the HOL-Light theorem prover, and are included in the appendix with commentary. 32 pages |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|