`semantic` 设计

设计目标

semantic 以与表示无关的方式回答一个问题：这个数据表示哪个数？ 二进制浮点数、IEEE 十进制数和区间端点被映射为精确有理数、带符号无穷、NaN 和闭区间，从而使由不同包、以不同精度、在不同基数下计算出的值可以精确比较。出于同样的目的，checked 错误被映射到一套小而通用的词汇。本包是测试、诊断和协议的边界；它不执行任何算术。API 页面列出了各项条目，教程演示了它们的用法。

数学背景

浮点数是有理数

符号位为 $s$ 、整数系数 $c \ge 0$ 、指数为 $e$ 的有限二进制浮点数表示 $(-1)^{s} c\, 2^{e}$ ，有限十进制数表示 $(-1)^{s} c\, 10^{q}$ 。记 $m = (-1)^{s} c$ ，两者都具有 $m\, r^{k}$ 的形式，其中 $m$ 为整数，基数 $r \ge 2$ ， $k$ 为整数，这是一个有理数：

m\, r^{k} = \begin{cases} \dfrac{m\, r^{k}}{1}, & k \ge 0,\\[2ex] \dfrac{m}{r^{-k}}, & k < 0. \end{cases}

因此，有限二进制值恰好是二进有理数 $\mathbb{Z}[1/2] = \{\, a/2^{j} : a \in \mathbb{Z}, j \in \mathbb{N} \,\}$ ，有限十进制值恰好是 $\mathbb{Z}[1/10] = \{\, a/10^{j} \,\}$ ，两者都是 $\mathbb{Q}$ 的子环。这正是 ExactRational::from_scaled_integer 计算的映射，其中 $r^{|k|}$ 用 BigInt 精确求值。

约分形式是规范的

每个有理数 $x$ 都恰有一种表示 $n/d$ ，满足

d > 0, \qquad \gcd(|n|, d) = 1 \qquad (\text{and } 0 = 0/1).

存在性。 对任意 $d' \ne 0$ 的 $n'/d'$ ，将分子和分母同乘 $\operatorname{sgn}(d')$ ，再同除以 $g = \gcd(|n'|, |d'|)$ 。唯一性。 设 $n/d = n'/d'$ ，两对都已约分且 $d, d' > 0$ 。则

\begin{aligned} n d' &= n' d &&\text{(cross-multiplying)}\\ d \mid n d',\ \gcd(d, n) = 1 &\implies d \mid d' &&\text{(Euclid's lemma)}\\ d' \mid n' d,\ \gcd(d', n') = 1 &\implies d' \mid d\\ d, d' > 0 &\implies d = d' \implies n = n'. \end{aligned}

ExactRational::new 恰好建立这一形式（符号移到分子，用欧几里得算法求 gcd，零规范化为 $0/1$ ），并且字段是私有的，因此每个 ExactRational 都是约分的。于是，在两个 BigInt 字段上派生的结构相等就是有理数的相等： $n/d = n'/d' \iff (n, d) = (n', d')$ 。

比较不同基数的值

两个投影值的相等性由规范形式判定。本包不提供序比较，但该表示使之成为两次乘法的检验：对于约分的 $a/b$ 和 $c/d$ ， $b, d > 0$ ，

\frac{a}{b} < \frac{c}{d} \iff \frac{a}{b} - \frac{c}{d} < 0 \iff \frac{ad - cb}{bd} < 0 \iff ad - cb < 0 \quad (\text{since } bd > 0),

这正是教程基于 numerator() 和 denominator() 所实现的。

规范分母还解释了哪些十进制数具有二进制表示。约分后的二进制值的分母为 $2^{j}$ ；约分后的十进制值 $a/10^{j}$ 约分后的分母为 $2^{u} 5^{v}$ 。由约分形式的唯一性，一个十进制值等于某个（精度足够的）有限二进制浮点数，当且仅当其约分后的分母不含因子 $5$ 。十分之一约分为 $1/(2 \cdot 5)$ ，因此没有二进制浮点数等于它，binary64 0.1 的投影是 $3602879701896397/2^{55}$ ，是另一个数。¹1 Goldberg，“What every computer scientist should know about floating-point arithmetic”，ACM Computing Surveys 23(1)，1991，关于进制转换的一节；Knuth，TAOCP 第 2 卷，第 4.4 节。

///|
test "a decimal has a binary equal iff its denominator has no factor 5" {
  let denominator = fn(s : @semantic.SemanticScalar) {
    match s {
      Rational(q) => q.denominator().to_string()
      _ => "none"
    }
  }
  let d = fn(text : String) {
    @semantic.SemanticScalar::from_decimal(@decimal.Decimal::from_string(text).unwrap())
  }
  let b = fn(x : Double) {
    @semantic.SemanticScalar::from_bin_float(@bin_float.BinFloat::from_double(x))
  }
  inspect(denominator(d("0.375")), content="8")
  inspect(d("0.375") == b(0.375), content="true")
  inspect(denominator(d("0.1")), content="10")
  inspect(denominator(b(0.1)), content="36028797018963968")
}

区间是扩展有理数对

非空 BallFloat 表示 $X = \{\, t \in \mathbb{R} : \ell \le t \le u \,\}$ ，其中端点 $\ell \le u$ 属于 $\mathbb{Z}[1/2] \cup \{-\infty, +\infty\}$ ，无穷端点表示该侧无界，与 IEEE 1788-2015 基于集合的区间相同。²2 IEEE 1788-2015，Standard for Interval Arithmetic，第 7 条（基于集合的 flavor）：区间是 $\mathbb{R}$ 的闭连通子集，可能无界或为空。 SemanticInterval::from_ball_float 用 from_bin_float 分别投影 $\ell$ 和 $u$ ，因此这一对端点精确确定 $X$ 。空区间由 ball_float 以 $\ell = +\infty$ 和 $u = -\infty$ 存储，投影保留这对反转的端点；在扩展序中，lower > upper 恰好对空集成立。于是，对有理数 $t$ 的成员检验 $t \in X$ 就是两次上文推导的那种比较。

设计决策

精确有理数，而非公共浮点格式

问题。 比较二进制值与十进制值需要一个公共域。

可选方案。 (a) 把两者都转换为 Double 或宽二进制浮点数。(b) 把两者都转换为十进制字符串。(c) 把两者都投影到 $\mathbb{Q}$ 。

选择：(c)。 转换为浮点数会舍入，因此两个不同的值在转换后可能比较为相等（binary64 0.1 和十进制 0.1 都舍入为同一个 Double）。字符串比较依赖于格式化和同值类（cohort）。 $\mathbb{Z}[1/2]$ 和 $\mathbb{Z}[1/10]$ 都能无损嵌入 $\mathbb{Q}$ ，而约分形式使相等性变成字段比较。代价是大小： $r^{|k|}$ 约有 $|k| \log_2 r$ 位。

投影丢弃了什么

投影只保留所表示的值。它丢弃精度、十进制量子（同值类）、零的符号、NaN 载荷、符号与信号状态、区间装饰，以及所有标志和上下文状态。这些都是表示和计算的属性，由具体的包对外暴露。保留其中任何一项，都会使来自不同包的两个相等的数比较为不等，从而违背本包的初衷。

NaN 是单一的值，采用结构相等

SemanticScalar 派生了 Eq，因此 NaN == NaN。该类型是一个模型，其中“此次计算没有产生数”是诸多结果之一，而测试需要断言两个包都产生了它。IEEE 比较中 NaN 与自身无序，这一语义保留在具体的包和 PartialOrder 中。

独立的错误词汇

ArithmeticError 携带一条消息，对于认证失败还携带一个详情记录，其中包含精度和细化次数，而对于同一个数学上的失败，这些数值在不同包之间各不相同。SemanticError 只保留种类，因此 semantic_scalar_result 使结果可以跨包比较。该映射按固定顺序检验各个种类谓词，最后回退到 UnsupportedOperation；由于每个 ArithmeticErrorKind 构造器都有自己的谓词，每个种类都映射到同名的 SemanticError。

投影即普通函数

semantic_scalar_result 把投影作为参数接收，而不是基于 trait 进行分派。记 $\mathrm{Res}(T) = T + E$ 和 $\mathrm{Sem}(S) = S + E'$ ，该函数为

\texttt{semantic\_scalar\_result}(\cdot, f) = f + \texttt{from\_arithmetic} : T + E \longrightarrow S + E',

即两个映射的余积：在左侧被加项上应用 $f$ ，在右侧被加项上应用错误映射。它满足函子律 $\texttt{semantic\_scalar\_result}(r.\texttt{map}(g), f) = \texttt{semantic\_scalar\_result}(r, f \circ g)$ ，这使调用方可以在每条流水线上复用同一个投影。

正确性 / 不变式

约分形式。 每个 ExactRational 都满足 $d > 0$ 、 $\gcd(|n|, d) = 1$ 以及 $n = 0 \Rightarrow d = 1$ ；new 在 $d = 0$ 时中止。
精确性。 对有限的 $x$ ， $\texttt{from\_bin\_float}(x) = \texttt{Rational}([\![x]\!])$ 且 $\texttt{from\_decimal}(x) = \texttt{Rational}([\![x]\!])$ ；不做任何舍入。
相等性的可靠性与完备性。 对两种受支持标量类型中任意一种的有限 $x$ 、 $y$ ，二者的投影相等当且仅当 $[\![x]\!] = [\![y]\!]$ ；这就是约分形式的唯一性。
类别保持。 无穷投影为同号的 Infinity，每个 NaN 都投影为 NaN，有限值投影为 Rational。
区间。 from_ball_float 是两个端点投影组成的对；整条实轴得到 $(-\infty, +\infty)$ ，空区间得到 $(+\infty, -\infty)$ 。
代价。 from_scaled_integer 执行一次精确乘幂，对负指数还要执行一次 gcd；两者都是操作数位长 $O(|k| \log r + \log |m|)$ 的多项式。

被否决的替代方案

在 ExactRational 上实现算术。 精确有理数算术属于另一个库；在这里实现它会诱使人把投影当作数值类型使用，而它并不是。
为 SemanticScalar 提供 Ord 风格的实例。 NaN 和反转的空区间在全序中没有位置；调用方应显式地对有理数排序。
保留带符号零。 这会使 -0.0 和十进制 0 不相等，尽管它们表示同一个数。
为 @decimal_gda.Decimal 提供投影。 当前分支未提供；GDA 值通过其字符串形式或通过 @decimal.Decimal 进入本包。

边界

不提供算术、舍入、解析、格式化、交换编码或区间收紧。
语义值之间没有序，只有相等。
表示细节（精度、量子、带符号零、NaN 载荷与信号性、装饰、标志、上下文）被刻意舍弃。
只有 BinFloat、@decimal.Decimal 和 BallFloat 有投影。
指数极大的值的投影是精确的，因此也很大；本包不防范这一代价。

Goldberg，“What every computer scientist should know about floating-point arithmetic”，ACM Computing Surveys 23(1)，1991，关于进制转换的一节；Knuth，TAOCP 第 2 卷，第 4.4 节。 ↩
IEEE 1788-2015，Standard for Interval Arithmetic，第 7 条（基于集合的 flavor）：区间是 $\mathbb{R}$ 的闭连通子集，可能无界或为空。 ↩

semantic 设计