浮動小数点の精度

今私は automated software verification からの派生で、力学系の simulation 言語で、系を記述する微分方程式を打ち込めば (一定の条件下でなら) 誤差を自動で見積もって計算結果の精度に関する警告あるいは保証をくれた上で数値的に解いてくれる、というものを作るべく前向きに善処しております。*1実装言語は ocaml。
で、その数値解析の部分では当然基本的な演算 (今のところ加減乗除と平方根、三角・指数関数とその逆関数ぐらい) がどんな精度を保証してくれるかの情報が要るわけですが、これが意外と無い。とりあえず OCaml library には精度の話はビタイチ書いてない (期待してなかったけど)。Processor manual を見てみると、Intel Processor Manual には三角関数は 1.5ulps とかの記述があるが、Power PC なんかに至ってはそもそも超越関数を hardware で実装してない。無理関数すら無い。で、libC を見ても記述見当たらず。加減乗除についても記述が無いけど、IA32 とかは内部では 80bit で演算やってたりするから、多分 64 でやってる processor とは誤差が違うはず。
で、 abstraction layer を上に手繰って GNU Scientific Library とかに目をやると「正確だよ」と書いてあるだけで、保証の類は無いぽ。それと、layer が高すぎて不適切。
そういうのを漁ってる最中に long double の精度の compiler + architecture ごとの比較を見て、そういえば C level まで降りて行っても compiler に結果が依存するとか、同じ bit string を printf とかに渡しても中の人が使用してる algorithm によって出力が違ってくるとか思い出したあたりでゲンナリして諦めた。どうしょっか…
どれぐらいの高さの layer を building block に据えたらいいのやら。浮動小数点の精度解析を portable に書こうとするのがそもそもの間違いなんでしょうかね。

*1:本当に完成させる気があるかどうかは微妙。ていうかこの simulator の誤差見積り機能自体は多分静的解析に拘らず double と多倍長で実行したのを比較して危なげな差が出るか見た方が早い。でもわざわざ静的にするのは、highly parametrized な algorithm をどういう風に specialize するとどういう影響があるかを体系的に調べる手法を作るのに役立つかも知れないから。