数字串行方法在除法和平方根中的应用（附有经机械检验的正确性证明）
摘要：一种计算实数V的数字序列的通用方法 (Digit Serial Method, DSM) 被提出。推导出了这些数字的上界，以及由这些数字形成的对V的估计中的误差的上界。为了说明我们的结果，我们推导了一类高基数算法在除法和平方根中的范化族的这些上界。这些上界使得DSM的设计者能够确定，例如，某个参数选择是否允许快速形成和舍入近似值V。我们的所有主张都是用HOL-Light定理证明器进行机械验证的，并在附录中附有注释。
作者：Warren E. Ferguson Jr, Jesse Bingham, Levent Erk"ok, John R. Harrison, and Joe Leslie-Hurd
论文ID：1708.00140
分类：Numerical Analysis
分类简称：cs.NA
提交时间：2017-08-02