等式的加法属性对浮点数有效吗？

问题描述

也就是说，如果我有两个浮点数（IEEE-754二进制浮点数）a和b，并且我按如下方式计算c：

c = a - b

这总是真的吗？

c + b == a

这个简单问题的答案很难在网上找到答案。我找到的最接近的东西是this paper。也许我只是没有使用正确的术语。

解决方法

您肯定需要添加一些条件（不包括溢出）。此Java程序显示“ false”。

public strictfp class Test {
    public static void main(String[] args) {
        double a = Double.MAX_VALUE;
        double b = -Double.MAX_VALUE;
        double c = a-b;
        System.out.println(c+b == a);
    }
}

实数运算中的

a-b是最大有限两倍的两倍。在浮点算法中，它溢出到无穷大。

,

我的假设是，该问题与使用IEEE-754二进制浮点算术进行的计算有关。

虽然测试不能证明假设的属性，但可以通过找到反例轻松地反驳一个假设。在这种情况下，我们甚至不需要走太远，因为我们可以手工找出一个失败的案例。因为IEEE-754浮动格式具有有限的精度，所以对于非零的a和b，其大小与| a |足够不同。 b |，并且在没有上溢和下溢的情况下，先c == -b，然后再c+b == 0 != a。

以下简单的ISO-C99测试程序可以找到这种情况和其他情况：

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <string.h>
#include <float.h>
#include <math.h>

// Fixes via: Greg Rose,KISS: A Bit Too Simple. http://eprint.iacr.org/2011/007
static unsigned int z=362436069,w=521288629,jsr=362436069,jcong=123456789;
#define znew (z=36969*(z&0xffff)+(z>>16))
#define wnew (w=18000*(w&0xffff)+(w>>16))
#define MWC  ((znew<<16)+wnew)
#define SHR3 (jsr^=(jsr<<13),jsr^=(jsr>>17),jsr^=(jsr<<5)) /* 2^32-1 */
#define CONG (jcong=69069*jcong+13579)                     /* 2^32 */
#define KISS ((MWC^CONG)+SHR3)

float __uint32_as_float (uint32_t a)
{
    float r;
    memcpy (&r,&a,sizeof r);
    return r;
}

int main (void)
{
    const float ULMT = sqrtf (FLT_MAX) / 2; // avoid overflow
    const float LLMT = sqrtf (FLT_MIN) * 2; // avoid underflow
    const uint64_t N = 1ULL << 10;    
    uint64_t count = 0LL;
    uint32_t ai,bi;
    float af,bf,cf,sum;
   
    do {
        do {
            ai = KISS;
            af = __uint32_as_float (ai);
        } while (!isfinite(af) || (fabsf (af) > ULMT) || (fabsf (af) < LLMT));
        do {
            bi = KISS;
            bf = __uint32_as_float (bi);
        } while (!isfinite(bf) || (fabsf (bf) > ULMT) || (fabsf (bf) < LLMT));
        
        cf = af - bf;
        sum = cf + bf;
        if (sum != af) {
            printf ("a!=c+b:  a=% 15.6a  b=% 15.6a c=% 15.6a  b+c=% 15.6a\n",af,sum);
        }
        count++;
    } while (count < N);
    return EXIT_SUCCESS;
}