TwoSumの証明に2週間かかった

前に「浮動小数点数小話」という同人誌を出しましたが、私としては浮動小数点数についてもっとちゃんとした本をいずれ出したいと思っています。執筆に着手するのは早い方が良いので、浮動小数点数についてのまとめノートみたいものを書き始めています。

「小話」や今度出る「Binary Hacks Rebooted」には例外だとかハードウェア寄りの話題を多く盛り込みました。一方で、浮動小数点数を極める上では、浮動小数点数に関する数学的な定理も扱いたいです。

浮動小数点数について成り立つ数学的な定理にはどのようなものがあるでしょうか。以前「浮動小数点数の丸めの相対誤差を計算機イプシロンで評価する」に書いたような、誤差を不等式で評価するものがあります。一方で、浮動小数点数を巧妙なやり方で足し引きすると、誤差のない等式を示すことができる場合があります。

例えば、FastTwoSumというアルゴリズムがあります。一定の条件（基数が3以下、非正規化数を含む、最近接丸めが使用される）の下で u の指数部が v の指数部以上であれば

  1. s := u + v（浮動小数点数としての和）
  2. z := s - u（浮動小数点数としての差）
  3. t := v - z（浮動小数点数としての差）

で計算した s と t は（オーバーフローが発生しなければ）数学的な等式として \(u+v=s+t\) を満たします。つまり、s は真の和 \(u+v\) に対して誤差を含むかもしれませんが、その誤差自体を t として厳密に計算することができるのです。

FastTwoSumは事前にオペランドの（指数部の）大小がわかっている必要があり、また、十進には使えません。そのような場合に使えるアルゴリズムとして、TwoSumがあります。これは入力 u と v に対して

  1. s := u + v（浮動小数点数としての和）
  2. u' := s - v（浮動小数点数としての差）
  3. v' := s - u'（浮動小数点数としての差）
  4. delta_u := u - u'（浮動小数点数としての差）
  5. delta_v := v - v'（浮動小数点数としての差）
  6. t := delta_u + delta_v（浮動小数点数としての和）

で計算した s と t が（オーバーフローが発生しなければ）数学的な等式として \(u+v=s+t\) を満たすというものです。

TwoSumはKnuth（TAoCP vol2）やMøllerによって（独立に？）提案されたようです。「Handbook of Floating-Point Arithmetic」や「精度保証付き数値計算の基礎」でもこのアルゴリズムが紹介されています。

さて、Knuthの本ではこの定理は「指数オーバーフロー／アンダーフローが起きないとして」と書かれています。しかし、IEEE 754のような非正規化数を持つ体系であれば足し算・引き算からなるアルゴリズムでアンダーフローの悪影響は受けないような気がします。定理の成り立つ条件に疑念が生じたらどうするか？そう、証明を追えばいいですね。

しかし、「Handbook of 〜」や「精度保証付き〜」にはこのアルゴリズムの正当性の証明はありません。Møllerの論文を見ると小数表示を使っており、あまり真似したい感じではありません。残るはKnuthの本です。

というわけでKnuthの本をベースに証明を追いかけてみましたが、本の執筆の際にかなり圧縮されたのか、なかなか読み解くのが大変でした。具体的には、2週間くらいかかりました。本に書かれているのは証明の概略と言ったほうが良さそうですが、その方針本当に合ってる？と疑う場面もありました。手元の証明の分量は6ページくらいになりました（TAoCP vol2では2ページ程度で済まされています）。

定理1個で2週間とは、なかなかきついですね。今度の秋にまた技術書典があるようですが、本のクオリティーとか私生活の都合を考えると無理に新刊を出さない方がいいかもしれません。

ところで、定理の証明に詰まったときは直観に立ち返ることが大事です。証明で詰まったときは

  1. 直観で（インフォーマルに）考えて、「この主張は成り立ちそうだぞ」というのを見出す。
  2. QuickCheck等のテストツールで、その主張が実際の浮動小数点型で成り立つかランダムテストを行う。容易な反例があればここで見つかる。
  3. 反例が見つからなければ、真面目に証明を考える。

という流れで進めました。QuickCheckのデフォルトでは浮動小数点数のコーナーケースはなかなか踏んでくれなかったりしますが、その辺の話はまた別の機会にしましょう。

ちなみに、「小話」の売り上げがそこそこあるので浮動小数点数周りの論文は有料でも買っちゃおうという気分になっています。Møllerの論文も有料でしたが買いました。「小話」を買ってくださった方、ありがとうございます。

私が将来書く同人誌に、TwoSumのわかりやすい証明が載ることを祈っていてください。まあTwoSum周りの話は切り出して単体のPDFとして公開するということも考えられますが。

Spread the love