`def` 设计

设计目标

def 为 floating 的四种表示（二进制 BinFloat、IEEE 十进制 @decimal.Decimal、GDA 十进制 @decimal_gda.Decimal 和区间 BallFloat）的共同之处提供一套统一词汇：值属于哪一类、符号是什么、以什么精度存储、如何转换到另一精度，以及它是其值的哪一个代表。它还为 IEEE 比较的结果命名，并重新导出 Luna-Flow/arithmetic 的上下文与错误类型。本包刻意保持精简：只陈述契约，不包含任何数值算法。API 页面列出了各项条目；教程演示了它们的用法。

数学背景

值及其含义

基数为 $\beta$ （BinFloat 为 $\beta = 2$ ，两种十进制均为 $\beta = 10$ ）的有限标量是由符号位 $s$ 、系数 $c \in \mathbb{N}$ 和指数 $e \in \mathbb{Z}$ 组成的三元组，表示实数

[\![x]\!] = (-1)^{s}\, c\, \beta^{e}.

多个三元组可以表示同一个实数：在十进制下 $(0, 15, -1)$ 和 $(0, 150, -2)$ 都表示 $1.5$ ， $(0, 0, e)$ 和 $(1, 0, e)$ 都表示 $0$ 。非有限标量表示 $\pm\infty$ ，或者是 NaN，NaN 不表示任何数。端点为 $\ell \le u$ 的非空 BallFloat 表示闭集 $X = \{\, t \in \mathbb{R} : \ell \le t \le u \,\}$ （无穷端点表示该侧无界），空区间表示 $\varnothing$ 。

对精度 $p \ge 1$ ，令

\mathbb{F}_{\beta,p} = \{\, (-1)^{s} c\, \beta^{e} : s \in \{0,1\},\ 0 \le c < \beta^{p},\ e \in \mathbb{Z} \,\}

为至多有 $p$ 位基数 $\beta$ 有效数字、指数无界的数。对方向 $m$ （RoundingMode），舍入函数 $\circ_{m,p} : \mathbb{R} \to \mathbb{F}_{\beta,p}$ 把实数映到 $\mathbb{F}_{\beta,p}$ 中相邻的元素： $\nabla$ （TowardNegative）映到 $\le t$ 的最大元素， $\Delta$ （TowardPositive）映到 $\ge t$ 的最小元素，TowardZero 映到这两者中绝对值较小的一个，AwayFromZero 映到较大的一个，ToNearestEven 映到较近的一个，平局时取偶数系数。¹1 IEEE 754-2019，第 4.3 条（舍入方向属性）。AwayFromZero 不是 IEEE 二进制属性；它对应 GDA 的舍入 Up（Cowlishaw，General Decimal Arithmetic Specification）。

IEEE 比较关系

IEEE 754 对比较的定义使得任意一对浮点数据之间恰好成立四种关系之一：小于、等于、大于和无序。²2 IEEE 754-2019，第 5.11 条（比较谓词的细节）及表 5.1。静默谓词与信号谓词的区别仅在于静默 NaN 操作数是否发出无效运算信号，这也是 bin_float 把该关系与 BinaryFlags 一并返回的原因。在扩展实数上，前三种就是通常的三分律，其中 $-0 = +0$ ，且对每个有限的 $t$ 有 $-\infty < t < +\infty$ ；无序恰在至少一个操作数为 NaN 时成立，包括两者是同一个 NaN 的情形。PartialOrder 就是把这一四值关系表示为数据类型。

设计决策

小而开放的 trait，而非数值塔

问题。 泛型代码必须能向任何表示询问若干问题，但各种表示并不共享算术定律：二进制和十进制运算在不同基数下舍入，GDA 运算贯穿一个粘滞上下文，区间运算返回的是包络而不是舍入后的点。

可选方案。 (a) 一个包含算术、序和解析的宽泛“实数” trait。(b) 一个只包含与表示无关的观测和重设精度的 trait。(c) 没有共享 trait。

选择：(b)。 Floating 恰好只有 classify、sign、precision、with_precision 和 normalized。算术取自 MoonBit 的运算符 trait 以及 Luna-Flow/arithmetic 的能力 trait（SqrtChecked、AddContextual……），每种类型只在能遵守相应定律时才实现它们。单一的宽泛 trait 会把同一套定律强加于全部四个领域；例如，区间无法实现标量的 compare，除非对相互重叠的操作数撒谎。这遵循 Luna-Flow 的原则：代码只依赖于陈述其需求的最小 trait 组合。

`Sign` 合并两个零

sign 回答的是“值位于零的哪一侧”，而不是“符号位是什么”。把 $-0$ 和 $+0$ 合并为 Zero，使 sign 成为所表示值的函数，从而在各种表示之间保持一致，也与同样忽略带符号零的 semantic 投影一致。符号位仍可通过具体的包观测到。标量实现对 NaN 返回 Zero，因为 NaN 在数轴上没有位置；关心这一点的调用方应先检查 is_nan。

对于区间 $X = [\ell, u]$ ，同一问题有三个诚实的答案，BallFloat::sign 按如下方式返回：

\operatorname{sign}(X) = \begin{cases} \texttt{Positive} & \text{if } \ell > 0 \quad(\text{every member is positive}),\\ \texttt{Negative} & \text{if } u < 0 \quad(\text{every member is negative}),\\ \texttt{Zero} & \text{if } \ell \le 0 \le u \quad(0 \in X). \end{cases}

由于 $\ell \le u$ ，对非空 $X$ 这三种情形是穷尽且互斥的：若既非 $\ell > 0$ 也非 $u < 0$ ，则 $\ell \le 0 \le u$ 。因此区间上的 Zero 意味着“包含零”，而通过 sign 定义的 is_zero 也继承了这一含义。

`PartialOrder` 是 IEEE 的四路关系

问题。 比较结果必须能够表达 NaN 操作数的情形。

可选方案。 (a) 通过 MoonBit 的 Compare 返回 Int。(b) 返回 Option[Int]。(c) 返回一个四值枚举。

选择：(c)。 设 $\preceq$ 为浮点数据上的“小于或等于”。它在整个集合上并不是一个序：

\begin{aligned} &\text{reflexivity fails:} && \mathrm{NaN} \preceq \mathrm{NaN} \text{ is false, since the pair is unordered;}\\ &\text{totality fails:} && \text{neither } 1 \preceq \mathrm{NaN} \text{ nor } \mathrm{NaN} \preceq 1;\\ &\text{antisymmetry fails on data:} && -0 \preceq +0 \text{ and } +0 \preceq -0, \text{ but } -0 \ne +0 \text{ as data.} \end{aligned}

限制在非 NaN 数据上时， $\preceq$ 是自反、传递且完全的，因此是一个全预序，它按“等于”所得的商就是扩展实数的全序。加入 NaN 后它连预序都不是，因此任何以 Int 为值的 Compare 实例都无法合规地表示它：无论为无序对选择哪个整数，基于它的排序都会把 NaN 当作可比较的。带有显式 Unordered 的枚举保留了这一信息，并迫使调用方在 match 中处理它。Option[Int] 虽能携带同样的信息，却会赋予“无答案”以“缺失”这一泛泛含义，并且失去了名称。

具体的包还额外提供了确实是完全的关系，供需要全序的任务使用：BinFloat::total_order 实现了 IEEE 的 totalOrder 谓词（第 5.10 条），而 BinFloat::compare（Compare 实例）是一个把所有 NaN 置于所有数之上的全预序。它们是与 PartialOrder 不同的关系，按调用处的需要选择。

重新导出算术类型

ArithmeticContext、ArithmeticError、RoundingMode、FpClass 以及认证相关类型归 Luna-Flow/arithmetic 所有，该库定义了 floating 所实现的 contextual 与 checked trait。def 用 pub using 重新导出它们，而不是定义外观相似的副本，因此 @def.RoundingMode 的值就是 @lf_arith.RoundingMode 的值，两个仓库之间不存在转换层。

正确性 / 不变式

`Floating` 定律

下面的定律就是该 trait 的契约。它们针对值 $x$ 、精度 $p$ 和方向 $m$ 陈述； $q = \max(1, p)$ 。本仓库的四个实现都满足这些定律，下游实现也应当满足。

\begin{aligned} &\textbf{(F1) partition} && \text{exactly one of } \texttt{is\_finite}(x),\ \texttt{is\_infinite}(x),\ \texttt{is\_nan}(x) \text{ holds;}\\ &\textbf{(F2) sign} && \texttt{classify}(x) \ne \texttt{NaN} \implies \texttt{sign}(x) \text{ is given by the side of } 0 \text{ on which } [\![x]\!] \text{ lies;}\\ &\textbf{(F3) precision} && \texttt{precision}(x) \ge 1;\\ &\textbf{(F4) re-precision} && \texttt{precision}(\texttt{with\_precision}(x, p, m)) = q;\\ &\textbf{(F5) rounding} && x \text{ a finite scalar} \implies [\![\texttt{with\_precision}(x,p,m)]\!] = \circ_{m,q}([\![x]\!]);\\ &\textbf{(F6) enclosure} && x \text{ an interval} \implies [\![x]\!] \subseteq [\![\texttt{with\_precision}(x,p,m)]\!];\\ &\textbf{(F7) normal form} && [\![\texttt{normalized}(x)]\!] = [\![x]\!],\quad \texttt{normalized}(\texttt{normalized}(x)) = \texttt{normalized}(x). \end{aligned}

对于非有限标量，with_precision 保持类别和符号，只改变存储的精度，因此 (F4) 仍然成立。区间的 (F2) 就是上文推导的三情形规则；对标量而言，当 $[\![x]\!] = 0$ 时“ $0$ 的哪一侧”为 Zero。

为什么 (F6) 对 BallFloat 成立。 对中心为 $c$ 、半径为 $r$ 的有界球，with_precision 计算 $\tilde c = \circ_{m,q}(c)$ ，把误差 $|c - \tilde c|$ 和半径向上舍入为 $\tilde e \ge |c-\tilde c|$ 和 $\tilde r \ge r$ ，以向上舍入把它们相加得到 $R \ge \tilde r + \tilde e$ ，并存储 $[\nabla(\tilde c - R), \Delta(\tilde c + R)]$ 。对任意满足 $|t - c| \le r$ 的成员 $t$ ，

|t - \tilde c| \le |t - c| + |c - \tilde c| \le r + |c - \tilde c| \le \tilde r + \tilde e \le R,

因此 $\nabla(\tilde c - R) \le \tilde c - R \le t \le \tilde c + R \le \Delta(\tilde c + R)$ 。方向 $m$ 只移动中心；对每个 $m$ 包络都成立。无界区间把下端点向下舍入、上端点向上舍入，包络关系平凡成立。

(F5) 的推论

舍入在其目标集合上是恒等映射：若 $t \in \mathbb{F}_{\beta,q}$ ，则对每个方向都有 $\circ_{m,q}(t) = t$ ，因为 $t$ 就是它自己的相邻元素。因此

[\![x]\!] \in \mathbb{F}_{\beta,q} \implies [\![\texttt{with\_precision}(x, p, m)]\!] = [\![x]\!],

特别地，提高精度从不改变值，因为当 $p \le p'$ 时 $\mathbb{F}_{\beta,p} \subseteq \mathbb{F}_{\beta,p'}$ 。

一般而言，分两步降低精度与一次降低并不相同。对定向模式则相同。取 $q \le p$ 和 $m =$ TowardZero，把 $\circ_{m,k}$ 记作 $\circ_k$ ，并令 $a = \circ_q(t)$ ，即 $\mathbb{F}_{\beta,q}$ 中与 $t$ 同号且绝对值不超过 $|t|$ 的最大元素。则

\begin{aligned} a \in \mathbb{F}_{\beta,q} \subseteq \mathbb{F}_{\beta,p},\ |a| \le |t| &\implies |a| \le |\circ_p(t)| \le |t| && \text{(definition of } \circ_p\text{)}\\ b \in \mathbb{F}_{\beta,q},\ |b| \le |\circ_p(t)| &\implies |b| \le |t| \implies |b| \le |a| && \text{(definition of } a\text{)}\\ &\implies \circ_q(\circ_p(t)) = a = \circ_q(t). \end{aligned}

用“ $\le t$ 的最大元素”进行同样的论证，可适用于 $\nabla$ 和 $\Delta$ 。对 ToNearestEven，该恒等式不成立（双重舍入）。³3 Muller 等，Handbook of Floating-Point Arithmetic，第 2 版，2018，第 3.2 节（双重舍入）；Goldberg，“What every computer scientist should know about floating-point arithmetic”，1991。取二进制下的 $t = 1.0100001_2 = 161/128$ 。当 $p = 3$ 时，相邻元素为 $1.25$ 和 $1.5$ ， $t$ 舍入为 $1.25$ ，而它恰好位于 $q = 2$ 时的相邻元素 $1$ 和 $1.5$ 的正中间；平局取偶数系数，即 $1$ 。而把 $t$ 直接舍入到两位得到 $1.5$ ，因为 $t > 1.25$ ：

///|
test "double rounding to nearest differs from one rounding" {
  let t = @bin_float.BinFloat::from_double(1.2578125)
  let nearest = @lf_arith.RoundingMode::ToNearestEven
  let twice = @def.Floating::with_precision(
    @def.Floating::with_precision(t, 3, nearest),
    2,
    nearest,
  )
  let once = @def.Floating::with_precision(t, 2, nearest)
  inspect(twice.to_string(), content="1p0")
  inspect(once.to_string(), content="3p-1")
  let toward_zero = @lf_arith.RoundingMode::TowardZero
  let twice_rz = @def.Floating::with_precision(
    @def.Floating::with_precision(t, 3, toward_zero),
    2,
    toward_zero,
  )
  let once_rz = @def.Floating::with_precision(t, 2, toward_zero)
  inspect(twice_rz.to_string() == once_rz.to_string(), content="true")
}

谓词

四个谓词都是 classify 和 sign 的投影，因此其正确性归结为 (F1) 和 (F2)。is_zero 先求值 classify，并使用短路的 &&；因此它从不对 NaN 类的值调用 sign，从而在空区间上仍是全函数，尽管 BallFloat::sign 在那里会中止。

开销

除委托的实现外，def 的每个条目都是常数时间。with_precision 和 normalized 的代价等于具体包中舍入或去除尾随零的代价：对十进制与系数长度成线性，对二进制与系数的位长成线性。

被否决的替代方案

带算术的 Real 超 trait。 它会声称舍入算术和区间算术并不满足的定律（结合律、全序），并会掩盖精确运算、舍入运算与包络运算之间的区别。
用 Compare 表示 IEEE 比较。 Int 结果无法表达无序；见上文的推导。
分别设立 NegativeZero / PositiveZero 符号。 这会使 sign 依赖于表示而非值，而且区间符号没有对应物。
在本地定义 RoundingMode 和 ArithmeticContext 的副本。 这样在与 Luna-Flow/arithmetic 的每个边界上都需要转换。

边界

这里不实现任何算术、解析、格式化或比较；def 只为结果命名（Sign、PartialOrder）并陈述契约。
Floating 并不蕴含域、全序、IEEE 格式、精确算术或任何错误行为。泛型代码必须显式要求它所用到的额外能力 trait。
with_precision 既不遵守指数界，也不报告标志；上下文和标志属于具体包的 *_ctx API 以及 Luna-Flow/arithmetic 的 contextual trait。
Sign 不暴露零或 NaN 的符号位。
这些定律由各实现记录并测试；对于下游实现，trait 本身并不强制执行它们。

IEEE 754-2019，第 4.3 条（舍入方向属性）。AwayFromZero 不是 IEEE 二进制属性；它对应 GDA 的舍入 Up（Cowlishaw，General Decimal Arithmetic Specification）。 ↩
IEEE 754-2019，第 5.11 条（比较谓词的细节）及表 5.1。静默谓词与信号谓词的区别仅在于静默 NaN 操作数是否发出无效运算信号，这也是 bin_float 把该关系与 BinaryFlags 一并返回的原因。 ↩
Muller 等，Handbook of Floating-Point Arithmetic，第 2 版，2018，第 3.2 节（双重舍入）；Goldberg，“What every computer scientist should know about floating-point arithmetic”，1991。 ↩

def 设计