floating-point - rango - norme ieee 754

IEEE doble tal que sqrt(x*x) ≠ x

Question

¿Existe un IEEE doble x>0 tal que sqrt(x*x) ≠ x , bajo la condición de que el cálculo x*x no se desborde o subdesborde a Inf , 0 o un número denormal?

Esto se debe a que sqrt devuelve el resultado representable más cercano, y también lo hace x*x (ambos como lo exige el estándar IEEE, "la operación de la raíz cuadrada se calcula como si tuviera una precisión infinita, y luego se redondea a uno de los dos puntos flotantes más cercanos" Números de la precisión especificada que rodean el resultado infinitamente preciso ").

Bajo el supuesto de que si existieran tales dobles, entonces probablemente hay ejemplos cercanos a 1, escribí un programa para encontrar estos contraejemplos, y no pudo encontrar ninguno entre 1.0 y 1.0000004780981346 .

La pregunta similar anterior, los cuadrados perfectos y los números de punto flotante responden a la pregunta en negativo en situaciones donde el cálculo de x*x no implica redondeo. Esa respuesta no es suficiente para esta pregunta porque puede ser posible que x*x implique redondeo en una dirección, luego sqrt(x*x) implique redondeo en la misma dirección, produciendo una respuesta que no sea exactamente x .

Answer 1

Sylvie Boldo ha demostrado formalmente que no existe un número de punto flotante que satisfaga las condiciones de su pregunta.

Citando el resumen del artículo:

Los expertos en puntos flotantes saben que las fórmulas matemáticas pueden fallar o dar resultados imprecisos cuando se implementan en aritmética de punto flotante. Este artículo describe un ejemplo en el que, sorprendentemente, no es el caso. De hecho, al usar la raíz 2 y un rango de exponente ilimitado, el cálculo de la raíz cuadrada del cuadrado de un número de coma flotante a es exactamente | a |. Una consecuencia es el hecho de que el cálculo de punto flotante de a / sqrt (a ² + b ² ) siempre está en el intervalo [−1, 1]. Esto elimina la necesidad de una prueba cuando se llama a arccos o arcsin en este valor. Para obtener más garantías, esta propiedad se verificó formalmente con el asistente de pruebas Coq y la biblioteca Flocq. La conclusión dará pistas sobre lo que sucede sin suposiciones y en otros aspectos, donde el comportamiento es muy diferente.

La "utilización de radix 2" probablemente estuvo implícita en su pregunta (aunque el IEEE también tiene formatos y operaciones de números de punto flotante con valores estandarizados), y "un rango de exponente ilimitado" es equivalente a su restricción de "no desbordamiento o subdesbordamiento".

Una razón que hace que la propiedad sea posible es que x*x “se expande” (el intervalo [1,2] se asigna a [1,4], por ejemplo) de una manera tal que, cuando no hay desbordamiento o subdesbordamiento, el redondeo que puede ocurrir para * es benigno y x sigue siendo el número de punto flotante más cercano a la raíz cuadrada real del producto de punto flotante x*x . Este argumento de mano ondulada no constituye una prueba, por lo que es bueno que el artículo vinculado contiene una.