Czy można uzyskać 0, odejmując dwie nierówne liczby zmiennoprzecinkowe?

Czy w poniższym przykładzie można uzyskać dzielenie przez 0 (lub nieskończoność)?

public double calculation(double a, double b)
{
     if (a == b)
     {
         return 0;
     }
     else
     {
         return 2 / (a - b);
     }
}

W normalnych przypadkach oczywiście nie. Ale co jeśli ai bsą bardzo bliskie, może (a-b)skutkować 0precyzją obliczeń?

Zwróć uwagę, że to pytanie dotyczy Javy, ale myślę, że będzie dotyczyło większości języków programowania.

W Javie a - bnigdy nie jest równe 0if a != b. Dzieje się tak, ponieważ Java wymusza operacje zmiennoprzecinkowe IEEE 754, które obsługują zdenormalizowane liczby. Ze specyfikacji :

W szczególności język programowania Java wymaga obsługi zdenormalizowanych liczb zmiennoprzecinkowych IEEE 754 i stopniowego niedomiaru, co ułatwia udowodnienie pożądanych właściwości poszczególnych algorytmów numerycznych. Operacje zmiennoprzecinkowe nie są „wyrównywane do zera”, jeśli obliczony wynik jest liczbą zdenormalizowaną.

Jeśli FPU działa z liczbami zdenormalizowanymi , odejmowanie liczb nierównych nigdy nie daje zera (w przeciwieństwie do mnożenia), zobacz także to pytanie .

W przypadku innych języków to zależy. Na przykład w C lub C ++ obsługa IEEE 754 jest opcjonalna.

Mimo to, możliwe jest w celu ekspresji 2 / (a - b)do przelewu, na przykład z a = 5e-308a b = 4e-308.

Jako obejście, co z następującymi?

public double calculation(double a, double b) {
     double c = a - b;
     if (c == 0)
     {
         return 0;
     }
     else
     {
         return 2 / c;
     }
}

W ten sposób nie polegasz na obsłudze IEEE w żadnym języku.

Nie otrzymasz dzielenia przez zero, niezależnie od wartości a - b, ponieważ dzielenie zmiennoprzecinkowe przez 0 nie zgłasza wyjątku. Zwraca nieskończoność.

Teraz jedynym sposobem a == bzwrócenia prawdy jest, jeśli ai bzawierają dokładnie te same bity. Jeśli różnią się tylko najmniej znaczącym bitem, różnica między nimi nie będzie wynosić 0.

EDYTOWAĆ :

Jak słusznie skomentowała Batszeba, są pewne wyjątki:

1. „Żadna liczba nie porównuje” fałszu ze sobą, ale będzie miała identyczne wzorce bitowe.

2. -0,0 jest definiowane w celu porównania prawdy z +0,0, a ich wzory bitowe są różne.

Więc jeśli oba ai bsą Double.NaN, osiągniesz klauzulę else, ale ponieważ NaN - NaNrównież zwraca NaN, nie będziesz dzielić przez zero.

Nie ma przypadku, w którym może wystąpić tutaj dzielenie przez zero.

SMT Solver Z3 umożliwia precyzyjną IEEE zmiennoprzecinkowych arytmetycznych. Poprośmy Z3 o znalezienie liczb ai btakie, że 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)

Wynik jest UNSAT. Nie ma takich numerów.

Powyższy ciąg SMTLIB pozwala również Z3 na wybranie dowolnego trybu zaokrąglania ( rm). Oznacza to, że wynik zachowuje się dla wszystkich możliwych trybów zaokrąglania (z których jest pięć). Wynik obejmuje również możliwość, że dowolna ze zmiennych w grze może być NaNnieskończona.

a == bjest wdrażany jako fp.eqjakość, aby +0fi -0fporównać równe. Porównanie z zerem jest również realizowane za pomocą fp.eq. Ponieważ pytanie ma na celu uniknięcie dzielenia przez zero, jest to właściwe porównanie.

Gdyby test równości został zaimplementowany przy użyciu równości bitowej +0fi -0fbyłby sposobem na zrobienie a - bzera. Niepoprawna poprzednia wersja tej odpowiedzi zawiera szczegółowe informacje dotyczące trybu dla ciekawskich.

Z3 Online nie wspiera jeszcze teorii FPA. Wynik ten uzyskano przy użyciu najnowszej niestabilnej gałęzi. Można go odtworzyć za pomocą powiązań .NET w następujący sposób:

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);

Korzystanie Z3 odpowiedzieć na pytania IEEE pływak jest dobre, bo trudno jest przeoczyć przypadków (takich jak NaN, -0f, +-inf) i można zadać dowolne pytania. Nie ma potrzeby interpretowania i cytowania specyfikacji. Możesz nawet zadawać mieszane pytania typu float i integer, takie jak „czy ten konkretny int log2(float)algorytm jest poprawny?”.

Dostarczona funkcja może rzeczywiście zwrócić nieskończoność:

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)); 
    }
}

Wynik jest Result: -Infinity.

Gdy wynik dzielenia jest zbyt duży, aby można go było zapisać w postaci podwójnej, zwracana jest nieskończoność, nawet jeśli mianownik jest różny od zera.

W implementacji zmiennoprzecinkowej, która jest zgodna z IEEE-754, każdy typ zmiennoprzecinkowy może przechowywać liczby w dwóch formatach. Jeden („znormalizowany”) jest używany dla większości wartości zmiennoprzecinkowych, ale druga najmniejsza liczba, którą może reprezentować, jest tylko odrobinę większa od najmniejszej, więc różnica między nimi nie jest reprezentowana w tym samym formacie. Drugi („zdenormalizowany”) format jest używany tylko dla bardzo małych liczb, których nie można przedstawić w pierwszym formacie.

Obwody do wydajnej obsługi zdenormalizowanego formatu zmiennoprzecinkowego są drogie i nie wszystkie procesory go obejmują. Niektóre procesory oferują wybór między operacjami na naprawdę małych liczbach, które są znacznie wolniejsze niż operacje na innych wartościach, lub zmuszaniem procesora do traktowania liczb, które są zbyt małe dla znormalizowanego formatu, jako zero.

Ze specyfikacji Java wynika, że ​​implementacje powinny obsługiwać zdenormalizowany format, nawet na komputerach, na których spowodowałoby to wolniejsze działanie kodu. Z drugiej strony jest możliwe, że niektóre implementacje mogą oferować opcje pozwalające na szybsze działanie kodu w zamian za nieco niechlujną obsługę wartości, które dla większości celów byłyby zbyt małe, aby mieć znaczenie (w przypadkach, gdy wartości są zbyt małe, aby mieć znaczenie, może być irytujące, że obliczenia z nimi trwają dziesięć razy dłużej niż obliczenia, które mają znaczenie, więc w wielu praktycznych sytuacjach wyrównanie do zera jest bardziej przydatne niż powolna, ale dokładna arytmetyka).

W dawnych czasach przed IEEE 754 było całkiem możliwe, że a! = B nie implikowało ab! = 0 i na odwrót. To był jeden z powodów, dla których stworzono IEEE 754 w pierwszej kolejności.

W przypadku IEEE 754 jest to prawie gwarantowane. Kompilatory C lub C ++ mogą wykonywać operacje z większą precyzją niż jest to potrzebne. Więc jeśli a i b nie są zmiennymi, ale wyrażeniami, to (a + b)! = C nie implikuje (a + b) - c! = 0, ponieważ a + b można obliczyć raz z większą dokładnością, a raz bez wyższa precyzja.

Wiele jednostek FPU można przełączyć w tryb, w którym nie zwracają one zdenormalizowanych liczb, ale zastępują je 0. W tym trybie, jeśli a i b są małymi znormalizowanymi liczbami, w których różnica jest mniejsza niż najmniejsza znormalizowana liczba, ale większa niż 0, a ! = b również nie gwarantuje a == b.

„Nigdy nie porównuj liczb zmiennoprzecinkowych” to kultowe programowanie cargo. Wśród ludzi, którzy mają mantrę „potrzebujesz epsilon”, większość nie ma pojęcia, jak właściwie wybrać ten epsilon.

Przychodzi mi na myśl przypadek, w którym mógłbyś to spowodować. Oto analogiczna próbka o podstawie 10 - tak naprawdę zdarzy się to oczywiście w przypadku podstawy 2.

Liczby zmiennoprzecinkowe są przechowywane mniej więcej w notacji naukowej - to znaczy zamiast widzieć 35,2, przechowywana liczba byłaby bardziej jak 3,52e2.

Wyobraź sobie dla wygody, że mamy jednostkę zmiennoprzecinkową, która działa w oparciu o podstawę 10 i ma 3 cyfry dokładności. Co się stanie, gdy odejmiesz 9,99 od 10,0?

1.00e2-9.99e1

Shift, aby nadać każdej wartości ten sam wykładnik

1,00e2-0,999e2

Zaokrąglij do 3 cyfr

1.00e2-1.00e2

O o!

To, czy może się to ostatecznie zdarzyć, zależy od projektu FPU. Ponieważ zakres wykładników podwójnej jest bardzo duży, sprzęt musi w pewnym momencie zaokrąglić wewnętrznie, ale w powyższym przypadku tylko 1 dodatkowa cyfra wewnętrznie zapobiegnie problemowi.

Nie powinieneś nigdy porównywać liczb zmiennoprzecinkowych lub podwójnych dla równości; ponieważ nie możesz naprawdę zagwarantować, że liczba przypisana do liczby zmiennoprzecinkowej lub podwójnej jest dokładna.

Aby porównać wartości zmiennoprzecinkowe pod kątem równości, musisz sprawdzić, czy wartość jest „wystarczająco zbliżona” do tej samej wartości:

if ((first >= second - error) || (first <= second + error)

Dzielenie przez zero jest nieokreślone, ponieważ granica od liczb dodatnich ma tendencję do nieskończoności, a granica od liczb ujemnych do ujemnej nieskończoności.

Nie jestem pewien, czy jest to C ++ czy Java, ponieważ nie ma tagu języka.

double calculation(double a, double b)
{
     if (a == b)
     {
         return nan(""); // C++

         return Double.NaN; // Java
     }
     else
     {
         return 2 / (a - b);
     }
}

Podstawowym problemem jest to, że komputerowa reprezentacja liczby podwójnej (czyli liczby zmiennoprzecinkowej lub liczby rzeczywistej w języku matematycznym) jest błędna, gdy masz „za dużo” dziesiętnego, na przykład gdy masz do czynienia z liczbą podwójną, której nie można zapisać jako wartość liczbowa ( pi lub wynik 1/3).

Zatem a == b nie można zrobić z żadną podwójną wartością a i b, jak sobie radzić z a == b, gdy a = 0,333 i b = 1/3? W zależności od twojego systemu operacyjnego, FPU, liczby, języka i liczby 3 po 0, będziesz mieć wartość prawda lub fałsz.

W każdym razie, jeśli wykonujesz „obliczanie podwójnej wartości” na komputerze, musisz poradzić sobie z dokładnością, więc zamiast robić a==b, musisz zrobić absolute_value(a-b)<epsilon, a epsilon odnosi się do tego, co modelujesz w tym czasie w swoim algorytmie. Nie możesz mieć wartości epsilon dla całego podwójnego porównania.

W skrócie, kiedy wpisujesz a == b, masz wyrażenie matematyczne, którego nie można przetłumaczyć na komputerze (dla dowolnej liczby zmiennoprzecinkowej).

PS: bum, wszystko, na co tu odpowiadam, jest mniej więcej w odpowiedziach i komentarzach innych.

Na podstawie odpowiedzi @malarres i komentarza @Taemyr, oto mój mały wkład:

public double calculation(double a, double b)
{
     double c = 2 / (a - b);

     // Should not have a big cost.
     if (isnan(c) || isinf(c))
     {
         return 0; // A 'whatever' value.
     }
     else
     {
         return c;
     }
}

Chodzi mi o to, aby powiedzieć: najłatwiejszym sposobem sprawdzenia, czy wynikiem podziału jest nan, czy inf, jest faktycznie wykonanie podziału.