atcoder.jp
$X:Y = 16:9$ であるかを判定したいです。こういう問題は（たぶん）何も考えずに浮動小数点型の除算で行う人と、何も考えずに整数型の乗算で行う人に大きく二分される気がします。
今回は、何かしら考えて遊んでみましょうという回です。
クイズ
まずはクイズです。次のうち、今回の問題の制約 $X, Y \in [1\lldot 1000]\cap\Z$ において反例が存在するものはどれでしょう？
fn check0_1(x: f64, y: f64) -> bool { 9.0 * x == 16.0 * y }
fn check0_2(x: f64, y: f64) -> bool { 0.0625 * x == 0.1111111111111111 * y }
fn check1_1(x: f64, y: f64) -> bool { x / y == 16.0 / 9.0 }
fn check1_2(x: f64, y: f64) -> bool { x / 16.0 == y / 9.0 }
fn check1_3(x: f64, y: f64) -> bool { y / x == 9.0 / 16.0 }
fn check1_4(x: f64, y: f64) -> bool { 16.0 / x == 9.0 / y }
fn check2_1(x: f64, y: f64) -> bool { (x * 9.0) / y == 16.0 }
fn check2_2(x: f64, y: f64) -> bool { (x * 9.0) / 16.0 == y }
fn check2_3(x: f64, y: f64) -> bool { (y * 16.0) / x == 9.0 }
fn check2_4(x: f64, y: f64) -> bool { (y * 16.0) / 9.0 == x }
fn check3_1(x: f64, y: f64) -> bool { x * (9.0 / y) == 16.0 }
fn check3_2(x: f64, y: f64) -> bool { x * (9.0 / 16.0) == y }
fn check3_3(x: f64, y: f64) -> bool { y * (16.0 / x) == 9.0 }
fn check3_4(x: f64, y: f64) -> bool { y * (16.0 / 9.0) == x }
上限が小さいので全量を愚直にテストできます。
正解は check3_1 で、$(X, Y) = (784, 441)$ のみが反例でした（！）。
上限が $10^5$ の場合は、check3_3 が反例 $(X, Y) = (1872, 1053)$ を持ちますが、残りの関数たちはいずれも正当でした。
上限が $10^9$ の場合はどうでしょう？
disclaimer: 上限が $10^9$ の場合の正当性について、上記の全部の関数に証明を与えているわけではありません。各関数の最小反例などを挙げているわけでもありません。すいません。
説明
check0_1
fn check0_1(x: f64, y: f64) -> bool { 9.0 * x == 16.0 * y }
check0_1 は整数での判定と同じ形で、$\max{\{9X, 16Y\}}\le 2^{53}$ であれば正当であることがすぐわかります。
$16\otimes Y = 16Y$ から、$\max{\{9X, Y\}}\le 2^{53}$ で正当だと思います。
check2_*
fn check2_1(x: f64, y: f64) -> bool { (x * 9.0) / y == 16.0 }
fn check2_2(x: f64, y: f64) -> bool { (x * 9.0) / 16.0 == y }
fn check2_3(x: f64, y: f64) -> bool { (y * 16.0) / x == 9.0 }
fn check2_4(x: f64, y: f64) -> bool { (y * 16.0) / 9.0 == x }
$2^{53}$ 以下の任意の正整数 $x$, $y$, $m$ について $x/y = m \iff x\oslash y = m$ であることが示せます（下記の記事で示しました（元々は $\floor{x/y} = \floor{x\oslash y}$ だけ示していましたが、今回の記事のために追記しました））。
rsk0315.hatenablog.com
check2_* の右辺が整数であることを踏まえると、check2_* は $\max{\{9X, 16Y\}} \le 2^{53}$ であれば正当であるとわかります。
check1_*
fn check1_1(x: f64, y: f64) -> bool { x / y == 16.0 / 9.0 }
fn check1_2(x: f64, y: f64) -> bool { x / 16.0 == y / 9.0 }
fn check1_3(x: f64, y: f64) -> bool { y / x == 9.0 / 16.0 }
fn check1_4(x: f64, y: f64) -> bool { 16.0 / x == 9.0 / y }
$2^{26}\approx 6.71\times 10^7$ 以下の任意の正整数 $x_1, y_1, x_2, y_2$ について、
$$x_1/y_1 = x_2/y_2 \iff x_1\oslash y_1 = x_2\oslash y_2$$
が成り立つことが示せます（下記の記事で示しました）。
rsk0315.hatenablog.com
よって、check1_* は $\max{\{X, Y\}} \le 2^{26}$ であれば正当であるとすぐわかります。
4 つ中 2 つの値が定数であることを利用すると、もっと広い範囲で正当であることを示せるのかもしれません。
こういうタイプのもの（precision を上げると正当な範囲が広がりそうなもの）は、小さめの precision たちで実験するのが定石です。
実験をしてみましたがよくわかりませんでした。いかがでしたか？
check1_1
- $p$ が $6$ 増えるごとに最小反例が $2^6$ 倍くらいになってそう
- 最小反例の大きさは $p\bmod 6$ に応じて違う事情になってそう
- $\tfrac{16}9$ が $2$ 進法で $6$ 桁周期になっているから？
check1_2, check1_3
- $p$ が $1$ 増えるごとに最小反例が $2$ 倍くらいになってそう
check1_4
- $p$ が $1$ 増えるごとに最小反例が $2$ 倍くらいになってそう
check1_2, check1_3 ほど整った感じではない
どうやら $2^{26}$ よりはもっと広い範囲で正当っぽそうな雰囲気はありました。
check3_2
fn check3_2(x: f64, y: f64) -> bool { x * (9.0 / 16.0) == y }
任意の正整数 $x\le 2^{53}/9$ に対し、$x\otimes (9\oslash 16) = (x\otimes 9) / 16 = 9x/16$ が成り立つことから、$\max{\{9X, Y\}}\le 2^{53}$ で正当であるとわかります。
check0_2, check3_4
fn check0_2(x: f64, y: f64) -> bool { 0.0625 * x == 0.1111111111111111 * y }
fn check3_4(x: f64, y: f64) -> bool { y * (16.0 / 9.0) == x }
$(1\oslash 16)\otimes x \stackrel?= (1\oslash 9)\otimes y$ と $x \stackrel?= (16\oslash 9)\otimes y$ ですが、$16$ が 2 べきであることに注意すると、これらは同値であることがわかります。
ここで、$16\oslash 9 = \tfrac19\cdot(16 - 2^{-50})$ です。よって、
$$
\begin{aligned}
(16\oslash 9)\otimes y
&= (\tfrac19\cdot(16 - 2^{-50}) )\otimes y \\
&= \roundcirc{\tfrac19\cdot(16 - 2^{-50})\cdot y} \\
&= \roundcirc{\tfrac{16}9\cdot y - \tfrac y9\cdot 2^{-50}} \\
\end{aligned}
$$
となります。$\tfrac y9\cdot 2^{-50}$ の誤差項の影響が無視できるうちは正当となります。
exercise: それはどういう範囲か？
exercise: 分母が $9$ の代わりに $49$ だと $y = 49$ が反例になると思うが、今回はなぜ大丈夫なのか？
実験をしたところでは、check1_1 同様に、$p$ が $6$ 増えると最小反例は $2^6$ 倍になっていて、各 $p$ での大きさは $p\bmod 6$ による感じになっていそうでした。
$$
\begin{aligned}
X &= \begin{cases}
2^{p-2}+2, & \text{if~} p \bmod 6 \in\{0, 1\}; \\
112 \cdot \frac{64^{\frac{p-8}6}-1}{63}+48\cdot 64^{\frac{p-8}6} + 2, & \text{if~} p \bmod 6 = 2; \\
2^{p-3}+7, & \text{if~} p \bmod 6 \in\{3, 4\}; \\
7 \cdot \frac{64^{\frac{p-5}6}-1}{63} + 3\cdot 64^{\frac{p-5}6}, & \text{if~} p \bmod 6 = 5
\end{cases} \\
% &= \begin{cases}
% 2^{p-2}+2, & \text{if~} p \bmod 6 \in\{0, 1\}; \\
% \frac{112}{63} \cdot (64^{\frac{p-8}6}-1) + 48\cdot 64^{\frac{p-8}6} + 2, & \text{if~} p \bmod 6 = 2; \\
% 2^{p-3}+7, & \text{if~} p \bmod 6 \in\{3, 4\}; \\
% \frac7{63} \cdot (64^{\frac{p-5}6}-1) + 3\cdot 64^{\frac{p-5}6}, & \text{if~} p \bmod 6 = 5
% \end{cases} \\
&= \begin{cases}
2^{p-2}+2, & \text{if~} p \bmod 6 \in\{0, 1\}; \\
(48 + \frac{16}9) \cdot 64^{\frac{p-8}6} + \frac29, & \text{if~} p \bmod 6 = 2; \\
2^{p-3}+7, & \text{if~} p \bmod 6 \in\{3, 4\}; \\
(3+\frac19) \cdot 64^{\frac{p-5}6} - \frac19, & \text{if~} p \bmod 6 = 5
\end{cases} \\
\end{aligned}
$$
かつ
$$
Y = \begin{cases}
\frac9{16}\cdot(X-2)+1, & \text{if~}p \bmod 6 \in \{0, 1, 2\}; \\
\frac9{16}\cdot(X-7)+4, & \text{if~}p \bmod 6 \in \{3, 4, 5\} \\
\end{cases}
$$
が最小反例になっていそうな雰囲気がありました。
$p = 53$ のとき、
$$
\begin{aligned}
X &= (3+\tfrac19)\cdot 2^{48}-\tfrac19 \\
&= \tfrac19\cdot(7\cdot 2^{50}-1) \\
&= 875699927544263, \\
Y &= \tfrac9{16}\cdot(X-7)+4 \\
% &= \tfrac9{16}\cdot\left((3+\tfrac19)\cdot 2^{48}-\tfrac19-7\right)+4 \\
&= \tfrac9{16} \cdot\tfrac19\cdot(7\cdot 2^{50}-64)+4 \\
&= 7\cdot 2^{46} \\
&= 492581209243648
\end{aligned}
$$
です。実際、この $X$, $Y$ に対して
$$
\tfrac XY = 1.{\small 777777777777777}{\footnotesize 552208655314253}{\scriptsize 9092472621372767(857142{\dots})} \ne \tfrac{16}9
$$
ですが、check0_2 や check3_4 は True を返しました。最小性は示していません。
check3_1, check3_3
fn check3_1(x: f64, y: f64) -> bool { x * (9.0 / y) == 16.0 }
fn check3_3(x: f64, y: f64) -> bool { y * (16.0 / x) == 9.0 }
$(1\oslash 49)\otimes 49 = 1-2^{-53}$ が有名です。
$(X, Y) = (16\cdot 49, 9\cdot 49) = (784, 441)$ が check3_1 の反例でした。
$(1\oslash 117)\otimes 1053 = 9 + 2^{-49}$ です。
$(X, Y) = (16\cdot 117, 9\cdot 117) = (1872, 1053)$ が check3_3 の反例でした。
$(x\oslash y)\otimes z$ は反例がたくさんある形の式に見えます。
rsk0315.hatenablog.com
反例
見つけたうちで最も小さい反例です。最小性はほぼ示していません。
| 関数名 |
$x$ |
$y$ |
check0_1 |
${\small 1000799917193447}$ |
${\small 562949953421314}$ |
check0_2 |
${\small 875699927544263}$ |
${\small 492581209243648}$ |
check1_1 |
${\small 941929333829127}$ |
${\small 529835250278884}$ |
check1_2 |
${\small 1125899906842631}$ |
${\small 633318697598980}$ |
check1_3 |
${\small 1125899906842631}$ |
${\small 633318697598980}$ |
check1_4 |
${\small 750600033020791}$ |
${\small 422212518574195}$ |
check2_1 |
${\small 1000799917193447}$ |
${\small 562949953421314}$ |
check2_2 |
${\small 1000799917193447}$ |
${\small 562949953421314}$ |
check2_3 |
${\small 1125899906842631}$ |
${\small 633318697598980}$ |
check2_4 |
${\small 1125899906842631}$ |
${\small 633318697598980}$ |
check3_1 |
${\small 784}$ |
${\small 441}$ |
check3_2 |
${\small 1000799917193447}$ |
${\small 562949953421314}$ |
check3_3 |
${\small 1872}$ |
${\small 1053}$ |
check3_4 |
${\small 875699927544263}$ |
${\small 492581209243648}$ |
Stern–Brocot 木を用いて、各範囲に含まれる分数を探したりしました。
$$
\begin{aligned}
\tfrac{633318697598981}{1125899906842633} &\in [\tfrac9{16}-2^{-54}\lldot \tfrac9{16}), \\
\tfrac{633318697598980}{1125899906842631} &\in (\tfrac9{16}\lldot \tfrac9{16}+2^{-54}], \\
\tfrac{941929333829127}{529835250278884} &\in [\tfrac{16}9-2^{-53}\lldot\tfrac{16}9), \\
\tfrac{16012798675095097}{9007199254740992} &\in (\tfrac{16}9\lldot\tfrac{16}9+2^{-53}]. \\
\end{aligned}
$$
check1_4 に関しては、x >> 36 == 0x2AAA となる範囲においては（全探索で確認して）最小でしたが、上位 bit は雰囲気で探索したのでよくわかりません。
おまけ
(y * 16.0) * 0.1111111111111111 == x とか (y * 16.0) * (1.0 / x) == 9.0 とかを考え出すとキリがなくなりそうだったのでやめました。
16.0 / x == 9.0 * (1.0 / y) のように左辺と右辺で形が違う場合などを網羅するのは大変です。
あとがき
コンテスト中にこんなもんを考えるくらいなら整数型を使うだろ
↑ 至極真っ当な指摘だなあ 🙄
過去にそういう記事を書いたえびちゃんとしては、制約を見てそういう気分になった日には x / y == 16.0 / 9.0 で解くこともあるかもしれません。Rustacean であるところのえびちゃん的には、f64 だと .0 をつける必要があるのでやっぱり i32 で書くかもしれません。
${}\cdot\tfrac19\cdot{}$ ← 顔文字っぽい
「浮動小数点型を使いましょう」「浮動小数点型はいいぞ」という主張をする気はないんですが、これくらいの簡単な問題で復習をしながら「ふつうは浮動小数点型を避けて整数型で解くけど、浮動小数点型で解けるんだっけ？」とかを考えて練習しておかないと、実際に浮動小数点型を使うことを要求される問題で下手なミスをやらかすんじゃないか？という気はします。とはいえ浮動小数点型を使わされる問題はあまり多くなく、他の数え上げとかを訓練しておいた方がコスパがいいみたいなところもあり、ン〜〜〜という気持ちになります。数え上げより浮動小数点型を要求される問題が多い世界線の AtCoder を見たいかと言われると、まぁ別にそんなことはないですね。推しが人気になると微妙な気持ちになる厄介オタクみたいな心理ですか？
「既知の lemma から、この制約では大丈夫なことを示せます」というのを言える場合でも、「最小反例はこれこれです」というのを示すのは難しい場合が多いです。
「precision を上げてもいくらでも小さい反例があるパターン」と「precision を上げるのに伴って最小反例が大きくなっていくパターン」があり、後者については小さい precision における実験ベースで「た〜ぶんこれくらいの大きさの反例を構成できるんじゃないか？」という遊びができることは多いですが、きちんと示すのは大変な場合が多いんじゃないかなと思っています。
ABC の A 問題くらいをメインで解いている初心者だと、この手の煩雑な議論を追うのは厳しいところがある気がします。
括弧のつけ方ひとつで計算結果（というか証明の大変さ）が大きく異なることはよくあることなので、議論の中身を把握していない初心者に「今回の問題は浮動小数点型でも解けるらしい」という粒度の事実だけが伝わってしまうことはあまりうれしくないんじゃないかなと思っています。
一方で、なにも考えずに「浮動小数点型は使わない方がいいんだよ」とだけ初心者に伝える風潮もなんか違うんじゃないかなぁというような気もしています。
計算量の記法について怪しい記事がたくさんあるのと同様、ちゃんと理解していない人がちゃんと理解しないまま伝承しがちなトピックのひとつだろうなぁとは思っています。
気が向いたらそのうちポエム記事を書くかもしれません。過去のポエム記事でなにを書いたかはあまり覚えていません。
rsk0315.hatenablog.com
おわり
おわりです。
