decimal_gda_checked 设计

设计目标

decimal_gda_checked 让通用十进制算术(General Decimal Arithmetic,GDA)规范的控制流可以写成方法调用链。在 GDA 中,每个运算都接收一个上下文,可能引发若干信号,把它们记录到上下文的粘滞状态中,并在所引发的信号属于上下文的陷阱集合时终止计算。11 M. Cowlishaw,General Decimal Arithmetic Specification,1.70 版,“Context”(标志与陷阱使能)和 “Exceptional conditions” 两节。 decimal_gda 把单个运算实现为返回 GdaOutcome 的纯函数;GdaDecimalChecked 把返回的上下文传入下一个运算,遇到陷阱时短路,并提供唯一一种显式的继续方式。API 页面列出了各项运算;教程演示了陷阱与恢复。

数学背景

信号、状态与陷阱

设 Σ\Sigma 为 GDA 的十三种信号(ConversionSyntax、DivisionByZero、DivisionImpossible、DivisionUndefined、InvalidContext、InvalidOperation、Overflow、Underflow、Subnormal、Inexact、Rounded、Clamped、LostDigits)。一个 GdaFlags 值是 Σ\Sigma 的子集,即 BΣ\mathbb{B}^{\Sigma} 中的一个元素,而 GdaFlags::combine 就是并集,即逐字段的 OR。与 IEEE 标志一样,(BΣ,∪,∅)(\mathbb{B}^{\Sigma}, \cup, \varnothing) 是一个交换幂等幺半群(有界并半格)。GdaTrapSet 则是另一个子集 T⊆ΣT \subseteq \Sigma。

GDA 把四种信号归入无效运算:I={ConversionSyntax,DivisionImpossible,DivisionUndefined,InvalidContext}I = \{\texttt{ConversionSyntax}, \texttt{DivisionImpossible}, \texttt{DivisionUndefined}, \texttt{InvalidContext}\}。实现在两处体现这一点:

r⊨s    ⟺    s∈r, except r⊨InvalidOperation  ⟺  InvalidOperation∈r∨r∩I≠∅,δ(r)  =  r∪{InvalidOperation:r∩I≠∅}.\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⊨sr \models s 即 GdaFlags::contains;δ\delta 是 complete_gda(位于 src/decimal_gda/gda_context.mbt)加入状态的状态增量。

δ\delta 是幺半群同态。令 χ(r)=[ r∩I≠∅ ]\chi(r) = [\, r \cap I \ne \varnothing \,],则有 χ(a∪b)=χ(a)∨χ(b)\chi(a \cup b) = \chi(a) \lor \chi(b),因此

δ(a∪b)=a∪b∪{InvOp:χ(a)∨χ(b)}=δ(a)∪δ(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 的单步运算

上下文是 c=(π,S,T)c = (\pi, S, T):参数 π\pi(精度、舍入、Emin⁡E_{\min}、Emax⁡E_{\max}、clamp、extended)、状态 SS 和陷阱 TT。一个运算由操作数和 π\pi 计算出结果 v′v' 以及引发的信号 rr。然后

step⁡(v′,r,c)={Completed(v′,c,∅)r=∅,Trapped(τ(r,T),v′,c[S∪δ(r)],r)τ(r,T) defined,Completed(v′,c[S∪δ(r)],r)otherwise,\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}

其中陷阱选择器 τ(r,T)\tau(r, T) 是固定优先级列表 InvalidOperation、DivisionByZero、DivisionUndefined、DivisionImpossible、InvalidContext、ConversionSyntax、Overflow、Underflow、Subnormal、Inexact、Rounded、Clamped、LostDigits 中第一个满足 r⊨sr \models s 且 s∈Ts \in T 的 ss。注意状态在陷阱判定之前更新,因此被陷阱捕获的信号会出现在下一个状态中;并且 v′v' 是 GDA 为该情形规定的确定结果(例如除以零时为 ±∞\pm\infty),而不是占位值。

以陷阱为吸收元的单子流水线

把 GdaOutcome[Decimal] 记作 O=Completed(V×C×BΣ)+Trapped(Σ×V×C×BΣ)O = \texttt{Completed}(V \times C \times \mathbb{B}^{\Sigma}) + \texttt{Trapped}(\Sigma \times V \times C \times \mathbb{B}^{\Sigma})。每个流水线方法都是如下的 bind:

Completed(v,c,_)> ⁣ ⁣> ⁣ ⁣=f=f(v,c),Trapped(s,v,c,r)> ⁣ ⁣> ⁣ ⁣=f=Trapped(s,v,c,r),\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)=op(v,…,c)f(v, c) = \mathrm{op}(v, \dots, c) 是 decimal_gda 中的函数,单位元为 η(v,c)=Completed(v,c,∅)\eta(v, c) = \texttt{Completed}(v, c, \varnothing)。这就是上下文上的状态单子与一个以整个被陷阱捕获的结果为载荷的异常相结合。22 E. Moggi,“Notions of computation and monads”,1991(状态单子与异常单子);P. Wadler,“Monads for functional programming”,1995。 单子律可以像错误单子那样逐情形验证:左单位律 η(v,c)> ⁣ ⁣> ⁣ ⁣=f=f(v,c)\eta(v, c) \mathbin{>\!\!>\!\!=} f = f(v, c) 由第一个等式得到;右单位律成立,是因为 f=ηf = \eta 把 Completed(v,c,r)\texttt{Completed}(v, c, r) 映为 Completed(v,c,∅)\texttt{Completed}(v, c, \varnothing),它在值和上下文上与输入一致(最近一步的标志只是逐步的观测,每一步都会重置);结合律成立,是因为 Trapped 输入在两边都原样返回,而 Completed 输入使两边都化为 f(v,c)> ⁣ ⁣> ⁣ ⁣=gf(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 把 Trapped(s,v,c,r)↦Completed(v,c,∅)\texttt{Trapped}(s, v, c, r) \mapsto \texttt{Completed}(v, c, \varnothing),并保持已完成的结果不变。它保留上下文,因此

status⁡(ρ(x))=status⁡(x),traps⁡(ρ(x))=traps⁡(x),ρ∘ρ=ρ.\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")
}

普通操作数,不合并上下文

每个二元方法的第二个操作数都是普通的 Decimal。两条流水线会携带两个粘滞状态和两个陷阱集合;在 GDA 中合并它们没有规定的含义,因为一次计算只有一个当前上下文。

与 Luna-Flow/arithmetic 的关系

流水线接收 GdaContext,它携带 ArithmeticContext 所没有的状态与陷阱。@decimal_gda.Decimal 的 contextual trait 实现(供基于 Luna-Flow/arithmetic 的泛型代码使用)采用本包 IEEE 风格的 DecimalContext::from_arithmetic_context,并逐运算报告 ArithmeticDiagnostics,不涉及陷阱。两种模型保持分离:泛型算法观测不到陷阱,GDA 流水线也不会把状态丢给诊断记录。

正确性 / 不变式

状态是粘滞的

定理。 设一条流水线从状态为 S0S_0 的上下文出发,依次经过引发信号为 r1,…,rnr_1, \dots, r_n 的已完成步骤。则最终上下文的状态为

Sn=S0∪δ(r1)∪⋯∪δ(rn)=S0∪δ(r1∪⋯∪rn).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=∅r = \varnothing 的步骤保持上下文不变,且 S∪δ(∅)=SS \cup \delta(\varnothing) = S;否则该步骤令 Sk+1=Sk∪δ(rk+1)S_{k+1} = S_k \cup \delta(r_{k+1})。第二个等号即 δ\delta 的同态性质。□\square

推论:状态只增不减(Sk⊆Sk+1S_k \subseteq S_{k+1}),与各步信号的顺序无关,并且只要引发过任何无效运算情形就有 InvalidOperation∈Sn\texttt{InvalidOperation} \in S_n。触发陷阱的那一步也包括在内,因为状态在陷阱判定之前更新;而 ρ\rho 保持状态,因此该定理可跨越 resume_defined 延续。

第一个陷阱终结流水线

定理。 在流水线 xk=opk(xk−1)x_k = \mathrm{op}_k(x_{k-1}) 中,若第 jj 步是第一个结果为 Trapped 的步骤,则除非应用 resume_defined,对每个 n≥jn \ge j 都有 xn=xjx_n = x_j。

证明。 每个运算方法都对结果做模式匹配,并对 Trapped 返回 self,因此 k>jk > j 时 xk=xk−1x_{k} = x_{k-1};对 kk 归纳即得。□\square

结合选择器 τ\tau,报告的信号是确定的:它是第一个触发陷阱的步骤所引发的、优先级最高的被捕获信号。

陷阱取决于当前步骤,而非历史

陷阱判定使用当前步骤引发的信号 rr,而不是状态 SS。先前在未设置该陷阱的上下文中引发的信号不会使后续步骤触发陷阱,清除状态也不影响陷阱判定。这与 GDA 一致:在 GDA 中,陷阱是引发该情形的那个运算的事件。

开销

每一步的代价是 GDA 运算本身,加上对两个 13 字段记录的常数量工作。运算未引发任何信号时,上下文原样传递。

被否决的替代方案

  • 把陷阱表示为 ArithmeticError。 会丢失确定结果和下一个上下文。
  • 自动恢复。 会掩盖接受被陷阱捕获结果的决定;GDA 把这一决定留给处理程序。
  • 流水线上的运算符。 理由与合并上下文相同。
  • 恢复时清除状态。 会抹去曾经发生过被陷阱捕获情形的证据。

边界

  • 本包没有自己的算术;所有运算都来自 decimal_gda。
  • 只有生成接口中的运算集合拥有流水线方法;其他 decimal_gda 运算需在 value() / context() 上执行,再用 from_outcome 重新包装。
  • 没有 ArithmeticError,也没有 IEEE DecimalFlags;IEEE 风格的标志累积属于 decimal_checked 的契约。
  • 不合并流水线,不隐式恢复,流水线执行期间不修改陷阱集合。

Footnotes

  1. M. Cowlishaw,General Decimal Arithmetic Specification,1.70 版,“Context”(标志与陷阱使能)和 “Exceptional conditions” 两节。 ↩

  2. E. Moggi,“Notions of computation and monads”,1991(状态单子与异常单子);P. Wadler,“Monads for functional programming”,1995。 ↩