double において 1.0 / 49.0 * 49.0 < 1.0 が true になることは有名です。
では、一般に x / y * y == x となるのはどういうときでしょうか？ また、その誤差はどのくらいでしょうか？
こうした疑問自体はある程度自然であり、素朴なアルゴリズムの誤差評価の文脈でも出てくるものではあります。 これについて考えていたところ次のような定理を示せたので、今回はそれの話をします。
Theorem: 仮数部が $p$ bits の浮動小数点型において、$x, y\in [1\lldot 2)$ を一様ランダムに選ぶ。このとき、$(x\oslash y)\otimes y = x$ が成り立つ確率は $\ln(4)-\tfrac12+O(2^{-p})$ である。
すなわち、十分大きい $p$ において $0.886294$ 程度の確率で $(x\oslash y)\otimes y = x$ が成り立つということです。
精度を上げても確率 $1$ に近づくわけではなく、たとえば float, double, long double, __float128 のどれであってもほぼ同様の確率でそうなります。
記法
$\roundcirc{x}$ で、実数 $x$ を $p$-bit 仮数部の浮動小数点型に丸めた値を表します。 $x \otimes y$ と $x \oslash y$ で、それぞれ浮動小数点型における乗算 $\roundcirc{xy}$ と除算 $\roundcirc{x/y}$ を表します。
実数 $x\gt 0$ について、$2^e\le x\lt 2^{e+1}$ を満たす唯一の整数 $e$ に対して $\hfloor{x}=2^e$ とします。
観察
（まずは、上記の定理の存在を知らない時点のえびちゃんに遡って、追体験をお届けします。）
浮動小数点数で誤差が問題になる状況において、仮数部の桁数を上げれば解決するものとそうでないものがあります。
$(x\oslash y)\otimes y \ne x$ が成り立つような $(x, y)$ は __float128 でも依然として存在するものですし、今回は後者であろうと予想するのが自然そうです。
そうした状況においては、仮数部が短い浮動小数点型を自前で実装・エミュレートする方法が有効です。 速度が非常に重要になるわけでもないため、四則演算（や FMA や平方根）の correct rounding な実装をするのは比較的容易です。 これらの演算については IEEE 754 下で correct rounding を仮定できるため、ふつうの処理系に関してはそういう前提で考えてよいでしょう。
整数性を使うにあたって便利なので、$[1\lldot 2)$ の代わりに $\{2^{p-1}, \dots, 2^p-1\}$ で考えます。指数部で $2^{p-1}$ 倍の調整をするだけなので一般性は変わりません。
というわけで、$p \in \{4, 5, \dots, 9\}$ で実験してみます。 下方向を $+x$、右方向が $+y$（いわゆる $x$-$y$ で連想する方向を時計回りに $90^\circ$ 回した形）で、$(x\oslash y)\otimes y$ の値で色分けをしています。白が $x$、ピンクが $x-2^{-p}$、赤が $x-2^{-p+1}$、青が $x+2^{-p+1}$ です。
わ、これは何らかの規則性があると見るのが自然でしょう。えびちゃんもこれにはびっくりです。アーチ上の模様が積み重なっているように見えます。
え、こわ、非自明な結果出るのやめてもらっていいですか？ 証明しなきゃいけなくなっちゃうので...
— えびちゃん🍑🍝🦃 (@rsk0315_h4x) 2026年2月27日
え、めちゃこわくなってきた
— えびちゃん🍑🍝🦃 (@rsk0315_h4x) 2026年2月27日
ということで、この規則性っぽい部分について考察すれば、何かしらが求められそうです。
基本的な性質たち
丸めに関して基本的な性質をまとめておきます。改めての証明は行いません。
Property 0.1: $n\in \{2^{p-1}, \dots, 2^p-1\}$, $r\in[0\lldot 1)$ に対して、$x = n+r$ のとき、 $$ \roundcirc{x} = \begin{cases} n, & \text{if~}r \lt \tfrac12; \\ n, & \text{if~}r = \tfrac12 \wedge n \equiv 0 \pmod 2; \\ n+1, & \text{if~} r = \tfrac12 \wedge n \equiv 1 \pmod 2; \\ n+1, & \text{if~} r \gt \tfrac12 \end{cases} $$ が成り立つ。
Property 0.2: $n\in \{2^{p-1}, \dots, 2^p-1\}$, $r\in[0\lldot 1)$ に対して、$x = n+r$ のとき、$|{\roundcirc{x}-x}|\le \tfrac12$ が成り立つ。
考察
Lemma 1: $x, y\in \{2^{p-1}, \dots, 2^p-1\}$ とする。このとき、下記が成り立つ。 $$ (x\oslash y)\otimes y \in \begin{cases} \{x-\tfrac12, x\}, & \text{if~}x = 2^{p-1}; \\ \{x\}, & \text{if~}x \gt 2^{p-1} \wedge x \le y; \\ \{x-1, x, x+1\}, & \text{if~}x \gt 2^{p-1} \wedge x\gt y. \end{cases} $$
Proof
Case 1: $x = 2^{p-1}$.
$x = y$ のとき明らかに $(x\oslash y)\otimes y = x$ であるから、以降 $x\lt y$ とする。このとき $\tfrac12\lt x/y\lt 1$ より $\hfloor{x/y} = \tfrac12$ である。
$2^{p-1}\le x/y\cdot 2^p\lt 2^p$ に注意し、 $$ \begin{aligned} |(x\oslash y)-(x/y)| &= |\roundcirc{x/y\cdot 2^p}\cdot 2^{-p} - x/y| \\ &= |\roundcirc{x/y\cdot 2^p} - x/y\cdot 2^p| \cdot 2^{-p} \\ &\le \tfrac12\cdot 2^{-p} = 2^{-p-1} \end{aligned} $$ が成り立つ。よって、ある $|\delta|\le 2^{-p-1}$ を用いて $x\oslash y = x/y+\delta$ と表せ、 $$ \begin{aligned} (x\oslash y)\otimes y &= (x/y+\delta)\otimes y \\ &= \roundcirc{(x/y+\delta)\cdot y} \\ &= \roundcirc{x+\delta y} \end{aligned} $$ である。$y\lt 2^p$ より $|\delta y| \lt \tfrac12$ であるから、 $$ (x\oslash y)\otimes y = \begin{cases} x-\tfrac12, & \text{if~} -\tfrac12 \lt \delta y \lt -\tfrac14; \\ x, & \text{if~} -\tfrac14 \le \delta y \lt \tfrac12 \end{cases} $$ が成り立つ。
Case 2: $x\gt 2^{p-1} \wedge x\le y$.
Case 1 同様にして $x\lt y$ とする。このとき $\tfrac12\lt x/y\lt 1$ より $\hfloor{x/y} = \tfrac12$ である。
ある $|\delta|\le 2^{-p-1}$ に対して $(x\oslash y)\otimes y = \roundcirc{x+\delta y}$ と表せ、$y\lt 2^p$ より $|\delta y| \lt \tfrac12$ なので $(x\oslash y)\otimes y = x$ が従う。
Case 3: $x\gt 2^{p-1} \wedge x\gt y$.
このとき $1\lt x/y\lt 2$ より $\hfloor{x/y} = 1$ である。
$2^{p-1}\le x/y\cdot 2^{p-1}\lt 2^p$ に注意し、 $$ \begin{aligned} |(x\oslash y)-(x/y)| &= |\roundcirc{x/y\cdot 2^{p-1}}\cdot 2^{-p+1} - x/y| \\ &= |\roundcirc{x/y\cdot 2^{p-1}} - x/y\cdot 2^{p-1}| \cdot 2^{-p+1} \\ &\le \tfrac12\cdot 2^{-p+1} = 2^{-p} \end{aligned} $$ が成り立つ。よって、ある $|\delta|\le 2^{-p}$ に対して$(x\oslash y)\otimes y = \roundcirc{x+\delta y}$ と表せる。 $y\lt 2^p$ より $|\delta y| \lt 1$ であるから、 $$ (x\oslash y)\otimes y \in \{x-1, x, x+1\} $$ が従う。$\qed$
Lemma 2: $x, y\in \{2^{p-1}, \dots, 2^p-1\}$ に対し、$x \gt 2^{p-1}$ かつ $x\gt y$ のとき $(x\oslash y)\otimes y = x-1$ となる必要十分条件は、$r = x\cdot 2^{p-1}\bmod y$ として $$ ( (r\gt 2^{p-2})\wedge (r\lt y-r) )\vee( (r = 2^{p-2})\wedge (x\bmod 2=1) ) $$ である。
Proof
Case 1: $r\lt 2^{p-2}$.
このとき $(x\oslash y)\otimes y = x$ を示す。$r/y \lt 2^{p-2}/2^{p-1} = \tfrac12$ が成り立つ。
ある $q\in\Z$ が存在して $x\cdot 2^{p-1}=qy+r$ と表せる。 $2^{p-1}\le x/y\cdot 2^{p-1}\lt 2^p$ より $$ \begin{aligned} x\oslash y &= \roundcirc{x/y\cdot 2^{p-1}}\cdot 2^{-p+1} \\ &= \roundcirc{q+r/y}\cdot 2^{-p+1} \\ &= q\cdot 2^{-p+1} \end{aligned} $$ であり、$r\cdot 2^{-p+1} \lt \tfrac12$ に注意して $$ \begin{aligned} (x\oslash y)\otimes y &= \roundcirc{qy}\cdot 2^{-p+1} \\ &= \roundcirc{x\cdot 2^{p-1}-r}\cdot 2^{-p+1} \\ &= \roundcirc{x-r\cdot 2^{-p+1}} \\ &= x \end{aligned} $$ が成り立つ。
Case 2: $r = 2^{p-2}$.
このとき $x\bmod 2=0 \iff (x\oslash y)\otimes y = x$ を示す。
Case 1 同様にして $$ \begin{aligned} (x\oslash y)\otimes y &= \roundcirc{x-r\cdot 2^{-p+1}} \\ &= \roundcirc{x-\tfrac12} \end{aligned} $$ であり、Property 0.1 より従う。
Case 3: $r\gt 2^{p-2}$.
このとき $r/y\lt \tfrac12 \iff (x\oslash y)\otimes y = x-1$ を示す。
Case 3-1: $r/y\lt \tfrac12$.
$r\cdot 2^{-p+1} \gt \tfrac12$ に注意しつつ Case 1 同様にして $$ \begin{aligned} (x\oslash y)\otimes y &= \roundcirc{x-r\cdot 2^{-p+1}} \\ &= x-1 \end{aligned} $$ が成り立つ。
Case 3-2: $r/y = \tfrac12$.
これを満たす $(x, y)$ は存在しないことを背理法で示す。
$r = \tfrac y2$ とすると、$x\cdot 2^{p-1} = qy+\tfrac y2$、すなわち $x\cdot 2^p = (2q+1)\cdot y$ が成り立つ。 $x$ は整数であるから左辺は $2^p$ で割り切れるが、$y\lt 2^p$ なので右辺は $2^p$ で割り切れないため矛盾。
Case 3-3: $r/y \gt \tfrac12$.
$2^{p-1}\le x/y\cdot 2^{p-1}\lt 2^p$ より $$ \begin{aligned} x\oslash y &= \roundcirc{x/y\cdot 2^{p-1}}\cdot 2^{-p+1} \\ &= \roundcirc{q+r/y}\cdot 2^{-p+1} \\ &= (q+1)\cdot 2^{-p+1}. \end{aligned} $$ $r\lt y$ より $$ \begin{aligned} (x\oslash y)\otimes y &= ( (q+1)\cdot 2^{-p+1})\otimes y \\ &= \roundcirc{( (q+1)\cdot 2^{-p+1})\cdot y} \\ &= \roundcirc{qy + y}\cdot 2^{-p+1} \\ &= \roundcirc{x\cdot 2^{p-1}+y-r}\cdot 2^{-p+1} \\ &= \roundcirc{x + (y-r)\cdot 2^{-p+1})} \\ &\ge \roundcirc{x}\cdot 2^{-p+1} \\ &= x\cdot 2^{-p+1}. \quad\qed \end{aligned} $$
Lemma 3: $x, y\in \{2^{p-1}, \dots, 2^p-1\}$ に対し、$x \gt 2^{p-1}$ かつ $x\gt y$ のとき $(x\oslash y)\otimes y = x+1$ となる必要十分条件は、$r = x\cdot 2^{p-1}\bmod y$ として $$ ( (y-r\gt 2^{p-2})\wedge (r\gt y-r) )\vee( (y-r = 2^{p-2})\wedge (x\bmod 2=1) ) $$ である。
Proof. Lemma 2 と同様にして示せる。$\qed$
Lemma 4: $x, y\in \{2^{p-1}+1, \dots, 2^p-1\}$ に対し、$r_y(x) = x\cdot 2^{p-1}\bmod y$ とする。
$x\gt y$ とし、正整数 $k$ に対して $\angled{r_y(x), r_y(x+1), \dots, r_y(x+k-1)}$ が下記をすべて満たすとする。
- 各 $0\le i\lt k-1$ に対して $r_y(x+i) \gt r_y(x+i+1)$
- $r_y(x-1) \lt r_y(x)$
- $r_y(x+k-1) \lt r_y(x+k)$
このとき、ちょうど一つの $i\in\{0, 1, \dots, k-1\}$ に対して $( (x+i)\oslash y)\otimes y \ne x+i$ が成り立つ。
Proof
$0\lt y-2^{p-1}\lt 2^{p-1}\lt y$ が成り立つことに注意する。任意の $0\le i\lt k-1$ に対し、 $$ \begin{aligned} r_y(x+i+1) &= (x+i+1)\cdot 2^{p-1}\bmod y \\ &= ( (x+i)\cdot 2^{p-1} + 2^{p-1})\bmod y \\ &= ( (x+i)\cdot 2^{p-1} - (y - 2^{p-1}) )\bmod y \\ &= r_y(x+i) - (y-2^{p-1}) \end{aligned} $$ が成り立つ。よって、$\angled{r_y(x), r_y(x+1), \dots, r_y(x+k-1)}$ は交差 $-(y-2^{p-1})$ の等差数列である。
Case 1: $2^{p-2} \in \{r_y(x), r_y(x+1), \dots, r_y(x+k-1)\}$.
$y - r_y(x+i) = 2^{p-2} \iff r_y(x+i+1) = 2^{p-2}$ であることと $(x+i)\bmod 2 = 1$ と $(x+i+1)\bmod 2 = 1$ のうちどちらか片方のみが成り立つことから従う。
Case 2: $2^{p-2} \notin \{r_y(x), r_y(x+1), \dots, r_y(x+k-1)\}$.
Lemmata 2–3 を踏まえると、$( (x+i)\oslash y)\otimes y\ne x+i$ であることは $r_y(x+i)$ が $\angled{2^{p-2}, \dots, y-2^{p-2}}$ に含まれることと同値である。 $\angled{2^{p-2}, \dots, y-2^{p-2}}$ は連続する $y-2^{p-1}+1$ 個の整数であり、交差 $-(y-2^{p-1})$ であり $2^{p-2}$ を含まない等差数列との共通部分はちょうど 1 つである。$\qed$
Lemma 5: $y\in \{2^{p-1}+1, \dots, 2^p-1\}$ とする。 $(x\oslash y)\otimes y \ne x$ かつ $x\gt 2^{p-1}$ なる $x$ の個数は $-y + 3\cdot 2^{p-1} - 2^{2p-1}/y+O(1)$ 個である。
Proof
下記を満たす連続部分列の個数は、高々 1 つである。
- 各 $0\le i\lt k-1$ に対して $r_y(x+i) \gt r_y(x+i+1)$
- $x-1 = y$
- $r_y(x+k-1) \lt r_y(x+k)$
また、下記についても同様である。
- 各 $0\le i\lt k-1$ に対して $r_y(x+i) \gt r_y(x+i+1)$
- $r_y(x-1) \lt r_y(x)$
- $x+k-1 = 2^p$
これらの連続部分列に対応する $i$ のうち $( (x+i)\oslash y)\otimes y \ne x+i$ となるものは高々 1 つである。
各 $i$ に対して、$q_i$ が存在して $r_y(y+i) = r_y(y) - i(y-2^{p-1}) + q_iy$ が成り立つ。求める値は $q_{2^p-y}+O(1)$ となる。 $$ \begin{aligned} q_{2^p-y}y &= r_y(2^p) - r_y(y) + (2^p-y)(y-2^{p-1}) \\ &= (2^{2p-1}\bmod y) - 0 + (2^p-y)(y-2^{p-1}) \\ &= (2^p-y)(y-2^{p-1}) + O(y) \end{aligned} $$ であり、 $$ \begin{aligned} \frac{(y-2^{p-1})(2^p-y)}y &= \frac{2^p\cdot y - y^2 -2^{2p-1} + 2^{p-1}\cdot y}y \\ &= -y + 3\cdot 2^{p-1} - 2^{2p-1}/y \end{aligned} $$ であるから、 $$ q_{2^p-y} = -y + 3\cdot 2^{p-1} - 2^{2p-1}/y + O(1) $$ となる。$\qed$
Theorem 6: $x, y\in \{2^{p-1}, \dots, 2^p-1\}$ を一様ランダムに選んだとき、$(x\oslash y)\otimes y = x$ となる確率は $\ln(4)-\tfrac12+O(2^{-p}) \approx 0.886294$ である。
Proof
余事象を考える。 まず、Lemma 1 より $( (x\oslash y)\otimes y)-x = -\tfrac12$ なる確率は $O(2^{-p})$ である。
$|( (x\oslash y)\otimes y)-x| = 1$ なる通り数は次の通りである。 $$ \begin{aligned} &\phantom{{}={}} \sum_{y=2^{p-1}+1}^{2^p-1} {-y + 3\cdot 2^{p-1} - 2^{2p-1}/y + O(1)} \\ &= -\tfrac12(2^{p-1}-1)(2^p+2^{p-1}) + 3\cdot 2^{p-1}\cdot (2^{p-1}-1) - 2^{2p-1}\cdot (H_{2^p-1}-H_{2^{p-1}}) + O(1) \\ &= 3\cdot 2^{p-1}\cdot (-\tfrac12(2^{p-1}-1) + (2^{p-1}-1) ) - 2^{2p-1}\cdot (H_{2^p-1}-H_{2^{p-1}}) + O(1) \\ &= 3\cdot 2^{p-1}\cdot \tfrac12(2^{p-1}-1) - 2^{2p-1}\cdot (H_{2^p-1}-H_{2^{p-1}}) + O(1) \\ &= 3\cdot 2^{p-2}\cdot (2^{p-1}-1) - 2^{2p-1}\cdot (H_{2^p-1}-H_{2^{p-1}}) + O(1) \\ &= 3\cdot (2^{2p-3}-2^{p-2}) - 2^{2p-1}\cdot (H_{2^p-1}-H_{2^{p-1}}) + O(1) \\ &= 3\cdot 2^{2p-3} - 2^{2p-1}\cdot (\ln(2^p)-\ln(2^{p-1}) ) + O(2^p) \\ &= 3\cdot 2^{2p-3} - 2^{2p-1}\ln(2) + O(2^p) \\ &= 2^{2(p-1)} \cdot \left(\tfrac32-\ln(4)\right) + O(2^p). \end{aligned} $$ これを $2^{2(p-1)}$ で割って、$\tfrac32-\ln(4)+O(2^{-p})$ を得る。これらより、求める確率は $$ 1-\left(\tfrac32-\ln(4)+O(2^{-p})\right) = \ln(4)-\tfrac12+O(2^{-p}) $$ となる。$\qed$
Claim 7: $y$ を固定したときに $(x\oslash y)\otimes y=x$ となりにくいのは $y=2^{p-1/2}$ のときで、確率は $2\sqrt2-2+O(2^{-p}) \approx 0.828427$ である。
Proof
相加相乗平均の関係に注意して、$|( (x\oslash y)\otimes y)-x| = 1$ なる通り数は $$ \begin{aligned} &\phantom{{}={}} \max_y {(-y + 3\cdot 2^{p-1} - 2^{2p-1}/y)} \\ &= 3\cdot 2^{p-1} - \min_y {(y + 2^{2p-1}/y)} \\ &= 3\cdot 2^{p-1} - 2\cdot (2^{2p-1})^{1/2} \\ &= 3\cdot 2^{p-1} - 2^{p+1/2} \\ &= 3\cdot 2^{p-1} - 2\sqrt 2\cdot 2^{p-1} \\ &= (3-2\sqrt 2)\cdot 2^{p-1} \end{aligned} $$ である。上界を達成するのは $y=2^{p-1/2}$ である。$( (x\oslash y)\otimes y)-x = -\tfrac12$ なる確率は $O(2^{-p})$ であるから、求める確率は $$ 1 - ( (3-2\sqrt 2) + O(2^{-p}) ) = 2\sqrt 2-2 + O(2^{-p}) $$ である。$\qed$
実験
f32, f64, f80, f128 のそれぞれについて $10^9$ 回選んだときの $( (x\oslash y)\otimes y)-x$ は次の通りでした。C++ における f32 の promotion の仕様から、明示的に f32 にキャストする必要があり、そこで二重丸めが起きている気がします。一応ここではおそらくは影響しないはず？
| 型 | $-1$ | $-\tfrac12$ | $0$ | $1$ |
|---|---|---|---|---|
f32 |
$56859910$ | $23$ | $886284147$ | $56855920$ |
f64 |
$56868530$ | $0$ | $886294349$ | $56837121$ |
f80 |
$56863534$ | $0$ | $886292498$ | $56843968$ |
f128 |
$56845181$ | $0$ | $886294978$ | $56859841$ |
綺麗に揃った値になっていてうれしいです。
xyy_count.cpp
#include <iomanip> #include <iostream> #include <map> #include <quadmath.h> #include <random> template <typename F> F random_1_2(std::mt19937& mt) { return F(); } template <> float random_1_2(std::mt19937& mt) { return (mt() & ~(~0u << 23)) | 1u << 23; } template <> double random_1_2(std::mt19937& mt) { unsigned long res = mt(); res <<= 32; res |= mt(); res &= ~(~0uL << 52); res |= 1uL << 52; return res; } template <> long double random_1_2(std::mt19937& mt) { unsigned long res = mt(); res <<= 32; res |= mt(); res |= 1uL << 63; return res; } template <> __float128 random_1_2(std::mt19937& mt) { unsigned __int128 res = mt(); res <<= 32; res |= mt(); res <<= 32; res |= mt(); res <<= 32; res |= mt(); res &= ~(~(unsigned __int128)0u << 112); res |= (unsigned __int128)(1u) << 112; return res; } template <typename F> void count_f(long n) { std::map<F, unsigned long> c; std::cerr << std::fixed << std::setprecision(1); std::random_device rd; std::mt19937 mt(rd()); for (int i = 0; i < n; ++i) { volatile F x = random_1_2<F>(mt); volatile F y = random_1_2<F>(mt); volatile F z = F(x / y) * y; ++c[F(z - x)]; } std::cout << "---\n"; for (auto [x, y]: c) { std::cout << double(x) << '\t' << y << '\n'; } } int main() { long const N = 1e9; count_f<float>(N); count_f<double>(N); count_f<long double>(N); count_f<__float128>(N); }
これに基づいて $\ln(4)$ の値を計算するというギャグも可能そうです。精度はお察しです。
あとがき
この手の命題を示すと、「浮動小数点型は自動正確丸め機能つき整数型であるなあ」のような気持ちになります。整数分野に強い人はこの手の話を簡単に示せそうだなという気がします。示してうれしいかは人によりそうです。
今回の記事は AtCoder Weekday Contest 0014 Beta C についての話を Twitter で見ていたときに考え始めました。
(x/y)*z の形の式について、（無限精度での）xz/y が整数になる場合でも浮動小数点型だと誤差が出るケースが多数存在しますね
— えびちゃん🍑🍝🦃 (@rsk0315_h4x) 2026年2月27日
そういう反例が多数存在しますというふわふわリプライを送りつけ、「そんなふわふわリプライが許されるのか？」という気持ちで調べていました。 実際、無視するとまずそうな比率で存在していそうということがわかってよかったです。
その問題の解説には (非推奨) Claude 4.5 Opus だとか (非推奨) Qwen3-Coder-480B だとかがあり、非推奨ってなんやねんという気持ちにはなりました。Beta ということもあってまぁそのへんはまぁという感じなのかもしれません。
速度を求めるにあたって v = x/y とし、その後で時間を掛けて距離 v*t を求めるようなコードを書くと、今回の記事の形の式になります。
なので、多少の個数の y == t のランダムケースを用意すれば、そのような解法を落とせそうだなぁという感じがします。
仮数部の桁数を上げても解決しない具体的な例を具体的な確率つきで示すことができて、うれしいなという気持ちです。 好きな数を聞かれたら $\ln(4)-\tfrac12$ と答えるようになってしまうかもしれません。
浮動小数点型びっくり命題シリーズとしては下記もありますが、今回のもお気に入りになりそうです。
AtCoder Weekday Contest 0014 Beta B の解説 も浮動小数点型を用いており、こちらの正当性は下記から従う気がします。
おわり
おわりです。
