えびちゃんの日記

えびちゃん（競プロ）の日記です。

5.0 * x == x + x + x + x + x

浮動小数点数

証明

binary64, tiesToEven で考えます。以下、$x$ は有限の浮動小数点数とします。特に、$x$ は NaN ではありません*1。

Claim 1: 任意の $x$ に対し、$x \oplus x = 2 \otimes x = 2x$ が成り立つ。

Proof: 明らか。$\qed$

Claim 2: 任意の $x$ に対し、$(x \oplus x)\oplus x = 3 \otimes x$ が成り立つ。

Proof

$$ \begin{aligned} (x\oplus x)\oplus x &= 2x \oplus x \\ &= \roundcirc{2x+x} \\ &= \roundcirc{3x} \\ &= 3\otimes x. \quad\qed \end{aligned} $$

Claim 3: 任意の $x$ に対し、$( (x\oplus x)\oplus x)\oplus x = 4\otimes x = 4x$ が成り立つ。

Proof

$4\otimes x = 4x$ は明らか。$(3\otimes x) \oplus x = 4x$ を示せばよい。

$x = 0$ の場合は明らかなので、$x\gt 0$ について考える。一般性を失わず $2^{52}\le x\lt 2^{53}$ とする。 ある実数 $|\varepsilon|\le 2^{-53}$ が存在して $3\otimes x = 3x + \hfloor{3x}\cdot\varepsilon$ が成り立つ。

$1.5\cdot 2^{53}\le 3x\lt 1.5\cdot 2^{54}$ より、$\hfloor{3x} = 2^{53}$ または $\hfloor{3x} = 2^{54}$ が成り立つ。

Case 1: $\hfloor{3x} = 2^{53}$

$\varepsilon' = \hfloor{3x}\cdot\varepsilon$ とすると $|\varepsilon'|\le 1$ が成り立つ。

$$ \begin{aligned} (3\otimes x)\oplus x &= (3x + \hfloor{3x}\cdot\varepsilon) \oplus x \\ &= (3x + \varepsilon')\oplus x \\ &= \roundcirc{3x + \varepsilon' + x} \\ &= \roundcirc{4x + \varepsilon'}. \end{aligned} $$

Case 1-a: $x = 2^{52}$

$4x$ 未満で最大の浮動小数点数は、$4x-2$ である。$\roundcirc{4x-1} = 4x$ であるから、$\roundcirc{4x+\varepsilon'}\ge 4x$ である。 また、$4x$ より大きい最小の浮動小数点数は $4x+4$ であるから、$\roundcirc{4x+\varepsilon'}\le 4x$ である。 よって、$\roundcirc{4x+\varepsilon'} = 4x$ である。

Case 1-b: $x \gt 2^{52}$

$4x$ 未満で最大の浮動小数点数は $4x-4$、$4x$ より大きい最小の浮動小数点数は $4x+4$ であるから、Case 1-a 同様にして $\roundcirc{4x+\varepsilon'} = 4x$ である。

Case 2: $\hfloor{3x} = 2^{54}$

$\varepsilon' = \hfloor{3x}\cdot\varepsilon$ とすると $|\varepsilon'|\le 2$ が成り立つ。 また、$2^{54}\le 3x\lt 4x\lt 2^{55}$ であることに注意する。

任意の整数 $2^{54}\le m\lt 2^{55}$ について、 $$ \roundcirc m = \begin{cases} m, & \text{if}\: m \equiv 0 \pmod 8; \\ m-1, & \text{if}\: m \equiv 1 \pmod 8; \\ m-2, & \text{if}\: m \equiv 2 \pmod 8; \\ m+1, & \text{if}\: m \equiv 3 \pmod 8; \\ m, & \text{if}\: m \equiv 4 \pmod 8; \\ m-1, & \text{if}\: m \equiv 5 \pmod 8; \\ m+2, & \text{if}\: m \equiv 6 \pmod 8; \\ m+1, & \text{if}\: m \equiv 7 \pmod 8 \\ \end{cases} $$ が成り立つ。よって $$ 3\otimes x = \roundcirc{3x} = \begin{cases} 3x, & \text{if}\: 3x \equiv 0 \pmod 8; \\ 3x-1, & \text{if}\: 3x \equiv 1 \pmod 8; \\ 3x-2, & \text{if}\: 3x \equiv 2 \pmod 8; \\ 3x+1, & \text{if}\: 3x \equiv 3 \pmod 8; \\ 3x, & \text{if}\: 3x \equiv 4 \pmod 8; \\ 3x-1, & \text{if}\: 3x \equiv 5 \pmod 8; \\ 3x+2, & \text{if}\: 3x \equiv 6 \pmod 8; \\ 3x+1, & \text{if}\: 3x \equiv 7 \pmod 8 \\ \end{cases} $$ であり、$3^{-1} \equiv 3 \pmod 8$ を踏まえて整理して、 $$ \begin{aligned} 3\otimes x &= \begin{cases} 3x, & \text{if}\: x \equiv 0 \pmod 8; \\ 3x-1, & \text{if}\: x \equiv 3 \pmod 8; \\ 3x-2, & \text{if}\: x \equiv 6 \pmod 8; \\ 3x+1, & \text{if}\: x \equiv 1 \pmod 8; \\ 3x, & \text{if}\: x \equiv 4 \pmod 8; \\ 3x-1, & \text{if}\: x \equiv 7 \pmod 8; \\ 3x+2, & \text{if}\: x \equiv 2 \pmod 8; \\ 3x+1, & \text{if}\: x \equiv 5 \pmod 8 \\ \end{cases} \\ &= \begin{cases} 3x, & \text{if}\: x \equiv 0 \pmod 8; \\ 3x+1, & \text{if}\: x \equiv 1 \pmod 8; \\ 3x+2, & \text{if}\: x \equiv 2 \pmod 8; \\ 3x-1, & \text{if}\: x \equiv 3 \pmod 8; \\ 3x, & \text{if}\: x \equiv 4 \pmod 8; \\ 3x+1, & \text{if}\: x \equiv 5 \pmod 8; \\ 3x-2, & \text{if}\: x \equiv 6 \pmod 8; \\ 3x-1, & \text{if}\: x \equiv 7 \pmod 8. \\ \end{cases} \end{aligned} $$

よって、 $$ (3\otimes x) + x = \begin{cases} 4x, & \text{if}\: x \equiv 0 \pmod 8; \\ 4x+1, & \text{if}\: x \equiv 1 \pmod 8; \\ 4x+2, & \text{if}\: x \equiv 2 \pmod 8; \\ 4x-1, & \text{if}\: x \equiv 3 \pmod 8; \\ 4x, & \text{if}\: x \equiv 4 \pmod 8; \\ 4x+1, & \text{if}\: x \equiv 5 \pmod 8; \\ 4x-2, & \text{if}\: x \equiv 6 \pmod 8; \\ 4x-1, & \text{if}\: x \equiv 7 \pmod 8 \\ \end{cases} $$ である。さて、 $$ \begin{aligned} x\equiv 0 \pmod 8 &\implies 4x \equiv 0 \pmod 8, \\ x\equiv 1 \pmod 8 &\implies 4x+1 \equiv 5 \pmod 8, \\ x\equiv 2 \pmod 8 &\implies 4x+2 \equiv 2 \pmod 8, \\ x\equiv 3 \pmod 8 &\implies 4x-1 \equiv 3 \pmod 8, \\ x\equiv 4 \pmod 8 &\implies 4x \equiv 0 \pmod 8, \\ x\equiv 5 \pmod 8 &\implies 4x+1 \equiv 5 \pmod 8, \\ x\equiv 6 \pmod 8 &\implies 4x-2 \equiv 6 \pmod 8, \\ x\equiv 7 \pmod 8 &\implies 4x-1 \equiv 3 \pmod 8 \end{aligned} $$ であるから、 $$ \begin{aligned} (3\otimes x) \oplus x &= \roundcirc{(3\otimes x)+x} \\ &= \begin{cases} 4x, & \text{if}\: x \equiv 0 \pmod 8; \\ (4x+1)-1, & \text{if}\: x \equiv 1 \pmod 8; \\ (4x+2)-2, & \text{if}\: x \equiv 2 \pmod 8; \\ (4x-1)+1, & \text{if}\: x \equiv 3 \pmod 8; \\ 4x, & \text{if}\: x \equiv 4 \pmod 8; \\ (4x+1)-1, & \text{if}\: x \equiv 5 \pmod 8; \\ (4x-2)+2, & \text{if}\: x \equiv 6 \pmod 8; \\ (4x-1)+1, & \text{if}\: x \equiv 7 \pmod 8 \\ \end{cases} \\ &= 4x. \quad\qed \end{aligned} $$

Claim 4: 任意の $x$ に対し、$( ( (x \oplus x)\oplus x)\oplus x)\oplus x = 5 \otimes x$ が成り立つ。

Proof

$$ \begin{aligned} ( ( (x \oplus x)\oplus x)\oplus x)\oplus x &= 4x \oplus x \\ &= \roundcirc{4x+x} \\ &= \roundcirc{5x} \\ &= 5\otimes x. \quad\qed \end{aligned} $$

Claim 5: 任意の $x$ に対し、$( ( ( (x \oplus x)\oplus x)\oplus x)\oplus x)\oplus x = 6 \otimes x$ が成り立つ。

Disproof

$x = 2^{52}+1$ とする。下記が成り立つ。 $$ \begin{aligned} (5\otimes x)\oplus x &= (5x-1)\oplus x \\ &= 6x-2, \\ 6\otimes x &= 6x+2. \quad\qed \end{aligned} $$

おまけ

note: 非正規化数に関しては、frexp を実装するときと同様にして、上記のケースに帰着できるはずです。非正規化数は実質的には固定小数点数なので、なんかいい感じになるはずです。

note: オーバーフローに関しても、なんやかんやでうまくいくはずです。

note: x == -0.0 のケースでも問題ないです。

おわり

「反例がない気はしないんだが」（笑）

*1:“floating-point number” は、無限大は含みますが NaN は含まない用語として定義されていますね。