走向实数API

2020-10-07 14:38:23

上一次我们看到,即使在由专家构建的科学计算应用程序中,浮点数的问题也是司空见惯的。浮点表示的特性也出现在更多的日常应用程序中,如计算器和电子表格。在这里,用户基础不太倾向于同情:

如果算术计算和结果直接向非浮点专家的人类用户公开,则浮点近似往往被视为错误。

汉斯-J。今天这篇论文的作者Boehm应该知道,因为他参与了Android计算器应用程序的开发。该应用程序会受到“大量(公开的)用户反馈”的影响,在2014年基于浮点的计算器中,会出现与不准确的结果、不必要的零等相关的错误报告。

这是一个经典的软件开发时刻。这个bug/功能请求表面上看起来就像任何其他普通问题,但从简单的实现到内部的研究级问题!在这种情况下,意识到你不能再只使用标准的IEEE浮点运算了。

对于计算器、电子表格和许多其他应用程序,我们不需要硬件浮点运算的原始性能。但是真正方便的是一个符合日常数学期望的实现。这样的实现是今天论文选择的主题。

据我们所知,这是对实用的通用实数类型的首次探索,它既反映了实数的数学定律,又支持在通常预期的情况下进行精确比较。

结果库以开源形式提供,打包在Android Calculator应用程序中,安装数量超过5亿。自从这一改变以来,“我们不再收到关于不准确结果错误报告,…。我们也没有看到关于不必要的零或类似的投诉。我们也没有收到关于完成计算所需时间长短的投诉。“。

显示的结果决不会暴露大于或等于最后显示的数字中的1的错误(对于中间结果,这可能需要极高的精度)

结果应该显示正确的四舍五入或截断的值,没有错误,滚动时前几位数字保持不变(例如,不要以17.0000开头,然后在滚动时必须显示16.999999999)。

除第一个约束外,所有这些约束都要求我们能够对值执行精确比较。

现代CPU内核每秒可执行数十亿次浮点运算(GFLOPS)。但这是有代价的:

可能无法满足预期的数学属性。例如,加法不再具有关联性:$(x+1)-1$可能与$x+(1-1)$非常不同;从0开始并将0.1相加100次可能不等于10.0。

结果不会像用户预期的那样显示,例如,使用IEEE双精度和JAVA输出格式化规则,$0.1+0.7=0.79999999999999999$,而不是预期的0.8%。

精度限制使得很难根据需要计算小的有限差,例如在计算导数时。

要证明计算没有超过浮点限制,所需的分析不是微不足道的。没有复合表达式的保证,可能很难为这些表达式获得任何合理的误差界。

在IEEE浮点运算中,实数表示为尾数$m$和指数$e$的形式$m\x 2^e$的有理近似。要返回到行为类似于实数的浮点数,我们需要不同的表示形式。这一点的基础是递归实数运算。

实数$x$被表示为将误差容限$e$映射到有理数$f_x(E)$的可计算函数$f_x$,使得$x$和$f_x(E)$之间的差小于误差容限$e$。这可以看作是从建设性的实数分析中得到的实数的实现。

上面的方案提供了任意精度,但不允许我们测试等价性。如果两个数字具有相同的表示法,它们是否相等?通过越来越精确地评估,如果它们不同,我们最终会发现不同之处,但如果它们相等,这个过程永远不会结束。看起来我们有个小问题:

很容易证明两个任意递归实数是否相等是不可判定的。

我们真的想问一个研究较少的交替问题:我们能否通过以下运算的组合来决定从整数常量计算出的递归实数的等式,这些运算我们将称为计算器运算:(1)四种基本算术运算和平方根;(2)sin、cos和tan三角函数及其逆函数;以及(3)指数函数和(自然)对数函数。(1)四个基本算术运算和平方根;(2)sin、cos和tan三角函数及其逆函数;以及(3)指数和(自然)对数函数。

事实证明,基于Richardson和Fitch在1994年给出的方法,初等函数和常数的恒等式问题,这个问题确实是可解的。

这些思想被打包在一个API下,该API支持预期的算术、三角、指数和对数函数以及平方根。有一个总是可以使用的近似比较运算符,但是如果两个数字在近似公差范围内,则可能会错误地认为它们相等。然后,当isCompable()返回true时,可以安全地使用精确比较运算符。关键是要确保isCompable()在尽可能多的情况下返回true。其他助手函数支持截断和确定准确表示结果所需的位数。

我们发现,只需惊人的少量工作,我们就可以确保isCompable()在大多数常见情况下返回TRUE。与递归实数的情况一样,所有的算术运算在逻辑上都会产生精确的答案。因此,标准的数学特性(如关联性)保持不变。只要只使用精确比较来测试相等性,并且仅当isCompare()和ExctlyTruncatable()结果为真时才使用比较和toStringTruncated,则所有操作都符合正常的数学规则。

RrProperty是一个参数化的标记字段,它告诉我们处理的是哪种实数。这是能够尽可能频繁地进行精确比较的关键。

这些字段表示的实数是ratfactor和rrfactor的算术积。Arg中有rrPropertytag指示rrfactor恰好为1或$\pi$,而Arg中的参数化标记指示rrfactor恰好为$\sqrt{arg}$、$e^{arg}$、$\ln(Arg)$、$\log_{10}(Arg)$、$\sin(\pi arg)$、$\tan(\pi arg)$、$\arcsin(Arg)$或$\arctan(Arg)$。最后,有一个标记值指示rrfactor是无理的。

我们的属性概念的优势在于,它支持足够的符号操作,以允许在大多数有趣的情况下进行可判断性比较。它似乎与经典数论的结果惊人地吻合。

您可以在本文的6.1节中找到算法的完整描述。最有趣的步骤是确定独立检查,它试图使用属性标记中的信息来证明递归实数都不是其他递归实数的有理倍数。

…。只要我们能产生描述被比较数的递归实部的性质,我们通常就能保证精确比较的收敛性。

如果两个论元具有相同的递归实因子,则比较因子和有理因子的符号。

如果两个论点具有相同的理性因素和相同类型的属性,则比较属性论点。

如果以上都不适用,则将有理和递归实数相乘作为递归实数,然后比较越来越精确的近似,直到它们不同为止。

Android计算器应用程序安装5亿次,没有任何与浮点行为相关的错误报告,这是一个相当好的评估!操作在不到一毫秒内完成,虽然没有GFLOPS性能,但对于许多应用程序来说肯定足够好了。总而言之,实现大约有6,000行代码。

§7.3中描述的Reals包的一个很好的用法是测试由java.lang.Math包和Java双精度除法提供的数学函数。令人振奋的是,我们只发现了一个轻微的违反Hypot()精度规范…的情况。";

我们已经论证过,可以实现一个在计算上有用的类型,该类型共享实数的基本数学属性,以及通常期望的属性,即在最常见的情况下,我们可以确定一对这样的数是否等于…。使用计算器算术的经验表明,应该避免让非专家用户接触到明显显示浮点舍入的结果。这提供了一种原则性的方法来避免这种情况。