`ball_float_checked` 设计

设计目标

ball_float_checked 使区间计算可以写成一条运算链，其中构造错误和无法认证的步骤都是显式错误，而每个成功的值仍是严格的包络。BallFloatResult 使 Result[BallFloat, ArithmeticError] 在 ball_float 的运算下封闭，且不添加任何区间算法。API 页面列出了这些运算，教程展示了流水线的用法。

数学背景

包络

记 $\mathbb{IR}$ 为 IEEE 1788-2015（基于集合的风格）意义下实数线上闭区间的集合：空集、有界区间 $[\ell, u]$ 、半直线以及 $\mathbb{R}$ 本身。¹1 IEEE 1788-2015，Standard for Interval Arithmetic，第 7–10 条。一个 BallFloat $X$ 表示 $\mathbb{IR}$ 中有限端点为二进制浮点数的元素。区间运算 $F$ 称为实函数 $f$ 的包络，当

\{\, f(t) : t \in X \cap \operatorname{dom} f \,\} \subseteq F(X) \qquad \text{for every } X,

二元运算同理。这正是 ball_float 所实现形式下的区间算术基本定理：用包络对公式求值，得到的是该公式值域的包络，因为包络性在复合下保持。若 $F$ 包络 $f$ 且 $G$ 包络 $g$ ，则

g(f(X \cap \operatorname{dom} f) \cap \operatorname{dom} g) \subseteq g(F(X) \cap \operatorname{dom} g) \subseteq G(F(X)),

第一步利用了像在 $\subseteq$ 下的单调性，第二步利用了 $G$ 的包络性质。²2 R. E. Moore、R. B. Kearfott、M. J. Cloud，Introduction to Interval Analysis，SIAM，2009，第 5 章；van der Hoeven，“Ball arithmetic”，2009。

作为错误单子的包装器

BallFloatResult 是异常单子 $M V = V + E$ ，其中 $V$ 为 BallFloat 值的集合， $E$ 为 ArithmeticError 值的集合， $\eta =$ ok 且 $\mathbin{>\!\!>\!\!=} =$ bind。单子定律（左、右单位律与结合律）以及 map 的函子定律在 bin_float_checked 设计中证明；该证明是对 $\mathrm{Ok}/\mathrm{Err}$ 的情形分析，不依赖 $V$ 的任何性质。运算符按相同的左偏方案提升（ball_result_lift2），因此首错误定理原样适用：表达式报告的是后序遍历中第一个产生错误的节点的错误。

设计决策

什么是错误，什么是值

问题。 区间计算可能以四种情形之一结束：输入不描述一个区间；运算对某个参数没有意义（零次根）；库无法认证足够紧致的包络；或真实值域为空或无界。

选择。 前三种是错误；第四种是值。

情形	结果	来源
NaN 界、 $\ell = +\infty$ 、 $u = -\infty$ 、 $\ell > u$	`DomainError`	`try_from_bounds`
非有限的 `exact`、`from_double`、`from_float` 源值	`DomainError`	`try_exact`, `try_from_double`, `try_from_float`
$0$ 次的 `rootn`	`DomainError`	`try_rootn`
包络无法在预算内认证	`CertificationFailure`	`try_*_interval`, `try_hypot`
值域为空（负数的 $\ln$ 、 $1/\{0\}$ ）	成功：空区间	区间运算
值域无界（ $1/[-1,1]$ ）	成功：整条实数线或半直线	区间运算

原因。 空的或无界的结果是真实值域的正确包络，因此将其变为错误会使包装器与基于集合的语义相悖： $\ln([-1, 1]) = [-\infty, 0]$ 是一个可靠的答案，而 $\ln(\{-2\}) = \varnothing$ 是精确答案。相比之下， $[+\infty, +\infty]$ 根本不是实数集合，而零次根对任何参数都无定义；这些属于调用者的错误。认证失败意味着库拒绝返回一个它无法证明的结果，这同样不是包络。若调用者在其应用中将空的或无界的结果视为失败，可用 bind 加上这条规则（参见教程）。

算术运算符不会失败

add、sub、mul 和 div 用 map 提升 BallFloat 运算符，因此它们从不引入错误：这四个集合运算在 $\mathbb{IR}$ 中总有包络（对于除法， $X / Y$ 定义为 $\{ s/t : s \in X, t \in Y \setminus \{0\} \}$ 的凸包，当 $Y = \{0\}$ 时为空）。算术表达式中的错误只可能来自其叶子。

幂通过 arithmetic trait 计算

pow_nat 和 pow_int 以 ArithmeticContext::new(x.precision()) 调用 Luna-Flow/arithmetic 的 PowNatChecked::pow_nat_checked 和 PowIntChecked::pow_int_checked。BallFloat 只从上下文中读取精度（舍入方向和指数界限对向外舍入的包络没有意义），对底数重设精度，并计算整个区间的幂。使用幂而非重复乘法可以避免依赖问题： $X \cdot X$ 把两个因子视为独立的，因此对 $X = [-1, 1]$ 给出 $[-1, 1]$ ，而 $\{t^2 : t \in X\} = [0, 1]$ 。

无装饰，无标志

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 先以 $\max(\textit{precision}, 8)$ 位就近舍入构建一个 BinFloat，再包络该值；在当前分支上，当整数所需位数超过精度时会丢失该整数（参见 API 页面中的警告）。

正确性 / 不变式

可靠性。 若表达式的每个叶子都是包络了预期实数输入的成功值，且表达式求值为 $\mathrm{Ok}(Y)$ ，则 $Y$ 包络实数公式在这些输入上的值域。这由上文的复合论证以及包装器对成功值恰好施加 ball_float 运算这一事实得出。
错误确定性。 若表达式求值为 $\mathrm{Err}(e)$ ，则 $e$ 是后序遍历中第一个产生错误的节点的错误。
无隐式恢复。 没有任何方法会把错误变为值，map 也从不把值变为错误（ $\texttt{map} = \mathbin{>\!\!>\!\!=} \circ\, (\eta \circ -)$ ）。
代价。 每个包装步骤在其所委托的区间运算之外增加 $O(1)$ 的工作量。

被否决的替代方案

将空结果视为错误。 破坏基于集合的语义，并会在存在可靠包络时对 $\ln([-1, 1])$ 报告错误。
在包装器中携带装饰。 会以第二套传播规则重复 ball_float 的装饰 API。
上下文变体（exp_ctx、…）。 包络在区间的精度下向外舍入；改变精度通过 with_precision 显式完成，它对任意舍入模式都能给出包络。
累积错误。 与二进制包装器一样，ArithmeticError 上没有合并运算。

边界

自身没有任何区间算法；所有包络都来自 ball_float。
不提供装饰、BallFlags、区间上下文或交换格式。
不提供错误恢复或累积；只保留第一个错误。
包装器本身不提供 Eq、Show 或包络关系；请用 result() 取出 BallFloat 来检测包含关系或顺序。
参数中超出定义域的部分会被忽略，而不报告。

IEEE 1788-2015，Standard for Interval Arithmetic，第 7–10 条。 ↩
R. E. Moore、R. B. Kearfott、M. J. Cloud，Introduction to Interval Analysis，SIAM，2009，第 5 章；van der Hoeven，“Ball arithmetic”，2009。 ↩

ball_float_checked 设计