IEEE double 使得 sqrt(x*x) ≠ x [英] IEEE double such that sqrt(x*x) ≠ x

问题描述

在计算x*x 不会上溢或下溢到 Inf、0 或非正规数?

Does there exist an IEEE double x>0 such that sqrt(x*x) ≠ x, under the condition that the computation x*x does not overflow or underflow to Inf, 0, or a denormal number?

假设 sqrt 返回最接近的可表示结果，x*x 也是如此(两者都是 IEEE 标准规定的，平方根运算计算为如果以无限精度计算，然后四舍五入为两个最接近的指定精度的浮点数之一，这些浮点数围绕无限精确的结果").

This is given that sqrt returns the nearest representable result, and so does x*x (both as mandated by the IEEE standard, "square root operation be calculated as if in infinite precision, and then rounded to one of the two nearest floating-point numbers of the specified precision that surround the infinitely precise result").

假设如果存在这样的双打，那么可能有接近1的例子，我写了一个程序来找到这些反例，它没有找到1.0和之间的任何反例1.0000004780981346.

Under the assumption that if such doubles would exist, then there are probably examples close to 1, I wrote a program to find these counterexamples, and it failed to find any between 1.0 and 1.0000004780981346.

上一个类似问题完美平方和浮点数的答案对于 x*x 的计算确实 not 涉及舍入的情况，这个问题是否定的.这个答案对于这个问题是不够的，因为 x*x 可能涉及一个方向的舍入，然后 sqrt(x*x) 可能涉及在一个方向上的舍入same 方向，因此产生的答案不完全是 x.

The previous similar question perfect squares and floating point numbers answers the question in the negative for situations where the computation of x*x does not involve rounding. That answer is not sufficient for this question because it may be possible for x*x to involve rounding in one direction, then sqrt(x*x) to involve rounding in the same direction, thus producing an answer that is not exactly x.

推荐答案

Sylvie Boldo 正式证明满足您问题条件的浮点数不存在.

Sylvie Boldo has formally proved that a floating-point number satisfying the conditions in your question does not exist.

引用文章摘要:

浮点专家知道数学公式可能会失败或在浮点运算中实现时给出不精确的结果.本文描述了一个示例，令人惊讶的是，它是绝对不是这样.实际上，使用基数 2 和无界指数范围，计算一个平方的平方根浮点数 a 正好是 |a|.结果是这样的事实a/sqrt (a² + b²) 的浮点计算总是在区间 [−1, 1].这消除了在调用arccos 或此值的 arcsin.如需更多保证，此物业使用 Coq proof assistant 和 Flocq 进行了正式检查图书馆.结论将提示如果没有会发生什么假设和其他基数，其中行为非常不同.

Floating-point experts know that mathematical formulas may fail or give imprecise results when implemented in floating-point arithmetic. This article describes an example where, surprisingly, it is absolutely not the case. Indeed, using radix 2 and an unbounded exponent range, the computation of the square root of the square of a floating-point number a is exactly |a|. A consequence is the fact that the floating-point computation of a/ sqrt (a² + b²) is always in the interval [−1, 1]. This removes the need for a test when calling an arccos or an arcsin on this value. For more guarantees, this property was formally checked using the Coq proof assistant and the Flocq library. The conclusion will give hints on what happens without assumptions and in other radices, where the behavior is very different.

使用基数 2"可能隐含在您的问题中(尽管 IEEE 也标准化了十进制浮点数格式和操作)，并且无界指数范围"相当于您的无上溢或下溢"限制.

"using radix 2" was likely implicit in your question (although the IEEE has also standardized decimal floating-point number formats and operations), and "an unbounded exponent range" is equivalent to your "no overflow or underflow" restriction.

使该属性成为可能的一个原因是 x*x 以这样的方式扩展"(例如，区间 [1,2] 映射到 [1,4])也就是说，当没有上溢或下溢时，* 可能发生的舍入是良性的，并且 x 仍然是最接近实际平方根的可表示浮点数浮点积 x*x.这种摇摆不定的论点并不构成证明，因此上面链接的文章包含一个证明是一件好事.

A reason making the property possible at all is that x*x "expands" (the interval [1,2] is mapped to [1,4], for instance) in a way such that, when there is no overflow or underflow, the rounding that can happen for * is benign and x is still the closest representable floating-point number to the real square root of the floating-point product x*x. This hand-wavy argument does not constitute a proof, so it's a good thing that the article linked above contains one.

这篇关于IEEE double 使得 sqrt(x*x) ≠ x的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！