ball_float_checked の設計
設計目標
ball_float_checked を使うと、区間計算を一連の演算の連鎖として記述でき、構築の誤りや認証できないステップは明示的なエラーとなり、成功した値はすべて厳密な包含区間であり続けます。BallFloatResult は Result[BallFloat, ArithmeticError] を ball_float の演算について閉じたものにし、区間アルゴリズムを何も追加しません。API ページには演算が列挙されており、チュートリアルではパイプラインの使い方を示しています。
数学的背景
包含区間
IEEE 1788-2015(集合ベースのフレーバー)の意味での実数直線の閉区間の集合を と書きます。これは空集合、有界区間 、半直線、そして 自身からなります。11 IEEE 1788-2015, Standard for Interval Arithmetic, 第 7–10 節。 BallFloat は、有限の端点が 2 進浮動小数点数である の要素を表します。区間演算 が実関数 の包含(enclosure)であるとは、次が成り立つことです。
二項演算についても同様です。これは ball_float が実装する形での区間演算の基本定理です。包含性は合成によって保たれるので、包含を用いて式を評価すると、式の値域の包含が得られます。 が を包含し、 が を包含するならば、
ここで最初のステップでは に関する像の単調性を、2 番目のステップでは の包含性を用いました。22 R. E. Moore, R. B. Kearfott, M. J. Cloud, Introduction to Interval Analysis, SIAM, 2009, 第 5 章; van der Hoeven, “Ball arithmetic”, 2009。
エラーモナドとしてのラッパー
BallFloatResult は例外モナド です。ここで は BallFloat の値の集合、 は ArithmeticError の値の集合であり、 ok、 bind です。モナド則(左単位元則、右単位元則、結合則)と map の関手則は bin_float_checked の設計で証明されています。その証明は のいかなる性質も用いない の場合分けです。演算子は同じ左優先の方式(ball_result_lift2)で持ち上げられるので、最初のエラーの定理がそのまま適用されます。式は、後行順で最初にエラーを生じたノードのエラーを報告します。
設計上の判断
何がエラーで何が値か
問題。 区間計算は 4 種類の状況で終わりえます。入力が区間を表していない場合、演算がある引数に対して意味を持たない場合(次数ゼロの根)、ライブラリが十分に緊密な包含区間を認証できない場合、そして真の値域が空または非有界である場合です。
選択。 最初の 3 つはエラーであり、4 つ目は値です。
| 状況 | 結果 | ソース |
|---|---|---|
| NaN の境界、、、 | DomainError | try_from_bounds |
有限でない exact、from_double、from_float のソース | DomainError | try_exact, try_from_double, try_from_float |
次数 の rootn | DomainError | try_rootn |
| 予算内で包含区間を認証できない | CertificationFailure | try_*_interval, try_hypot |
| 値域が空(負数の 、) | 成功:空区間 | 区間演算 |
| 値域が非有界() | 成功:実数直線全体または半直線 | 区間演算 |
理由。 空または非有界な結果は真の値域の正しい包含区間なので、それをエラーにするとラッパーが集合ベースの意味論と食い違ってしまいます。 は健全な答えであり、 は厳密な答えです。対照的に、 はそもそも実数の集合ではなく、次数ゼロの根はどの引数に対しても定義されません。これらは呼び出し側の誤りです。認証の失敗は、ライブラリが証明できない結果を返すことを拒んでいることを意味し、これも包含区間ではありません。空または非有界な結果を自分のアプリケーションでは失敗とみなす呼び出し側は、bind でその規則を追加します(チュートリアルを参照)。
算術演算子は失敗しない
add、sub、mul、div は BallFloat の演算子を map で持ち上げたものなので、エラーを生じることはありません。4 つの集合演算は常に 内に包含区間を持ちます(除算では、 は の包として定義され、 のときは空です)。算術式に現れるエラーは、その葉のエラーだけです。
冪は算術トレイトを経由する
pow_nat と pow_int は、ArithmeticContext::new(x.precision()) を引数として Luna-Flow/arithmetic の PowNatChecked::pow_nat_checked と PowIntChecked::pow_int_checked を呼び出します。BallFloat はコンテキストから精度だけを読み取り(丸め方向と指数の上下限は外向きに丸められた包含区間にとって意味を持ちません)、底の精度を変更し、区間全体の冪を計算します。繰り返し乗算する代わりに冪を用いることで依存性問題を回避できます。 は 2 つの因子を独立に扱うので、 に対しては を与えますが、 です。
装飾もフラグも持たない
IEEE 1788 の装飾(com、dac、def、trv、ill)は、関数が入力上で定義され連続であったかどうかを記録します。ball_float はこれを装飾付きの型 BallFloatDecorated で提供しています。ラッパーがこれを保持しないのは、装飾が失敗ではなく成功した評価についての情報であり、それをエラーチャネルと組み合わせるとすべての map が装飾の伝播に責任を負うことになるからです。BallFlags についても同様です。どちらかを必要とするアプリケーションは ball_float を直接使います。
構築時の精度
コンストラクタは ball_float のデフォルトを用います(整数は 16 ビット、Double は 53、Float は 24、exact はソースの精度、from_bounds は大きい方の境界の精度)。from_bounds、exact、from_double、from_float は外向きに丸めるので、ソースの値は常に包含されます。from_int と from_coefficient は、まず ビットで最近接に丸めた BinFloat を構築し、その値を包含します。現在のブランチでは、整数が精度より多くのビットを必要とする場合、これによって整数が失われます(API ページの警告を参照)。
正しさ/不変条件
- 健全性。 式のすべての葉が意図した実数入力を包含する成功値であり、式が に評価されるならば、 は入力上の実数の式の値域を包含します。これは上記の合成の議論と、ラッパーが成功値に対して
ball_floatの演算をそのまま適用するという事実から従います。 - エラーの決定性。 式が に評価されるならば、 は後行順で最初にエラーを生じたノードのエラーです。
- 隠れた復帰はない。 エラーを値に変えるメソッドは存在せず、
mapが値をエラーに変えることもありません()。 - コスト。 ラッパーの各ステップは、委譲先の区間演算に の作業を加えるだけです。
却下した代替案
- 空の結果をエラーとすること。 集合ベースの意味論を破り、健全な包含区間が存在する に対してエラーを報告することになります。
- ラッパーに装飾を持たせること。
ball_floatの装飾付き API を、2 つ目の伝播規則とともに重複させることになります。 - コンテキスト付きの変種(
exp_ctx、…)。 包含区間は区間の精度で外向きに丸められます。精度の変更はwith_precisionで明示的に行い、これはどの丸めモードでも包含性を保ちます。 - エラーの蓄積。 2 進のラッパーと同様に、
ArithmeticErrorを結合する演算は存在しません。
境界
- 独自の区間アルゴリズムは持たず、すべての包含区間は
ball_floatに由来します。 - 装飾、
BallFlags、区間コンテキスト、交換形式は扱いません。 - エラーからの復帰や蓄積は行わず、最初のエラーだけが保持されます。
- ラッパー自体には
Eq、Show、包含関係はありません。包含や順序を判定するには、result()でBallFloatを取り出してください。 - 引数のうち定義域外の部分は無視され、報告されません。