fdlibmから現在使用しているモデル チェッカー ツール ( cbmcsqrt ) への関数 (64 ビット double 用) の移植に取り組んでいます。
仕事の一環として、ieee-754 規格についてよく読みましたが、基本演算 (sqrt を含む) の精度の保証を理解していなかったと思います。
fdlibm の sqrt のポートをテストすると、64 ビット double で sqrt を使用して次の計算が得られました。
sqrt(1977061516825203605555216616167125005658976571589721139027150498657494589171970335387417823661417383745964289845929120708819092392090053015474001800648403714048.0) = 44464159913633855548904943164666890000299422761159637702558734139742800916250624.0
(このケースは、精度に関する私のテストで単純な事後条件を破りました。この事後条件が IEEE-754 で可能かどうかはわかりません)
比較のために、いくつかの多精度ツールは次のように計算しました。
sqrt(1977061516825203605555216616167125005658976571589721139027150498657494589171970335387417823661417383745964289845929120708819092392090053015474001800648403714048.0) =44464159913633852501611468455197640079591886932526256694498106717014555047373210.truncated
左から 17 番目の数字が異なることがわかります。これは、次のようなエラーを意味します。
3047293474709469249920707535828633381008060627422728245868877413.0
質問 1: この膨大な量のエラーは許容されますか?
標準では、すべての基本演算 (+、-、、/、sqrt) は 0.5 ulp 以内である必要があるとされています。これは、最も近い fp 表現に丸められた数学的に正確な結果に等しくなければならないことを意味します (wiki では、一部のライブラリは1 ulp しか保証されませんが、現時点ではそれほど重要ではありません)。
質問 2: すべての基本操作で、64 ビット double (マシン イプシロン) で 2.220446e-16 未満のエラーが発生するということですか?
x86-32 Linux システム (glibc / eglibc) で同じことを計算したところ、fdlibm で得られたのと同じ結果が得られました。
- a: 私は何か間違ったことをしました (しかし、どのように:
printf候補になるでしょうが、それが理由であるかどうかはわかりません) - b: エラー/精度はこれらのライブラリで一般的です