Início / coding / Perguntas / 79419785
Accepted
Hans Brende
Asked: 2025-02-07 09:36:42 +0800 CST

É sempre verdade que x * y = ((x * y) / y) * y sob a semântica IEEE 754?

  • 772

Dados dois números de ponto flutuante de precisão dupla, finitos e diferentes de zero xe y, é sempre verdade que a igualdade

x * y == ((x * y) / y) * y

mantém a semântica padrão IEEE 754?

Pesquisei programaticamente entre bilhões de possibilidades (inclusive na faixa subnormal) e não consegui encontrar um contraexemplo, mas também não tenho certeza de como provar que a afirmação é verdadeira.

(O que eu sei é que as afirmações mais simples x == (x / y) * ye x == (x * y) / ysão ambas falsas, pois posso facilmente encontrar contra-exemplos para elas.)

floating-point

1 respostas

  1. Best Answer

    Em precisão dupla (binário64), ou seja, precisão de p = 53 bits, tem-se o seguinte contra-exemplo:

    #include <stdio.h>
int main (int argc, char *argv[])
{
  double x = 0x1.0000004000001p+0;
  double y = 0x1.ffffff8000001p+0;
  double r1 = x * y;
  double r2 = ((x * y) / y) * y;
  printf ("r1 = %a\n", r1);
  printf ("r2 = %a\n", r2);
  return 0;
}

    quais saídas

    r1 = 0x1p+1
r2 = 0x1.fffffffffffffp+0

    Encontrei esse contra-exemplo fazendo testes exaustivos (a propriedade não depende do expoente de x e y, que pode ser definido como uma constante) em pequenas precisões com GNU MPFR , e encontrei um padrão: na precisão p = 2k+3, o seguinte par escrito na base 2 é um contra-exemplo:

    x = 1.0{k}10{k}1
y = 1.1{k}00{k}1

    onde {k}significa que o dígito é repetido k vezes.

    Nota: Este problema é um pouco similar ao que gerou um bug no GNU Emacs + Cairo, onde a expressão ((1/s)*b)*s)está envolvida. Veja meu artigo .

    • 8

relate perguntas