为 a+b+c 添加 3 条指令，并进行一次舍入

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在现实世界中实际存在的提示。

有没有包含

add3

的CPU指令集？有语言实现吗？

Answer 1

问题中要求的

err

和

res

由 Jean-Michel Muller 的 Handbook of Floating-Point Arithmetic 中的 Fast2Sum 算法提供 et al，Birkhäuser，2009 年，第 126 页，第 4.3.1 节， “Fast2Sum 算法。”该书将其归功于 1971 年的 Dekker，以及 Kahan 在 1965 年更早出现的操作：

给定一个底数小于或等于 3 的浮点格式，具有次正规数，并且数字

a

和

b

可以用 |

a

| 表示为该格式。 ≥ |

b

|，然后，使用舍入到最接近的值：

s = a+b;
z = s-a;
t = b-z;

计算

s

和

t

，使得

s

是最接近

a

+

b

和

s

+

t

=

a

+

b

的浮点数。 （因此

s

和

t

是问题中要求的

res

和

err

）。

|

a

| ≥ |

b

|绰绰有余；该算法仅要求

a

的浮点指数至少是

b

的指数，但仅仅比较值可能会更容易。因此，完整的实现需要在上述代码之前添加类似

if (fabs(b) > fabs(a)) swap(&a, &b);

的内容。

书上有证明。 （证明有一个勘误表；在不失一般性的情况下，它假设

a

> 0。这可能会在第二版中得到纠正。）

这不提供建议的通用

add3

功能，仅提供特定情况。

add3

由 Boldo 和 Melquiond 的

CorrectRoundedSum3

函数提供（第 201 页，第 6.3.4 节）。它操纵浮点数的编码，从而引发性能和可移植性问题。该操作仅限于递增或递减，因此标准 C

nexttoward

函数可能会代替它，尽管这不一定对性能更好。