IEEE双重使sqrt（x * x）≠x [英] IEEE double such that sqrt(x*x) ≠ x

问题描述

是否存在IEEE双重 x> 0 ，以便 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 不不涉及四舍五入。那个答案对于这个问题来说是不够的，因为 x * x 可能会在一个方向上涉及四舍五入，然后 sqrt（x * x） 涉及在相同的方向四舍五入，从而产生不完全 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 |。结果是
浮点计算一个/ sqrt（一个 ² + b ² ）的事实总是在
间隔[ -1,1]。当这个值调用
arccos或arcsin时，这样就不需要测试了。要获得更多保证，该物业
已使用Coq证明助理和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.

您的问题（尽管IEEE还规范了十进制浮点数格式和操作）

使用小数2可能是隐含的，而无限制指数范围等同于您的无溢出或下溢限制。

"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 扩展（间隔[ 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双重使sqrt（x * x）≠x的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！