core 设计

设计目标

arithmetic 是位于代数结构与具体数值之间的一层。luna-generic 说明一个类型是什么（环、域）；arithmetic 则说明一个类型能做哪些分析运算，以及做得有多诚实：平方根是否可能静默返回 NaN，是否会报告被拒绝的参数，还是在给定精度下同时报告结果是如何舍入的。泛型算法恰好声明它所依赖的能力，数值后端也恰好实现那些它能遵守其语义的能力。

本包提供词汇（trait、上下文、诊断与错误），以及针对原生 Float、Double 和整数类型的一组基础实例。正确舍入、忠实遵循上下文以及经认证的算术由数值后端提供，它们实现这些 trait。

数学背景

浮点格式

基数为 $\beta$、精度为 $p$、指数范围为 $[e_{\min}, e_{\max}]$ 的浮点格式是如下有限集合

$$\mathbb{F} = \{0\} \cup \{\, \pm m \cdot \beta^{\,e-p+1} \;:\; m \in \mathbb{Z},\ \beta^{p-1} \le m < \beta^{p},\ e_{\min} \le e \le e_{\max} \,\} \cup \{\, \pm m \cdot \beta^{\,e_{\min}-p+1} \;:\; 0 < m < \beta^{p-1} \,\}.$$

第二个集合是正规数，其首位数字位于 $\beta^{e}$（$e$ 称为调整指数）；第三个集合是低于 $\beta^{e_{\min}}$ 的次正规数。IEEE 754 把 $\mathbb{F}$ 扩展为 $\overline{\mathbb{F}} = \mathbb{F} \cup \{-\infty, +\infty, \mathrm{NaN}\}$，并带有有符号零。FpClass 是如下映射

$$\operatorname{class} : \overline{\mathbb{F}} \to \{\texttt{Finite}, \texttt{Infinity}, \texttt{NaN}\}, \qquad \operatorname{class}(x) = \begin{cases} \texttt{Finite} & x \in \mathbb{F},\\ \texttt{Infinity} & x = \pm\infty,\\ \texttt{NaN} & x = \mathrm{NaN}. \end{cases}$$

格式	$\beta$	$p$	$e_{\min}$	$e_{\max}$	来源
binary32	2	24	$-126$	$127$	Float
binary64	2	53	$-1022$	$1023$	Double
decimal32	10	7	$-95$	$96$	ArithmeticContext::decimal32
decimal64	10	16	$-383$	$384$	ArithmeticContext::decimal64
decimal128	10	34	$-6143$	$6144$	ArithmeticContext::decimal128

ArithmeticContext 把 $p$ 存为 precision，把调整指数的上下界存为 e_min 和 e_max；基数是后端类型的属性，而不是上下文的属性。三个十进制预设都满足 $e_{\min} = 1 - e_{\max}$，这是 IEEE 754 中的一条关系，它保证最小正规数的倒数 $\beta^{-e_{\min}} = \beta^{e_{\max}-1}$ 仍位于有限范围内。

机器 epsilon。 $1$ 在 $\mathbb{F}$ 中的后继是 $1 + \beta^{1-p}$：写出 $1 = \beta^{p-1} \cdot \beta^{\,0-p+1}$，得到 $m = \beta^{p-1}$ 和 $e = 0$，下一个有效数 $m + 1$ 给出

$$(\beta^{p-1} + 1)\,\beta^{1-p} = 1 + \beta^{1-p} =: 1 + \varepsilon .$$

更一般地，在 binade $[\beta^{e}, \beta^{e+1})$ 内，相邻两数相距 $\beta^{e-p+1} = \varepsilon\,\beta^{e}$。epsilon_contextual 返回 $\varepsilon$：对 Float 为 $2^{-23}$，对 Double 为 $2^{-52}$。

舍入

舍入函数 $\circ : \mathbb{R} \to \overline{\mathbb{F}}$ 把实数映射为可表示值。若 $a < x < b$ 是 $x \notin \mathbb{F}$ 的两个相邻值：

$$\begin{aligned} \operatorname{RN}(x) &= \text{the nearer of } a, b \text{ (ties to the even significand)} && \texttt{ToNearestEven}\\ \operatorname{RZ}(x) &= \text{the one of smaller magnitude} && \texttt{TowardZero}\\ \operatorname{RU}(x) &= b && \texttt{TowardPositive}\\ \operatorname{RD}(x) &= a && \texttt{TowardNegative}\\ \operatorname{RA}(x) &= \text{the one of larger magnitude} && \texttt{AwayFromZero} \end{aligned}$$

并且当 $x \in \mathbb{F}$ 时，每种模式都返回 $x$ 本身。每种模式都是单调的，即 $x \le y \Rightarrow \circ(x) \le \circ(y)$，并且在 $\mathbb{F}$ 上是幂等的；下文的认证论证只用到这两条性质。

相对误差。 设 $x$ 位于正规范围内，$\beta^{e} \le |x| < \beta^{e+1}$，且 $e_{\min} \le e \le e_{\max}$。$x$ 的两个相邻值相距 $\varepsilon\beta^{e}$，因此定向舍入模式使 $x$ 的移动小于一个间距，而就近舍入至多移动半个间距：

$$\begin{aligned} |\operatorname{RN}(x) - x| &\le \tfrac12\,\varepsilon\,\beta^{e} \le \tfrac12\,\varepsilon\,|x|,\\ |\circ_{\text{dir}}(x) - x| &< \varepsilon\,\beta^{e} \le \varepsilon\,|x|. \end{aligned}$$

因此 $\circ(x) = x(1 + \delta)$，其中 $|\delta| \le u$，单位舍入误差为

$$u = \begin{cases} \tfrac12\,\beta^{1-p} & \texttt{ToNearestEven},\\ \beta^{1-p} & \text{directed modes}. \end{cases}$$

格式	对 ToNearestEven 为 $u$
binary32	$2^{-24} \approx 5.96 \times 10^{-8}$
binary64	$2^{-53} \approx 1.11 \times 10^{-16}$
decimal32	$5 \times 10^{-7}$
decimal64	$5 \times 10^{-16}$
decimal128	$5 \times 10^{-34}$

在 $\beta^{e_{\min}}$ 以下，间距不再缩小，相对误差界变为绝对误差界：$|\operatorname{RN}(x) - x| \le \tfrac12\,\beta^{e_{\min}-p+1}$。超过最大有限数时，$\circ(x)$ 依舍入模式为 $\pm\infty$ 或最大有限数。这些就是 ArithmeticDiagnostics 中的 subnormal、underflow 和 overflow 条件。

舍入误差的标准模型

IEEE 754 要求 $+, -, \times, /$ 和 $\sqrt{\ }$ 是正确舍入的：计算结果就是精确结果的舍入。结合上面的误差界，对于 $\mathbb{F}$ 中的操作数以及位于正规范围内的结果，有

$$\operatorname{fl}(x \circ y) = (x \circ y)(1 + \delta), \qquad |\delta| \le u, \qquad \circ \in \{+, -, \times, /\}.$$

这正是上下文算术 trait 的契约：忠实遵循上下文的 AddContextual 按上下文的 $p$ 和舍入模式返回 $\operatorname{fl}(x + y)$，并且恰好在 $\delta \ne 0$ 时设置 inexact。这也是上下文之所以重要的原因：对于 decimal64 和 ToNearestEven，无论后端类型是什么，算法都可以依赖每次运算满足 $|\delta| \le 5 \times 10^{-16}$。

内置的 Float 和 Double 实例在就近舍入下对其自身的固定格式满足该模型，因为硬件运算是正确舍入的；但它们忽略上下文的精度和模式，也不检测 $\delta \ne 0$。它们的初等函数来自 Kaida-Amethyst/math，不保证正确舍入，因此对它们而言，该模型只在 $u$ 的某个未指明的小倍数下成立。

相邻值与 IEEE 编码

AdjacentContextual 计算

$$\operatorname{succ}(x) = \min\{\, y \in \overline{\mathbb{F}} : y > x \,\}, \qquad \operatorname{pred}(x) = \max\{\, y \in \overline{\mathbb{F}} : y < x \,\}.$$

Float 和 Double 实例在位模式上计算它们。对于 $k$ 位格式，符号为 $s$、带偏置指数字段为 $E$、尾数字段为 $F$ 的 IEEE 二进制值存储为无符号整数 $\operatorname{bits}(x) = s \cdot 2^{k-1} + E \cdot 2^{p-1} + F$。在非负值上，这个映射是保序的：

• 对固定的 $E$，值 $2^{E - \text{bias}}(1 + F\,2^{1-p})$（当 $E = 0$ 时为 $2^{1-\text{bias}}\,F\,2^{1-p}$）随 $F$ 严格递增；
• 字段为 $E$ 的最大值是 $2^{E-\text{bias}}(2 - 2^{1-p}) < 2^{E+1-\text{bias}}$，即字段为 $E + 1$ 的最小值；次正规数（$E = 0$）全部位于最小正规数 $2^{1-\text{bias}}$ 之下；
• $+\infty$ 为 $E = 2^{k-p} - 1$、$F = 0$，大于所有有限位模式。

由于编码按 $(E, F)$ 的字典序排列，而 $(E, F)$ 上的字典序就是 $E \cdot 2^{p-1} + F$ 上的整数序，因此对 $0 \le x < y$ 有 $\operatorname{bits}(x) < \operatorname{bits}(y)$，并且相邻两值之间不存在严格位于其间的位模式。所以

$$\operatorname{succ}(x) = \begin{cases} \operatorname{bits}^{-1}(\operatorname{bits}(x) + 1) & x > 0,\\ \operatorname{bits}^{-1}(\operatorname{bits}(x) - 1) & x < 0 \quad (\text{since } \operatorname{succ}(x) = -\operatorname{pred}(|x|)),\\ \text{smallest positive subnormal} & x = \pm 0, \end{cases}$$

$\operatorname{pred}$ 的情形对称。零的情形需要单独处理，因为 $+0$ 和 $-0$ 值相等但位模式不同。该公式重现了 API 中列出的边界情形：最大有限位模式加一就是 $+\infty$ 的位模式，且 $\operatorname{succ}(1) - 1 = \varepsilon$。由于按定义 $\operatorname{succ}(x)$ 属于 $\overline{\mathbb{F}}$，不会发生舍入，因此这些实例返回的空诊断是精确的，而不仅仅是“未检测到”。

包络与三值比较

包络 $X \subseteq \mathbb{R}$ 代表一个已知满足 $x \in X$ 的未知实数 $x$：区间 $[a, b]$，或球 $B(m, r) = [m - r, m + r]$。包络关系 trait 仅凭包络本身回答关于未知值的问题，方法是对每一对容许值进行量化：

$$\begin{aligned} \texttt{definitely\_lt}(X, Y) &\iff \forall x \in X,\ \forall y \in Y:\ x < y,\\ \texttt{definitely\_le}(X, Y) &\iff \forall x \in X,\ \forall y \in Y:\ x \le y,\\ \texttt{maybe\_eq}(X, Y) &\iff \exists x \in X,\ \exists y \in Y:\ x = y \iff X \cap Y \ne \emptyset,\\ \texttt{overlaps}(X, Y) &\iff X \cap Y \ne \emptyset,\\ \texttt{contains}(X, Y) &\iff Y \subseteq X. \end{aligned}$$

区间公式。 设 $X = [a, b]$ 和 $Y = [c, d]$ 非空。

$$\texttt{definitely\_lt}(X, Y) \iff b < c .$$

（$\Rightarrow$）取 $x = b \in X$、$y = c \in Y$。（$\Leftarrow$）对任意 $x \in X$、$y \in Y$：$x \le b < c \le y$。用 $\le$ 作同样的论证，得到 $\texttt{definitely\_le}(X, Y) \iff b \le c$。可能关系是存在性的：

$$\exists x \in X,\ \exists y \in Y:\ x < y \iff a < d .$$

（$\Rightarrow$）$a \le x < y \le d$。（$\Leftarrow$）取 $x = a$、$y = d$。它不需要单独的 trait，因为它就是交换参数后某个确定关系的否定：

$$\neg\,\texttt{definitely\_le}(Y, X) \iff \neg\,\forall y, x:\ y \le x \iff \exists x, y:\ x < y \iff a < d .$$

最后，$X \cap Y \ne \emptyset \iff a \le d \wedge c \le b$：若两者都成立，则 $\max(a, c) \le \min(b, d)$ 是一个公共点；反之，公共点 $z$ 给出 $a \le z \le d$ 和 $c \le z \le b$。对于球，代入端点得到 $\texttt{definitely\_lt}(B(m_1, r_1), B(m_2, r_2)) \iff m_1 + r_1 < m_2 - r_2$。

三值真值。 仅凭包络，“$x < y$”具有以下三种真值之一：

$$[\![\, x < y \,]\!] = \begin{cases} \mathsf{T} & \texttt{definitely\_lt}(X, Y),\\ \mathsf{F} & \texttt{definitely\_le}(Y, X),\\ \mathsf{U} & \text{otherwise}. \end{cases}$$

这个值是良定义的：同时为 $\mathsf{T}$ 和 $\mathsf{F}$ 需要 $b < c$ 且 $d \le a$，从而 $a \le b < c \le d \le a$，矛盾。同理，当 $\neg\,\texttt{maybe\_eq}(X, Y)$ 时 $[\![\, x = y \,]\!]$ 为 $\mathsf{F}$，否则为 $\mathsf{U}$，除非两个包络是同一个单点。复合条件按 Kleene 强三值逻辑组合：

$p$	$q$	$\neg p$	$p \wedge q$	$p \vee q$
$\mathsf{T}$	$\mathsf{T}$	$\mathsf{F}$	$\mathsf{T}$	$\mathsf{T}$
$\mathsf{T}$	$\mathsf{U}$	$\mathsf{F}$	$\mathsf{U}$	$\mathsf{T}$
$\mathsf{T}$	$\mathsf{F}$	$\mathsf{F}$	$\mathsf{F}$	$\mathsf{T}$
$\mathsf{U}$	$\mathsf{T}$	$\mathsf{U}$	$\mathsf{U}$	$\mathsf{T}$
$\mathsf{U}$	$\mathsf{U}$	$\mathsf{U}$	$\mathsf{U}$	$\mathsf{U}$
$\mathsf{U}$	$\mathsf{F}$	$\mathsf{U}$	$\mathsf{F}$	$\mathsf{U}$
$\mathsf{F}$	$\mathsf{T}$	$\mathsf{T}$	$\mathsf{F}$	$\mathsf{T}$
$\mathsf{F}$	$\mathsf{U}$	$\mathsf{T}$	$\mathsf{F}$	$\mathsf{U}$
$\mathsf{F}$	$\mathsf{F}$	$\mathsf{T}$	$\mathsf{F}$	$\mathsf{F}$

把 $\mathsf{U}$ 理解为“对某些容许值为真、对另一些为假”，则表中每一项都是对所有容许值都成立的最强陈述；例如 $\mathsf{F} \wedge \mathsf{U} = \mathsf{F}$，因为只要有一个合取项为假，无论另一项如何，合取都为假。¹1 S. C. Kleene, Introduction to Metamathematics, 1952, §64。具有三种结果的区间比较可追溯到 R. E. Moore, Interval Analysis, 1966。

认证阶段

基于证明的后端通过一条流水线计算 $\circ_{p_t}(f(x))$，即超越函数 $f$ 在目标精度 $p_t$ 下的正确舍入，流水线的各阶段就是 CertificationStage 的取值。以 $f = \exp$ 为例：

1. RangeReduction：写成 $x = k \ln 2 + r$，其中 $k \in \mathbb{Z}$ 且 $|r| \le \tfrac12 \ln 2$，从而 $\exp(x) = 2^{k}\exp(r)$。约简后的参数 $r$ 本身也必须被包络，这需要 $\ln 2$ 额外约 $\log_2 |x|$ 位的精度。

2. SeriesEvaluation：求和 $\sum_{j<N} r^{j}/j!$ 并界定余项。当 $|r| < N + 1$ 时，

   $$\Bigl|\sum_{j \ge N} \frac{r^{j}}{j!}\Bigr| \le \frac{|r|^{N}}{N!}\sum_{i \ge 0}\Bigl(\frac{|r|}{N+1}\Bigr)^{i} = \frac{|r|^{N}}{N!}\cdot\frac{1}{1 - |r|/(N+1)},$$

   这里用到了 $\frac{N!}{(N+i)!} \le (N+1)^{-i}$。

3. EnclosurePropagation：把截断误差界和工作精度 $p_w > p_t$ 下的每一个舍入误差传递到其余运算中，得到包络 $[\ell, h] \ni f(x)$。

4. TargetRounding：若 $\circ_{p_t}(\ell) = \circ_{p_t}(h)$，则该值就是答案，因为由单调性

   $$\ell \le f(x) \le h \;\Longrightarrow\; \circ_{p_t}(\ell) \le \circ_{p_t}(f(x)) \le \circ_{p_t}(h) = \circ_{p_t}(\ell).$$

   否则 $[\ell, h]$ 跨越了一个舍入边界：后端提高 $p_w$ 并重复计算，这就是 Ziv 策略。²2 A. Ziv, “Fast evaluation of elementary mathematical functions with correctly rounded last bit”, ACM TOMS 17(3), 1991。$f(x)$ 能多么接近舍入边界，这就是所谓的制表者困境（table maker’s dilemma）；对大多数函数而言，并不知道关于 $p_w$ 的有用先验界，这正是循环需要预算的原因。

当循环放弃时，后端返回 ArithmeticError::certification_failure，其中携带阶段、原因、$p_t$（target_precision）、最后的 $p_w$（work_precision）以及提高精度的次数（refinements）。在 TargetRounding 阶段，预期的原因是 RefinementBudgetExhausted；其他原因属于更早的阶段。本包只定义词汇，不进行任何求值。

设计决策

三个层级，而非单一签名

问题。 在紧凑循环中对 Double 求平方根，需要的是 fn sqrt(Double) -> Double，并接受负参数得到 NaN。十进制后端则需要精度和舍入模式，并且必须报告结果是否经过舍入。单一签名无法同时满足两者：要么强迫每次原生调用都带上 Result 和上下文，要么丢弃十进制调用方所需的信息。

可选方案。 (a) 只有非检查 trait；(b) 只有上下文 trait；(c) 三个相互独立的层级。

选择。 (c)。各层级携带的信息依次增多，并且每一层的结果类型都可以嵌入下一层：

$$\underbrace{T}_{\text{unchecked}} \;\xrightarrow{\;v \,\mapsto\, \mathrm{Ok}(v)\;}\; \underbrace{\mathrm{Result}[T, E]}_{\text{checked}} \;\xrightarrow{\;\mathrm{Ok}(v) \,\mapsto\, \mathrm{Ok}(v, \mathbf{0})\;}\; \underbrace{\mathrm{Result}[(T, D), E]}_{\text{contextual}},$$

其中 $D$ 是诊断集合，$\mathbf{0}$ 是其空值。除 Float 的整数嵌入外，内置的上下文适配器正是把这些嵌入应用于检查或非检查结果。约束表明算法能处理什么：T : Sqrt 接受后端自身的行为，T : SqrtChecked 处理拒绝，T : SqrtContextual 需要上下文和诊断。各层级之间没有 supertrait 关系，因此一个类型恰好实现它能遵守的那些层级：区间类型可以实现 DivChecked 和包络关系，而不必假装拥有一个不依赖上下文的 Sqrt。

上下文与诊断是显式的值

问题。 IEEE 754 把舍入方向和状态标志描述为执行环境的属性；C 通过 <fenv.h> 暴露它们，Python 的 decimal 则维护一个线程局部的当前上下文。两者都是隐藏状态：a + b 的结果依赖于某个并非参数的东西，而在一次计算中设置的标志在下一次计算中仍然存在。

可选方案。 (a) 全局可变上下文；(b) 线程局部或任务局部的上下文；(c) 把上下文作为参数，把标志放在返回值中。

选择。 (c)。每个上下文运算都是一个函数

$$\operatorname{op} : T^{n} \times \texttt{ArithmeticContext} \to \mathrm{Result}[(T, D), E],$$

因此相同的输入给出相同的输出，一次计算的诊断恰好是它所组合的各运算的诊断。这在所有 MoonBit 目标上表现一致（它们都不需要线程局部存储），使并发使用是安全的，并且测试可以完整给出一次运算的全部输入。代价是写法较为冗长，后端可以用自己的辅助函数来减轻。

错误、诊断与认证失败相互分离

问题。 IEEE 754 有五种异常：无效运算、除以零、上溢、下溢和不精确。其中一些描述的是不存在的结果，另一些描述的是存在但经过舍入的结果。

选择。 本包按是否返回值来划分它们：

情形	通道	IEEE 754 对应项
没有有意义的值（定义域错误、不定式）	Err, DomainError	无效运算
极点：有限非零值除以零	Err, DivisionByZero	除以零
$\overline{\mathbb{F}}$ 中与精确值不同的值	Ok，带 inexact、rounded	不精确
超出有限范围或低于正规范围的值	Ok，带 overflow、underflow、subnormal	上溢、下溢
输入有效但结果无法认证	Err, CertificationFailure	无

标志不能掩盖错误，也不能为了携带标志而凭空制造错误：$\operatorname{fl}(10^{300} \times 10^{300}) = +\infty$ 是正确的 IEEE 答案，所以它是一个带 overflow 的值，而不是失败。认证失败属于错误，但不是定义域错误：输入是有效的，更大的预算可能会成功，因此它携带调用方决定是否重试所需的数据。本包不强加任何重试策略。

包络关系不是序

问题。 区间看起来是有序的，为它们实现 Compare 会让泛型排序代码接受它们。

选择。 五个独立的关系 trait。Compare 承诺的是全序，但非空区间上的 definitely_lt 只是严格偏序。它是反自反的（对 $[a, b]$，$b < a$ 不成立）且是传递的：

$$b_1 < c_2 \;\wedge\; b_2 < c_3 \;\Longrightarrow\; b_1 < c_2 \le b_2 < c_3 \;\Longrightarrow\; b_1 < c_3 ,$$

但它不是全序：对于相互重叠的 $X, Y$，$\texttt{definitely\_lt}(X, Y)$ 和 $\texttt{definitely\_lt}(Y, X)$ 都不成立，二者也不相等。Compare 实例在这里必须回答 $<, =, >$ 之一，从而会对未知值断言某个错误的结论。

原生标量只实现它们能遵守的能力

问题。 Float 和 Double 可以通过忽略上下文来实现每一个 trait。

选择。 它们只在结果有意义时才实现某项能力：

• 所有非检查 trait 以及 Power，它们不承诺超出后端本身的任何东西；
• 检查 trait，它们唯一额外的承诺是拒绝无效参数；
• 上下文算术、绝对值、平方根与指数、整数嵌入、相邻值和格式查询，作为适配器实现，使泛型上下文代码也能在原生标量上运行；
• 不实现 ConstantsContextual 和 HyperbolicContextual，它们的目的在于给出遵循任意精度并带有有意义诊断的结果；固定精度的库函数无法做到这一点。

在固定格式使结果精确的地方（相邻值、Double 整数嵌入），这些适配器是诚实的；在检测代价较低的地方（Float 整数嵌入，见下文），它们会检测精度损失。算术适配器不检测舍入：它们的空诊断表示“未检测到”。API 页在使用处说明了这一点。

每个 trait 一项能力，不设 Real

像 Real : Field + Sqrt + Exponential + Trigonometric + Compare 这样的 trait 用起来方便，但会掩盖重要的差异：区间类型没有全序，十进制类型没有廉价的 sin，整数类型有 Power 却没有 Sqrt。本包中的每个 trait 都只表示一项能力，算法组合它所用到的约束，例如求斜边时用 T : Add + Mul + Sqrt。Radical 是唯一的合取，因为平方根和立方根经常需要一起使用。

三个浮点类别

IEEE 754 的 class 区分十个类别（signalling NaN 与 quiet NaN、负无穷与正无穷、正规数、次正规数和零，各分正负）。FpClass 只保留三个，因为泛型代码正是依据这些情形进行分支：有限值可以进入后续算术，无穷是有效的极限，而 NaN 是无效的。符号、零和次正规性则用该格式自身的 API 检测。

IntegralContextual 只嵌入 Int

每个后端都能接收 MoonBit 的 Int，而循环计数器和下标都是 Int。嵌入 BigInt 会要求每个后端都支持任意精度舍入；这留给一项单独的能力，从而让常见情形的实现保持低成本。

Power 保持单一签名

Power::pow(Self, Self) 对浮点类型和整数类型相同，因此泛型的幂运算不依赖于类型族。代价是指数类型就是底数类型：有符号整数和 BigInt 实例遇到负指数时必须中止，因为一般而言 $x^{-n} \notin \mathbb{Z}$。需要明确失败行为的代码应使用 PowNatChecked（指数为 UInt）或 PowIntChecked（指数为 Int）。

正确性与不变量

上下文不变量

ArithmeticContext::new 通过截断保证 $p \ge 1$，并通过中止保证 $e_{\min} \le e_{\max}$（当两者都存在时），而且这些字段在包外是只读的。因此每个上下文值都满足这两条，后端无需再次检查。

combine 的定律

ArithmeticDiagnostics 是布尔格 $D = \{0, 1\}^{6}$，combine 是逐分量的 $\vee$。由于每个分量都满足布尔定律，对所有 $d_1, d_2, d_3 \in D$：

$$\begin{aligned} (d_1 \vee d_2) \vee d_3 &= d_1 \vee (d_2 \vee d_3) && \text{associativity}\\ d_1 \vee d_2 &= d_2 \vee d_1 && \text{commutativity}\\ d \vee d &= d && \text{idempotence}\\ d \vee \mathbf{0} &= d && \mathbf{0} = \texttt{empty()} \end{aligned}$$

因此 $(D, \vee, \mathbf{0})$ 是一个交换的幂等幺半群，也就是带最小元的并半格。一次计算的诊断是其各步诊断的并，与求值顺序和结合方式无关，并且一个标志一旦设置，就不会因组合而被清除。

上下文运算的顺序组合

组合两个上下文运算 $f : A \to \mathrm{Result}[(B, D), E]$ 和 $g : B \to \mathrm{Result}[(C, D), E]$，得到

$$(g \mathbin{\bar\circ} f)(a) = \begin{cases} \mathrm{Err}(e) & f(a) = \mathrm{Err}(e),\\ \mathrm{Err}(e) & f(a) = \mathrm{Ok}(b, d_1),\ g(b) = \mathrm{Err}(e),\\ \mathrm{Ok}(c, d_1 \vee d_2) & f(a) = \mathrm{Ok}(b, d_1),\ g(b) = \mathrm{Ok}(c, d_2). \end{cases}$$

这是叠加在错误单子之上、基于 $(D, \vee, \mathbf{0})$ 的 writer 单子，而上面的幺半群定律恰好保证 $\bar\circ$ 满足结合律，并以 ArithmeticOutcome::exact 为单位元。³3 $\bar\circ$ 的结合律归结为诊断上 $\vee$ 的结合律以及值上函数复合的结合律；单位元律归结为 $d \vee \mathbf{0} = d$。参见 E. Moggi, “Notions of computation and monads”, 1991。 本包提供的是各个构件（exact、with_diagnostics、combine），而不是组合子；教程展示了一个简短的辅助函数。

整数嵌入到 Float

binary32 的 $p = 24$。满足 $|n| \le 2^{24}$ 的整数 $n$ 至多有 24 位有效位（或者就是 2 的幂 $2^{24}$ 本身），因此是可表示的；$2^{24} + 1$ 需要 25 位有效位，因此不可表示，就近偶数舍入把它变为 $2^{24}$。Float 实例无需宽整数比较即可检测这种损失：binary64 的 $p = 53 > 31$，所以 Double::from_int 对每个 Int 都是精确的，并且每个 binary32 值都是 binary64 值，所以扩展转换也是精确的。因此

$$\operatorname{double}(\operatorname{RN}_{32}(n)) = \operatorname{double}(n) \iff \operatorname{RN}_{32}(n) = n ,$$

并且该实例恰好在转换丢失信息时设置 inexact 和 rounded。不可能发生上溢，因为 $|n| \le 2^{31} < 2^{128}$。

二进制快速幂的误差界

Float 和 Double 的 PowNatChecked 用如下循环计算 $x^{n}$

$$\textit{acc} \leftarrow 1,\ \textit{f} \leftarrow x,\ k \leftarrow n;\quad \text{while } k > 0:\ \text{if } k \text{ odd}: \textit{acc} \leftarrow \textit{acc}\cdot \textit{f};\ k \leftarrow \lfloor k/2 \rfloor;\ \text{if } k > 0: \textit{f} \leftarrow \textit{f}^{2}.$$

正确性。 在精确算术下，每次迭代开始时 $\textit{acc}\cdot \textit{f}^{\,k} = x^{n}$ 成立。它在初始时成立；若 $k = 2j + 1$，则 $\textit{acc}\,\textit{f}\cdot(\textit{f}^{2})^{j} = \textit{acc}\,\textit{f}^{\,k}$；若 $k = 2j$，则 $\textit{acc}\,(\textit{f}^{2})^{j} = \textit{acc}\,\textit{f}^{\,k}$。当 $k = 0$ 时，该不变量给出 $\textit{acc} = x^{n}$。循环执行 $\lfloor \log_2 n \rfloor + 1$ 次，进行 $\lfloor\log_2 n\rfloor$ 次平方和 $\operatorname{popcount}(n)$ 次乘积，其中第一次乘积（$1 \cdot \textit{f}$）是精确的。整数 Power 实例在 $\mathbb{Z}/2^{k}$ 中使用同一不变量，其中每一步都是精确的。

舍入误差。 对每个近似 $x^{m}$ 的计算量 $q$ 赋予一个误差计数 $c(q)$，使得 $q = x^{m}\prod_i (1 + \delta_i)^{k_i}$，其中 $|\delta_i| \le u$ 且 $\sum_i k_i \le c(q)$。于是 $c(x) = 0$，而 $q_1 \approx x^{m_1}$ 与 $q_2 \approx x^{m_2}$ 的一次舍入乘积满足 $c \le c(q_1) + c(q_2) + 1$。由归纳法得 $c(q) \le m - 1$：

$$c(q_1 q_2) \le (m_1 - 1) + (m_2 - 1) + 1 = (m_1 + m_2) - 1,$$

平方是 $q_1 = q_2$ 的情形，此时共享的误差被计算两次。因此，在不发生上溢和下溢时，

$$\operatorname{fl}(x^{n}) = x^{n}(1 + \theta_{n-1}), \qquad |\theta_{n-1}| \le (1 + u)^{n-1} - 1 \le \gamma_{n-1} := \frac{(n-1)u}{1 - (n-1)u}.$$

最后一步是标准引理：当 $ku < 1$ 时 $|\prod_{i=1}^{k}(1+\delta_i)^{\pm 1} - 1| \le \gamma_k$。⁴4 N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002, Lemma 3.1 与 §3.1。 指数为负时，PowIntChecked 再做一次除法，由 $(1 + \delta)/(1 + \theta_{n-1})$ 得到 $|\theta| \le \gamma_{n}$。二进制快速幂并不能改进 $n - 1$ 次连续乘法的最坏情况误差界；它把工作量从 $n - 1$ 次乘法降低到 $O(\log n)$ 次。

检查除法

Float 和 Double 的 DivChecked 实例拒绝所有零除数，并用错误类别说明原因。$0/0$ 和 $\infty/\infty$ 是不定式：当 $t \to 0$ 或 $t \to \infty$ 时，极限 $\lim (\lambda t)/t = \lambda$ 可以取任意值，因此任何商都没有意义，类别为 DomainError。对 $x \ne 0$，当 $t \to 0$ 时 $x/t$ 发散，这是一个极点，类别为 DivisionByZero。这与 IEEE 754 的无效运算和除以零异常相对应，但更为严格：IEEE 对 $\infty/0$ 静默返回 $\pm\infty$，对 NaN$/0$ 静默返回 NaN，而检查实例返回 DivisionByZero。被除数为 NaN 且除数非零时，仍以 Ok(NaN) 传播；SqrtChecked 同样放行 NaN：检查运算拒绝无效参数，但不会重复报告先前的无效结果。

包络关系的可靠性与单调性

可靠性。 若 $x \in X$、$y \in Y$ 且 $\texttt{definitely\_lt}(X, Y)$，则 $x < y$：该关系是关于 $X \times Y$ 的全称陈述，而该集合包含 $(x, y)$。对偶地，若 $\neg\,\texttt{maybe\_eq}(X, Y)$，则 $x \ne y$。

细化下的单调性。 若 $X' \subseteq X$ 且 $Y' \subseteq Y$，则

$$\texttt{definitely\_lt}(X, Y) \Rightarrow \texttt{definitely\_lt}(X', Y'), \qquad \texttt{maybe\_eq}(X', Y') \Rightarrow \texttt{maybe\_eq}(X, Y),$$

因为全称陈述在定义域缩小后仍然成立，而存在陈述在定义域扩大后仍然成立。用三值逻辑的话说，细化包络可以把 $\mathsf{U}$ 变为 $\mathsf{T}$ 或 $\mathsf{F}$，但绝不会把 $\mathsf{T}$ 变为 $\mathsf{F}$。正因如此，“细化直到能作出判定”的循环（例如上文的目标舍入阶段）才是正确的：一旦作出判定，它就始终有效。这类循环用 Contains 检查细化后的包络 $X'$ 是否位于原包络之内，即 $\texttt{contains}(X, X')$。

这些 trait 不规定空包络的约定；由各后端自行说明。按照量词解读，当参数为空时，确定关系会空真地成立，因此若后端希望 $\mathsf{T}$ 绝不来自信息的缺失，就应对空包络返回 false。

被否决的方案

• 带粘滞标志的全局或线程局部上下文，如 C 的 <fenv.h> 和 Python 的 decimal。否决理由见显式的值：它使结果依赖于隐藏状态，并让标志在不同计算之间泄漏。
• Real 或 Number 超 trait。 否决，因为它掩盖了精确类型、近似类型和以包络为值的类型之间的差异。
• 为包络实现 Compare。 否决，因为确定序不是全序。
• 用于比较的三值结果类型（True | False | Unknown）。如上所示，两个布尔投影 definitely_* 和 maybe_eq 足以重建它，并且它们可以与普通的 if 组合；单独的类型会迫使每个调用方都处理 $\mathsf{U}$，即使它只关心一个方向。
• definitely_eq 关系。 对于非退化的包络，它总是为假，因此它只能用来检测相等的单点。
• 把诊断作为错误报告。 否决，因为不精确或上溢的 IEEE 结果是正确答案，把它变成 Err 会使每个经过舍入的运算都失败。
• 用 Option 或 raise 表示检查结果。 Option 会丢失原因；MoonBit 的 raise 会把失败置于返回类型之外。Luna-Flow 在各仓库中统一使用带结构化错误的 Result。
• 通过忽略上下文为原生标量实现 ConstantsContextual 和 HyperbolicContextual。 否决，因为这些 trait 存在的意义就是承诺忠实遵循上下文的结果。

边界

• 本包不实现任意精度、十进制、区间或球算术，也不对经认证的函数求值；它定义的是这些后端所实现的 trait。
• 内置的 Float 和 Double 实例不遵循上下文的精度、舍入模式或指数范围，它们的算术适配器也不检测舍入、上溢或下溢。
• 本包不承诺 Float 和 Double 的初等函数是正确舍入的；它们来自 Kaida-Amethyst/math。
• 本包不定义代数结构（Ring、Field 等），这些属于 luna-generic；也不定义向量、矩阵、复数或多项式。
• 除各随包实例所继承的行为之外，本包不为非检查 trait 选定分支割线或特殊值约定。
• 本包不为认证失败规定重试或精度提升策略。

Footnotes

1. S. C. Kleene, Introduction to Metamathematics, 1952, §64。具有三种结果的区间比较可追溯到 R. E. Moore, Interval Analysis, 1966。 ↩

2. A. Ziv, “Fast evaluation of elementary mathematical functions with correctly rounded last bit”, ACM TOMS 17(3), 1991。$f(x)$ 能多么接近舍入边界，这就是所谓的制表者困境（table maker’s dilemma）；对大多数函数而言，并不知道关于 $p_w$ 的有用先验界，这正是循环需要预算的原因。 ↩

3. $\bar\circ$ 的结合律归结为诊断上 $\vee$ 的结合律以及值上函数复合的结合律；单位元律归结为 $d \vee \mathbf{0} = d$。参见 E. Moggi, “Notions of computation and monads”, 1991。 ↩

4. N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002, Lemma 3.1 与 §3.1。 ↩