a+b+c 的 add3 指令，具有一次舍入

Question

背景

众所周知，两个浮点数的精确乘积并不总是浮点数，但误差exact(a*b) - float(a*b)却是。一些精确乘法的代码通过返回两个数字来利用这一点

res = a * b
err = fma(a, b, -res)

这利用了融合乘加指令，该指令(a*b)+c 通过一次舍入返回表达式。

问题

现在，我想对sums做同样的事情，即

res = a + b
err = add3(a, b, -res)

add3应该返回(a+b)+c 具有一次舍入的表达式。

除了这篇文章之外，我找不到add3现实世界中实际存在的提示。

是否有包含以下内容的CPU指令集add3？有语言实现它吗？

Answer 1

问题中要求的err和是由 Jean-Michel Muller等人的《浮点算术手册》中的 Fast2Sum 算法提供的，Birkh\xc3\xa4user，2009，第 126 页，第 4.3.1 节，\xe2\x80\x9cThe Fast2Sum算法。\xe2\x80\x9d 该书将其归功于 Dekker 于 1971 年提出的算法，其运算最早由 Kahan 在 1965 年提出：res

\n

给定一个底数小于或等于 3 的浮点格式，具有次正规数，以及可以用 | 表示的该格式的数字a和。| \xe2\x89\xa5 | |，然后使用舍入到最接近的值：bab

\n

s = a+b;\nz = s-a;\nt = b-z;\n

\n

计算s且t是最接近+且+ = +s的浮点数。（因此， 和是问题中要求的和。）abstabstreserr

\n

| a| \xe2\x89\xa5 | b| 绰绰有余；该算法仅要求 的浮点指数a至少为 的指数b，但仅仅比较这些值可能会更容易。因此，完整的实现需要类似于if (fabs(b) > fabs(a)) swap(&a, &b);上述代码之前的内容。

\n

书上有证明。（证明有一个勘误表；在不失一般性的情况下，它假设a> 0。这可能会在第二版中得到纠正。）

\n

这不提供建议的一般add3功能，仅提供具体情况。由Boldo 和 Melquiond 第 201 页第 6.3.4 节的函数add3提供。CorrectRoundedSum3它操纵浮点数的编码，从而引发性能和可移植性问题。该操作仅限于递增或递减，因此标准 Cnexttoward函数可能会代替它，尽管这不一定对性能有任何好处。

\n