Thi*_*ler 130 floating-point double floating-accuracy ieee-754
在以下示例中是否可以将除以0(或无穷大)？
public double calculation(double a, double b)
{
if (a == b)
{
return 0;
}
else
{
return 2 / (a - b);
}
}
在正常情况下,它当然不会.但是,如果a并且b非常接近,可能会(a-b)导致0计算的精确性？
请注意,这个问题适用于Java,但我认为它适用于大多数编程语言.
nwe*_*hof 131
在Java中,a - b永远不等于0if a != b.这是因为Java要求支持非规范化数字的IEEE 754浮点运算.从规格:
特别是,Java编程语言需要支持IEEE 754非规范化浮点数和逐渐下溢,这使得更容易证明特定数值算法的期望属性.如果计算结果是非规范化数字,则浮点运算不会"刷新为零".
如果FPU使用非规格化数字,减去不相等的数字永远不会产生零(与乘法不同),也可以看到这个问题.
对于其他语言,它取决于.例如,在C或C++中,IEEE 754支持是可选的.
也就是说,表达式可能2 / (a - b)会溢出,例如with a = 5e-308和b = 4e-308.
mal*_*res 50
作为一种解决方法,以下是什么？
public double calculation(double a, double b) {
double c = a - b;
if (c == 0)
{
return 0;
}
else
{
return 2 / c;
}
}
这样您就不会依赖任何语言的IEEE支持.
Era*_*ran 25
无论值是多少,都不会得到除零a - b,因为浮点除以0不会抛出异常.它返回无穷大.
现在,a == b返回true 的唯一方法是if a和b包含完全相同的位.如果它们仅由最低有效位区别,则它们之间的差异将不为0.
编辑:
正如Bathsheba正确评论的那样,有一些例外:
"不是数字比较"错误与自身,但将具有相同的位模式.
-0.0定义为与+0.0进行比较,并且它们的位模式不同.
因此,如果这两个a和b是Double.NaN,你会到达else子句,但由于NaN - NaN还返回NaN,你将不会被零除.
usr*_*usr 17
没有在这里可以发生除零的情况.
该SMT求解 Z3支持精确IEEE浮点算术.让我们让Z3找到数字a,b这样a != b && (a - b) == 0:
(set-info :status unknown)
(set-logic QF_FP)
(declare-fun b () (FloatingPoint 8 24))
(declare-fun a () (FloatingPoint 8 24))
(declare-fun rm () RoundingMode)
(assert
(and (not (fp.eq a b)) (fp.eq (fp.sub rm a b) +zero) true))
(check-sat)
结果是UNSAT.没有这样的数字.
上面的SMTLIB字符串也允许Z3选择任意舍入模式(rm).这意味着结果适用于所有可能的舍入模式(其中有五个).结果还包括游戏中的任何变量可能是NaN无限的可能性.
a == b被实现为fp.eq质量,使+0f和-0f比较相等.使用零也可以实现与零的比较fp.eq.由于该问题旨在避免被零除,这是适当的比较.
如果使用按位相+0f等-0f来实现相等测试,那将是一种使a - b零的方法.此答案的错误先前版本包含有关好奇的案例的详细信息.
Z3 Online尚不支持FPA理论.使用最新的不稳定分支获得该结果.它可以使用.NET绑定重现如下:
var fpSort = context.MkFPSort32();
var aExpr = (FPExpr)context.MkConst("a", fpSort);
var bExpr = (FPExpr)context.MkConst("b", fpSort);
var rmExpr = (FPRMExpr)context.MkConst("rm", context.MkFPRoundingModeSort());
var fpZero = context.MkFP(0f, fpSort);
var subExpr = context.MkFPSub(rmExpr, aExpr, bExpr);
var constraintExpr = context.MkAnd(
context.MkNot(context.MkFPEq(aExpr, bExpr)),
context.MkFPEq(subExpr, fpZero),
context.MkTrue()
);
var smtlibString = context.BenchmarkToSMTString(null, "QF_FP", null, null, new BoolExpr[0], constraintExpr);
var solver = context.MkSimpleSolver();
solver.Assert(constraintExpr);
var status = solver.Check();
Console.WriteLine(status);
使用Z3回答IEEE浮点问题是很好的,因为它是很难忽视的情况下(如NaN,-0f,+-inf),你可以问任意问题.无需解释和引用规范.您甚至可以询问混合浮点和整数问题,例如"这个特定int log2(float)算法是否正确？".
D K*_*ger 12
提供的函数确实可以返回无穷大:
public class Test {
public static double calculation(double a, double b)
{
if (a == b)
{
return 0;
}
else
{
return 2 / (a - b);
}
}
/**
* @param args
*/
public static void main(String[] args) {
double d1 = Double.MIN_VALUE;
double d2 = 2.0 * Double.MIN_VALUE;
System.out.println("Result: " + calculation(d1, d2));
}
}
输出是Result: -Infinity.
当除法的结果大到存储在double中时,即使分母非零,也返回无穷大.
在符合IEEE-754的浮点实现中,每个浮点类型都可以保存两种格式的数字.一个("标准化")用于大多数浮点值,但它可以表示的第二个最小数字只比最小值小一点,因此它们之间的差异不能用相同的格式表示.另一种("非规范化")格式仅用于在第一种格式中无法表示的非常小的数字.
有效处理非规范化浮点格式的电路是昂贵的,并非所有处理器都包含它.有些处理器提供之间既可以采用具有在非常小的数字操作是一个选择多比运算慢于其他价值,或具有处理器简单地认为这是标准化的格式零过小的数.
Java规范意味着实现应该支持非规范化格式,即使在这样做会使代码运行得更慢的机器上也是如此.另一方面,某些实现可能会提供一些选项,允许代码更快地运行,以换取稍微粗略的值处理,这对于大多数目的来说太小而不重要(在值太小而无关紧要的情况下,它可能令人讨厌的是,使用它们进行计算的时间是计算重要性的十倍,因此在许多实际情况下,齐次归零比慢速但精确的算法更有用.
在IEEE 754之前的旧时代,很可能a!= b并不意味着ab!= 0,反之亦然.这是首先创建IEEE 754的原因之一.
使用IEEE 754 几乎可以保证.允许C或C++编译器以比所需更高的精度执行操作.因此,如果a和b不是变量而是表达式,那么(a + b)!= c并不意味着(a + b) - c!= 0,因为a + b可以用更高的精度计算一次,并且一次没有精度更高.
许多FPU可以切换到一种模式,在这种模式下,它们不会返回非规范化数字,而是将其替换为0.在该模式下,如果a和b是微小的归一化数字,其中差值小于最小归一化数但大于0, != b也不保证== b.
"永远不要比较浮点数"是货物崇拜节目.在拥有"你需要一个epsilon"的口头禅的人中,大多数人都不知道如何正确地选择这个epsilon.