decimal_checked の設計
設計目標
decimal_checked は、IEEE 754 の 10 進演算の列を、最後に 2 つの問い(結果は何か、途中で何が起きたか)に答える 1 つの値に変えます。IEEE の 10 進算術は、例外条件を定義済みの結果に添えたステータスフラグとして報告します。単一の演算は (value, flags) を返しますが、多数のステップからなる計算ではすべてのステップのフラグが必要です。DecimalChecked は 1 つのコンテキストをステップ間で受け渡してフラグを蓄積しつつ、例外的な結果も値であるという IEEE の規則を保ちます。演算の一覧は API ページに、監査型のパイプラインはチュートリアルにあります。
数学的背景
フラグのモノイド
DecimalFlags は 13 個のブール型フィールド(inexact、rounded、overflow、…)を持つので、フラグ集合は の元、あるいは同値なことに 13 個のシグナルの集合 の部分集合です。DecimalFlags::combine はフィールドごとの OR です。
ブール OR は結合的、可換、冪等で単位元 を持ち、演算はフィールドごとに作用するので、
したがって は可換で冪等なモノイド、すなわち有界な結び半束です。部分集合として読めば は和集合です。DecimalFlags::contains(s) は座標 を読み出し、 へのモノイド準同型になっています:。
writer の射としての演算
固定されたコンテキスト のもとでの IEEE 演算は、10 進値 上の関数 であり、丸められた結果と立てられたフラグを返します(Decimal::add_ctx、div_ctx、sqrt_ctx、…)。このような関数は 上の writer モナドの Kleisli 射です。
モナド則はモノイド則に帰着します。左単位則:。右単位則:。結合則:、 とすると、 と はどちらも に等しくなります。11 P. Wadler, “Monads for functional programming”, 1995(出力モナド)。任意のモノイドから writer モナドが得られ、その法則はちょうどモノイド則です。
パイプラインの状態
DecimalChecked は 、すなわち値、コンテキスト、直近のステップのフラグ、蓄積されたフラグ、省略可能なエラーを保持します。プライベートな record ステップは writer の bind であり、直近のフラグで拡張され、エラーによってガードされています。
record_result は失敗しうる演算 を扱います。 のときは record と同じで、 のときは を返します。したがって完全なステップは、例外モナドの上に writer モナドを積み重ねたもので、エラーは吸収的です。
設計上の判断
フラグは蓄積され、例外的な結果は値のまま残る
問題。 長い 10 進計算では、いずれかのステップが丸めたか、オーバーフローしたか、ゼロ除算したかを報告しなければなりません。そして IEEE 754 はそのような各ステップに結果を定義しています。
選択肢。 (a) Luna-Flow/arithmetic のコンテキスト付きトレイトがゼロ除算と無効演算について行っているように、例外条件をエラーに変える。(b) 最後のステップのフラグだけを返す。(c) IEEE の値を保持し、フラグを蓄積する。
選択:(c)。 IEEE のモデルでは、計算は定義済みの結果で続行し、何が起きたかはステータスフラグが伝えます。監査は最後にフラグを検査します。22 IEEE 754-2019、7 節(デフォルトの例外処理)と 8 節(代替の例外処理):ステータスフラグは立てられると、明示的に下ろされるまで立ったままになります。 選択肢 (a) は IEEE が を定義しているにもかかわらず で停止してしまい、選択肢 (b) はそれ以前の条件を失います。エラーは、この実装で定義済みの IEEE の結果が存在しない唯一のケース、すなわち認証付きの初等関数が丸めを認証できない場合のために取っておかれます。(raised)と (flags)の両方を保持することで、呼び出し側は直近のステップと履歴全体の両方を見ることができます。
パイプラインごとに 1 つのコンテキスト、素のオペランド
問題。 二項演算が別のパイプラインをオペランドとして受け取ることも考えられます。
選択。 オペランドは素の Decimal 値です。2 つのパイプラインは 2 つのコンテキストと 2 つのフラグ履歴を持っています。それらを統合するにはどちらのコンテキストを優先するかの規則が必要で、履歴の和集合ではどちら側がフラグを立てたかが隠れてしまいます。素のオペランドなら、パイプラインは 1 つのコンテキストのもとでの単一の線形な履歴になり、コンテキストは with_context によってのみ変わります。このメソッドは現在の値を新しいコンテキストへ丸めたときのフラグを記録します。同じ理由で、この型は演算子を実装していません。
Luna-Flow/arithmetic のコンテキストの対応付け
パイプラインは DecimalContext を受け取ります。ArithmeticContext を持っている呼び出し側は DecimalContext::from_arithmetic_context でそれを変換します。この関数は次のように対応付けます。
ArithmeticContext | DecimalContext |
|---|---|
precision | precision |
rounding | rounding、および decimal_rounding = DecimalRoundingMode::from_arithmetic(rounding) |
e_min, e_max | 同じ値、存在しなければ |
clamp | clamp |
extended = true で、丸め後の極小性判定を使います。したがって、あらかじめ定義された ArithmeticContext::decimal64() は DecimalContext::decimal64() にちょうど対応します。コンストラクタはコンテキストを DecimalContext::ieee754() に通します。これは IEEE プロファイルを選択するためのフックで、現在のブランチではコンテキストをそのまま返します。
数学関数は、General Decimal Arithmetic 仕様が exp、ln、log10、power について行っているのと同様に、コンテキストを制限します。精度と両方の指数の上下限は絶対値で 以内でなければならず、そうでなければ結果は invalid_context を伴う NaN になります(src/decimal のプライベートな検査 math_context_is_restricted)。33 M. Cowlishaw, General Decimal Arithmetic Specification, version 1.70, “Arithmetic operations: exp, ln, log10, power”(コンテキストに対する制限)。 したがってデフォルトの無制限の指数範囲ではこれらの関数は使えません。このことは API ページとチュートリアルでも指摘されています。
フラグから算術の診断情報へ
Luna-Flow/arithmetic における Decimal のコンテキスト付きトレイト実装は ArithmeticDiagnostics を報告します。これは 6 個のブール値で、ArithmeticDiagnostics::combine(やはりフィールドごとの OR)で組み合わされます。src/decimal/traits.mbt のプライベートなヘルパー contextual_diagnostics は、共通する 6 つの座標を残すことでフラグを診断情報に対応付けます。この射影を と呼びます。座標射影はフィールドごとの OR と可換です。
したがって はモノイド準同型であり、帰納法により
パイプラインの蓄積されたフラグを最後に 1 回変換しても、各ステップを変換して組み合わせても、同じ診断情報が得られます。トレイト実装が ArithmeticError に変える条件(ゼロ除算と、DecimalFlags::has_error で判定される無効演算の系統)は が残す座標には含まれません。パイプラインはそれらを代わりにフラグとして保持します。
正しさ/不変条件
蓄積されたフラグはステップごとのフラグの和集合である
定理。 パイプラインがフラグ で構築され(from_outcome、from_decimal、parse、または数値コンストラクタによって)、その後、立てられたフラグ を伴う成功したステップ (with_context と apply を含む)を、途中で clear_flags を挟まずに経たとします。このとき
証明。 すべてのコンストラクタは と設定し、これが の場合です。 ならば、成功したステップ は record(または with_context 内の同一の更新)を通り、結合則により と を設定します。
の可換性と冪等性により、 はステップの順序やシグナルが何回立てられたかに依存しません。また contains の準同型性により、
次のテストは 3 ステップのパイプラインでこの定理を確かめます。蓄積されたフラグは、各ステップで立てられたフラグの OR に、組み合わせの順序によらず等しくなります。
///|
test "accumulated flags are the union of the raised flags" {
let ctx = @decimal.DecimalContext::decimal64()
let s0 = @decimal_checked.DecimalChecked::from_int(1, ctx)
let s1 = s0.div(@decimal.Decimal::from_int(3))
let s2 = s1.add(@decimal.Decimal::from_int(10))
let s3 = s2.div(@decimal.Decimal::zero())
let forward = s0.raised().combine(s1.raised()).combine(s2.raised()).combine(s3.raised())
let backward = s3.raised().combine(s2.raised()).combine(s1.raised()).combine(s0.raised())
inspect(s3.flags() == forward, content="true")
inspect(forward == backward, content="true")
inspect(s3.raised().inexact, content="false")
inspect(s3.flags().inexact && s3.flags().division_by_zero, content="true")
}
clear_flags の後は、その時点から として定理が再び成り立ちます。 はパイプラインに沿って単調です:。
エラーは吸収的である
定理。 状態が を持つとき、clear_flags 以外のすべての演算はその状態をそのまま返し、clear_flags は と だけを変更します。
証明。 record、record_result、with_context はガード self.error_ is None で始まり、そうでなければ self を返します。すべての算術メソッドは record または record_result を通ります。clear_flags は 2 つのフラグフィールドだけを更新します。
したがって報告されるのは最初のエラーであり、値とフラグは失敗したステップの前のまま残り、result() は を返します。エラーのないパイプラインでは、result() は writer モナドの出力 です。
コスト
1 ステップのコストは、委譲先の 10 進演算に、13 フィールドの OR 1 回と定数サイズの状態のコピーを加えたものです。
却下した代替案
- IEEE の例外をエラーにすること。 IEEE のデフォルトの例外処理とこのパッケージの目的に反します。コンテキスト付きトレイトが、単一の演算についてはすでにそのモデルを提供しています。
- パイプラインの統合。 2 つのコンテキストに対する標準的な規則がありません。上記を参照してください。
- 可変なフラグ。 Luna-Flow はコンテキストとステータスを値として保持します。不変な状態は分岐させたり比較したりできます。
- ステップごとの履歴の保存。 和集合は監査の問いに定数サイズで答えます。履歴が必要な呼び出し側は、関心のある状態を自分で保持します。
境界
- 独自の算術はありません。すべての結果は
decimalから得られます。 - トラップや代替の例外処理はありません。IEEE のフラグがパイプラインを停止させることはありません。トラップ駆動の制御フローは
decimal_gda_checkedの契約です。 - 演算子、パイプライン同士の演算、暗黙のコンテキスト変更はありません。
- エラーになるのは初等関数の認証の失敗だけです。
- コンテキストは
decimalの IEEE 10 進コンテキストです。スティッキーなステータスを持つ GDA コンテキストはdecimal_gdaに属します。
Footnotes
-
P. Wadler, “Monads for functional programming”, 1995(出力モナド)。任意のモノイドから writer モナドが得られ、その法則はちょうどモノイド則です。 ↩
-
IEEE 754-2019、7 節(デフォルトの例外処理)と 8 節(代替の例外処理):ステータスフラグは立てられると、明示的に下ろされるまで立ったままになります。 ↩
-
M. Cowlishaw, General Decimal Arithmetic Specification, version 1.70, “Arithmetic operations: exp, ln, log10, power”(コンテキストに対する制限)。 ↩