Czy w arytmetyce liczb całkowitych w języku C # a / b / c zawsze równa się a / (b * c)?

Niech a, b i c będą niedużymi dodatnimi liczbami całkowitymi. Czy a / b / c zawsze równa się a / (b * c) z arytmetyką całkowitoliczbową C #? U mnie w C # wygląda to tak:

int a = 5126, b = 76, c = 14;
int x1 = a / b / c;
int x2 = a / (b * c);

Więc moje pytanie brzmi: czy x1 == x2dla wszystkich a, bi c?

Niech \oznaczają dzielenia całkowitego (C # /operatora pomiędzy dwoma intS) i pozwolić /oznaczają zwykły podział matematycznej. Następnie, jeśli x,y,zsą dodatnimi liczbami całkowitymi i ignorujemy przepełnienie ,

(x \ y) \ z
    = floor(floor(x / y) / z)      [1]
    = floor((x / y) / z)           [2]
    = floor(x / (y * z))
    = x \ (y * z)

gdzie

a \ b = floor(a / b)

Skok od wiersza [1]do wiersza [2]powyżej wyjaśniono w następujący sposób. Załóżmy, że masz dwie liczby całkowite ai boraz liczbę ułamkową fw przedziale [0, 1). Łatwo to zobaczyć

floor(a / b) = floor((a + f) / b)  [3]

Jeśli w linii [1]identyfikujesz a = floor(x / y), f = (x / y) - floor(x / y)i b = z, to [3]implikuje to [1]i [2]jesteś równy.

Możesz uogólnić ten dowód na ujemne liczby całkowite (nadal ignorując przepełnienie ), ale zostawię to czytelnikowi, aby zachować prostotę.

Jeśli chodzi o kwestię przepełnienia - zobacz odpowiedź Erica Lipperta, aby uzyskać dobre wyjaśnienie! W swoim wpisie na blogu i odpowiedziach przyjmuje również znacznie bardziej rygorystyczne podejście , na co powinieneś zwrócić uwagę, jeśli uważasz, że jestem zbyt falujący.

To pytanie tak mi się spodobało, że 4 czerwca 2013 r . Uczyniłem je tematem mojego bloga . Dzięki za świetne pytanie!

Duże skrzynie są łatwe do zdobycia. Na przykład:

a = 1073741823; 
b = 134217727;
c = 134217727;

ponieważ b * cprzepełnia do liczby ujemnej.

Dodałbym do tego fakt, że w sprawdzonej arytmetyce różnica między a / (b * c)i (a / b) / cmoże być różnicą między działającym programem a programem, który ulega awarii. Jeśli iloczyn liczby całkowitej bi cprzekracza granice liczby całkowitej, poprzednia ulegnie awarii w sprawdzonym kontekście.

W przypadku małych dodatnich liczb całkowitych, powiedzmy, dostatecznie małych, aby pasowały do ​​skrótu, należy zachować tożsamość.

Timothy Shields właśnie przesłał dowód; Przedstawiam tutaj alternatywny dowód. Załóżmy, że wszystkie liczby są nieujemnymi liczbami całkowitymi i żadna z operacji nie przepełnia się.

Dzielenie liczb całkowitych x / yznajduje wartość qtaką, że q * y + r == x, gdzie 0 <= r < y.

Więc podział a / (b * c)znajduje taką wartość q1, że

q1 * b * c + r1 == a

gdzie 0 <= r1 < b * c

dzielenie ( a / b ) / cnajpierw znajduje wartość qttaką, że

qt * b + r3 == a

a następnie stwierdza wartość q2w taki sposób,

q2 * c + r2 == qt

Więc zastąp to w for qti otrzymamy:

q2 * b * c + b * r2 + r3 == a

gdzie 0 <= r2 < ci 0 <= r3 < b.

Dwie równe sobie rzeczy są sobie równe, więc mamy

q1 * b * c + r1 == q2 * b * c + b * r2 + r3

Załóżmy, że q1 == q2 + xdla jakiejś liczby całkowitej x. Zastąp to w i rozwiąż x:

q2 * b * c + x * b * c + r1 = q2 * b * c + b * r2 + r3
x  = (b * r2 + r3 - r1) / (b * c)

gdzie

 0 <= r1 < b * c
 0 <= r2 < c
 0 <= r3 < b

Czy może xbyć większe niż zero? Nie. Mamy nierówności:

 b * r2 + r3 - r1 <= b * r2 + r3 <= b * (c - 1) + r3 < b * (c - 1) + b == b * c

Zatem licznik tego ułamka jest zawsze mniejszy niż b * c, więc xnie może być większy od zera.

Czy może xbyć mniejsze niż zero? Nie, za pomocą podobnego argumentu pozostawiono czytelnikowi.

Dlatego liczba całkowita xjest równa zero, a zatem q1 == q2.

Jeśli wartości bezwzględne bi csą poniżej około sqrt(2^31)(ok. 46 300), tak aby b * cnigdy się nie przepełniły, wartości zawsze będą zgodne. W przypadku b * cprzepełnienia można zgłosić błąd w checkedkontekście lub uzyskać niepoprawną wartość w uncheckedkontekście.

Unikając błędów przepełnienia zauważonych przez innych, zawsze pasują.

Załóżmy, że to a/b=q1znaczy, że a=b*q1+r1, gdzie 0<=r1<b.
Teraz przypuśćmy, że to a/b/c=q2znaczy, że q1=c*q2+r2, gdzie 0<=r2<c.
To znaczy, że a=b(c*q2+r2)+r1=b*c*q2+br2+r1.
W tym celu a/(b*c)=a/b/c=q2musimy mieć 0<=b*r2+r1<b*c.
Ale b*r2+r1<b*r2+b=b*(r2+1)<=b*cw razie potrzeby te dwie operacje są zgodne.

To nie działa, jeśli są ujemne blub csą ujemne, ale nie wiem, jak działa dzielenie liczb całkowitych w tym przypadku.

Dam własny dowód dla zabawy. To również ignoruje przepełnienie i niestety obsługuje tylko pozytywy, ale myślę, że dowód jest czysty i wyraźny.

Celem jest pokazanie tego

floor(floor(x/y)/z) = floor(x/y/z)

gdzie /jest normalny podział (w całym tym dowodzie).

Przedstawiamy iloraz i resztę z a/b unikalnie as a = kb + r(przez to rozumiemy, że k,rsą unikalne i również zauważalne |r| < |b|). Potem będzie:

(1) floor(x/y) = k => x = ky + r
(2) floor(floor(x/y)/r) = k1 => floor(x/y) = k1*z + r1
(3) floor(x/y/z) = k2 => x/y = k2*z + r2

Więc naszym celem jest po prostu to pokazać k1 == k2. Cóż, mamy:

k1*z + r1 = floor(x/y) = k = (x-r)/y (from lines 1 and 2)
=> x/y - r/y = k1*z + r1 => x/y = k1*z + r1 + r/y

a zatem:

(4) x/y = k1*z + r1 + r/y (from above)
x/y = k2*z + r2 (from line 3)

Teraz obserwujemy z (2), że r1jest to liczba całkowita (for k1*zjest liczbą całkowitą z definicji) i r1 < z(również z definicji). Ponadto z (1) wiemy, że r < y => r/y < 1. Rozważmy teraz sumę r1 + r/yz (4). Twierdzenie jest takie r1 + r/y < zi jest to jasne z poprzednich twierdzeń (ponieważ 0 <= r1 < zi r1jest liczbą całkowitą, więc mamy 0 <= r1 <= z-1. Dlatego 0 <= r1 + r/y < z). Zatem r1 + r/y = r2z definicji r2(w przeciwnym razie byłyby dwie reszty, z x/yktórych jest sprzeczna definicja reszty). Stąd mamy:

x/y = k1*z + r2
x/y = k2*z + r2

i mamy nasz upragniony wniosek k1 = k2.

Powyższy dowód powinien działać z negatywami, z wyjątkiem kilku kroków, które musiałbyś sprawdzić w dodatkowych przypadkach ... ale nie sprawdziłem.

Przykład licznika: INT_MIN / -1 / 2