`decimal_gda_checked` の設計

設計目標

decimal_gda_checked は、General Decimal Arithmetic (GDA) 仕様の制御フローをメソッド呼び出しの連鎖として使えるようにします。GDA では、すべての演算がコンテキストを受け取り、シグナルを発生させることがあり、それをコンテキストのスティッキーなステータスに記録し、発生したシグナルがコンテキストのトラップ集合で有効になっていれば計算を停止します。¹1 M. Cowlishaw, General Decimal Arithmetic Specification, version 1.70, 「Context」節（フラグとトラップ有効化子）および「Exceptional conditions」節。 decimal_gda は個々の演算を GdaOutcome を返す純粋関数として実装しています。GdaDecimalChecked は返されたコンテキストを次の演算へ受け渡し、トラップで短絡し、続行するための明示的な手段を一つだけ提供します。演算の一覧は API ページに、トラップと回復の例はチュートリアルにあります。

数学的背景

シグナル、ステータス、トラップ

$\Sigma$ を 13 個の GDA シグナル（ConversionSyntax, DivisionByZero, DivisionImpossible, DivisionUndefined, InvalidContext, InvalidOperation, Overflow, Underflow, Subnormal, Inexact, Rounded, Clamped, LostDigits）の集合とします。GdaFlags の値は $\Sigma$ の部分集合、すなわち $\mathbb{B}^{\Sigma}$ の元であり、GdaFlags::combine は和集合、つまりフィールドごとの OR です。IEEE フラグの場合と同様に、 $(\mathbb{B}^{\Sigma}, \cup, \varnothing)$ は可換かつ冪等なモノイド（有界な結び半束）です。GdaTrapSet はもう一つの部分集合 $T \subseteq \Sigma$ です。

GDA は四つのシグナルを無効演算（invalid operation）としてまとめています: $I = \{\texttt{ConversionSyntax}, \texttt{DivisionImpossible}, \texttt{DivisionUndefined}, \texttt{InvalidContext}\}$ 。実装はこれを二か所で表現しています。

\begin{aligned} r \models s \;&\iff\; s \in r \text{, except } r \models \texttt{InvalidOperation} \iff \texttt{InvalidOperation} \in r \lor r \cap I \ne \varnothing,\\ \delta(r) \;&=\; r \cup \{\texttt{InvalidOperation} : r \cap I \ne \varnothing\}. \end{aligned}

$r \models s$ は GdaFlags::contains です。 $\delta$ は complete_gda（src/decimal_gda/gda_context.mbt 内）がステータスに加えるステータス差分です。

$\delta$ はモノイド準同型です。 $\chi(r) = [\, r \cap I \ne \varnothing \,]$ とおくと $\chi(a \cup b) = \chi(a) \lor \chi(b)$ が成り立つので、

\delta(a \cup b) = a \cup b \cup \{\texttt{InvOp} : \chi(a) \lor \chi(b)\} = \delta(a) \cup \delta(b), \qquad \delta(\varnothing) = \varnothing .

GDA の 1 ステップ

コンテキストは $c = (\pi, S, T)$ です。すなわち、パラメータ $\pi$ （精度、丸め、 $E_{\min}$ 、 $E_{\max}$ 、clamp、extended）、ステータス $S$ 、トラップ $T$ からなります。演算はオペランドと $\pi$ から結果 $v'$ と発生したシグナル $r$ を計算します。そして

\operatorname{step}(v', r, c) = \begin{cases} \texttt{Completed}(v', c, \varnothing) & r = \varnothing,\\ \texttt{Trapped}(\tau(r, T), v', c[S \cup \delta(r)], r) & \tau(r, T) \text{ defined},\\ \texttt{Completed}(v', c[S \cup \delta(r)], r) & \text{otherwise}, \end{cases}

ここでトラップ選択子 $\tau(r, T)$ は、固定された優先順位リスト InvalidOperation, DivisionByZero, DivisionUndefined, DivisionImpossible, InvalidContext, ConversionSyntax, Overflow, Underflow, Subnormal, Inexact, Rounded, Clamped, LostDigits のうち、 $r \models s$ かつ $s \in T$ を満たす最初の $s$ です。ステータスはトラップの判定より前に更新されるため、トラップされたシグナルは次のステータスに含まれること、また $v'$ はプレースホルダではなく、その条件に対して GDA が規定する定義済みの結果（例えばゼロ除算なら $\pm\infty$ ）であることに注意してください。

吸収的なトラップを持つモナドとしてのパイプライン

GdaOutcome[Decimal] を $O = \texttt{Completed}(V \times C \times \mathbb{B}^{\Sigma}) + \texttt{Trapped}(\Sigma \times V \times C \times \mathbb{B}^{\Sigma})$ と書きます。すべてのパイプラインメソッドは次の bind です。

\begin{aligned} \texttt{Completed}(v, c, \_) \mathbin{>\!\!>\!\!=} f &= f(v, c),\\ \texttt{Trapped}(s, v, c, r) \mathbin{>\!\!>\!\!=} f &= \texttt{Trapped}(s, v, c, r), \end{aligned}

ここで $f(v, c) = \mathrm{op}(v, \dots, c)$ は decimal_gda の関数であり、単位は $\eta(v, c) = \texttt{Completed}(v, c, \varnothing)$ です。これはコンテキスト上の状態モナドに、トラップされた結果全体をペイロードとする例外を組み合わせたものです。²2 E. Moggi, “Notions of computation and monads”, 1991（状態モナドと例外モナド）; P. Wadler, “Monads for functional programming”, 1995. モナド則はエラーモナドの場合とまったく同じく場合分けで成り立ちます。左単位則 $\eta(v, c) \mathbin{>\!\!>\!\!=} f = f(v, c)$ は第 1 式から従います。右単位則は、 $f = \eta$ が $\texttt{Completed}(v, c, r)$ を $\texttt{Completed}(v, c, \varnothing)$ に写し、これが値とコンテキストにおいて入力と一致することから成り立ちます（最新ステップのフラグはステップごとの観測値であり、各ステップでリセットされます）。結合則は、Trapped の入力は両辺で変更されずに返され、Completed の入力では両辺がともに $f(v, c) \mathbin{>\!\!>\!\!=} g$ に帰着することから成り立ちます。

設計上の判断

状態はちょうど一つの `GdaOutcome`

問題。 パイプラインは、値、次に使うコンテキスト、最新のシグナル、そしてトラップが発生したかどうかを記憶しなければなりません。

選択。 GdaDecimalChecked は一つの GdaOutcome だけを保持し、それ以外は何も持ちません。したがってこれは、decimal_gda の結果型をその演算について閉じたものです。すべての観測（value, context, raised, status, is_trapped, trapped_signal）は結果の射影であり、from_outcome / outcome は両方向に情報を失わずに変換します。

トラップはエラーではなく停止である

問題。 トラップされた GDA 条件は計算を停止させなければなりませんが、それはライブラリの失敗ではありません。仕様はその場合の結果とステータスの両方を定義しており、アプリケーションが続行を選ぶこともあります。

選択肢。 (a) トラップを ArithmeticError に変換する。(b) トラップされた結果を状態として保持し、明示的な回復を要求する。

選択: (b)。 変換すると、定義済みの結果と次のコンテキストが失われます。これらは GDA のハンドラが続行するために必要とするものです。トラップされた状態はすべての演算の不動点であり（後述）、resume_defined() が唯一の出口です。回復を明示的にすることで、「トラップの後に定義済みの結果を受け入れた」ことがコード上で見えるようになります。

再開時に保持されるもの

$\rho =$ resume_defined は $\texttt{Trapped}(s, v, c, r) \mapsto \texttt{Completed}(v, c, \varnothing)$ と写し、完了した結果は変更しません。コンテキストを保持するので、

\operatorname{status}(\rho(x)) = \operatorname{status}(x), \qquad \operatorname{traps}(\rho(x)) = \operatorname{traps}(x), \qquad \rho \circ \rho = \rho .

仕様が発生済みのフラグに要求するとおり、ステータスはトラップされたシグナルを記録し続けます。トラップ集合は変わらないので、同じ条件が再び起これば再度トラップされます。破棄されるのはステップごとの raised とトラップの印だけです。

///|
test "resume keeps status and traps and is idempotent" {
  let ctx = @decimal_gda.GdaContext::default()
  let zero = @decimal_gda.Decimal::zero()
  let trapped = @decimal_gda_checked.GdaDecimalChecked::parse("1", ctx).divide(zero)
  let once = trapped.resume_defined()
  let twice = once.resume_defined()
  inspect(once.status() == trapped.status(), content="true")
  inspect(twice.status() == once.status(), content="true")
  inspect(twice.value().to_string() == once.value().to_string(), content="true")
  // the context after resuming still traps division by zero
  let again = @decimal_gda_checked.GdaDecimalChecked::parse("2", once.context()).divide(zero)
  inspect(again.is_trapped(), content="true")
}

素のオペランドとコンテキストの非マージ

すべての二項メソッドの第 2 オペランドは素の Decimal です。二つのパイプラインは二つのスティッキーなステータスと二つのトラップ集合を持つことになりますが、計算が一つの現在のコンテキストを持つ GDA においては、それらをマージすることに規定された意味はありません。

Luna-Flow/arithmetic との関係

パイプラインは GdaContext を受け取ります。これは ArithmeticContext にはないステータスとトラップを持っています。@decimal_gda.Decimal の contextual トレイト実装（Luna-Flow/arithmetic 上のジェネリックなコード向け）は、パッケージの IEEE 流の DecimalContext::from_arithmetic_context を使い、トラップなしで演算ごとに ArithmeticDiagnostics を報告します。二つのモデルは分離されています。ジェネリックなアルゴリズムはトラップを観測できず、GDA パイプラインはそのステータスを診断レコードに奪われることがありません。

正しさ／不変条件

ステータスはスティッキーである

定理。 パイプラインがステータス $S_0$ のコンテキストから出発し、発生シグナル $r_1, \dots, r_n$ を持つ完了ステップを経るとする。このとき最終コンテキストのステータスは

S_n = S_0 \cup \delta(r_1) \cup \dots \cup \delta(r_n) = S_0 \cup \delta(r_1 \cup \dots \cup r_n).

証明。 帰納法による。 $r = \varnothing$ のステップはコンテキストを変更せず、 $S \cup \delta(\varnothing) = S$ である。そうでなければ、ステップは $S_{k+1} = S_k \cup \delta(r_{k+1})$ と設定する。第 2 の等式は $\delta$ の準同型性である。 $\square$

帰結として、ステータスは増加するのみであり（ $S_k \subseteq S_{k+1}$ ）、各ステップのシグナルの順序に依存せず、無効演算の条件がいずれか一つでも発生していれば $\texttt{InvalidOperation} \in S_n$ となります。ステータスはトラップの判定より前に更新されるので、トラップしたステップも含まれます。また $\rho$ はステータスを保存するので、この定理は resume_defined をまたいでも成り立ちます。

最初のトラップでパイプラインは終わる

定理。 パイプライン $x_k = \mathrm{op}_k(x_{k-1})$ において、ステップ $j$ が結果が Trapped となる最初のステップであれば、resume_defined が適用されない限り、すべての $n \ge j$ について $x_n = x_j$ である。

証明。 すべての演算メソッドは結果に対してパターンマッチし、Trapped に対しては self を返すので、 $k > j$ について $x_{k} = x_{k-1}$ である。 $k$ に関する帰納法による。 $\square$

選択子 $\tau$ と合わせると、報告されるシグナルは一意に定まります。それは、最初にトラップしたステップが発生させたシグナルのうち、トラップ対象で最も優先順位の高いものです。

トラップは履歴ではなくステップに依存する

トラップの判定には、ステータス $S$ ではなく、現在のステップが発生させたシグナル $r$ を使います。そのトラップを含まないコンテキストの下で以前に発生したシグナルは後続のステップをトラップさせず、ステータスをクリアしてもトラップには影響しません。これは、トラップが条件を発生させた演算のイベントである GDA と一致しています。

コスト

1 ステップのコストは、GDA の演算に、13 フィールドのレコード二つに対する定数時間の処理を加えたものです。演算が何も発生させなければ、コンテキストはそのまま受け渡されます。

却下した代替案

トラップを ArithmeticError にする。 定義済みの結果と次のコンテキストが失われます。
自動再開。 トラップされた結果を受け入れるという判断が隠れてしまいます。GDA はその判断をハンドラに委ねています。
パイプライン上の演算子。 コンテキストのマージと同じ理由で採用しません。
再開時にステータスをクリアする。 トラップされた条件が発生した証拠を消してしまいます。

境界

独自の算術は持ちません。すべての演算は decimal_gda に由来します。
生成されたインターフェースにある演算集合だけがパイプラインメソッドを持ちます。それ以外の decimal_gda の演算は value() / context() に対して実行し、from_outcome で包み直します。
ArithmeticError も IEEE の DecimalFlags も扱いません。IEEE 流のフラグ蓄積は decimal_checked の契約です。
パイプラインのマージ、暗黙の回復、パイプライン途中でのトラップ集合の変更はいずれも行いません。

M. Cowlishaw, General Decimal Arithmetic Specification, version 1.70, 「Context」節（フラグとトラップ有効化子）および「Exceptional conditions」節。 ↩
E. Moggi, “Notions of computation and monads”, 1991（状態モナドと例外モナド）; P. Wadler, “Monads for functional programming”, 1995. ↩

decimal_gda_checked の設計