Luna Flow
简体中文

core 设计

设计目标

core 规定了 luna-poly 中所有表示共享的含义：什么是单项式，单项式按什么顺序排列，什么是具名变量，以及通用算法在不了解存储方式的情况下可以对多项式做哪些观察。稠密、项数组、稀疏和绑定上下文的多项式，无论不可变还是可变，都建立在这些定义之上，因此它们在相等、排序和命名上的一致性来自构造本身，而非约定。

数学背景

多项式环

设 RR 为交换环（若只考虑加法运算，则为交换幺半群）。变量 x0,…,xn−1x_0, \dots, x_{n-1} 上的多项式是一个有限支撑函数 f:Nn→Rf : \mathbb{N}^n \to R，记作

f=∑α∈Nnfα xα,xα=x0α0x1α1⋯xn−1αn−1.f = \sum_{\alpha \in \mathbb{N}^n} f_\alpha \, x^\alpha, \qquad x^\alpha = x_0^{\alpha_0} x_1^{\alpha_1} \cdots x_{n-1}^{\alpha_{n-1}} .

xαx^\alpha 称为单项式，α\alpha 称为指数向量。多项式在逐点加法和如下卷积乘积下构成环 R[x0,…,xn−1]R[x_0, \dots, x_{n-1}]

(fg)γ=∑α+β=γfα gβ,(fg)_\gamma = \sum_{\alpha + \beta = \gamma} f_\alpha \, g_\beta ,

它是 xαxβ=xα+βx^\alpha x^\beta = x^{\alpha + \beta} 的双线性扩张。换言之，R[x0,…,xn−1]R[x_0, \dots, x_{n-1}] 是幺半群环 R[Nn]R[\mathbb{N}^n]，关于单项式的一切都是关于加法幺半群 Nn\mathbb{N}^n 的命题。

不固定元数的指数向量

ExponentVector 不携带 nn。它表示下列集合中的元素

N(∞)={ α:N→N∣αi=0 for all but finitely many i },\mathbb{N}^{(\infty)} = \{\, \alpha : \mathbb{N} \to \mathbb{N} \mid \alpha_i = 0 \text{ for all but finitely many } i \,\},

即可数无穷多个变量上的自由交换幺半群。补零映射 ιn(α0,…,αn−1)=(α0,…,αn−1,0,0,… )\iota_n(\alpha_0, \dots, \alpha_{n-1}) = (\alpha_0, \dots, \alpha_{n-1}, 0, 0, \dots) 是单射的幺半群同态 Nn→N(∞)\mathbb{N}^n \to \mathbb{N}^{(\infty)}，因此

R[x0]⊂R[x0,x1]⊂⋯⊂R[x0,x1,… ]=R[N(∞)]R[x_0] \subset R[x_0, x_1] \subset \cdots \subset R[x_0, x_1, \dots] = R[\mathbb{N}^{(\infty)}]

用两个变量写出的多项式，与用三个变量（最后一个未使用）写出的多项式，字面上就是同一个元素。

每个 α≠0\alpha \neq 0 都有最后一个非零位置 ℓ(α)=max⁡{i∣αi≠0}\ell(\alpha) = \max\{ i \mid \alpha_i \neq 0 \}，且有限字 (α0,…,αℓ(α))(\alpha_0, \dots, \alpha_{\ell(\alpha)}) 唯一确定 α\alpha。这个字就是 ExponentVector 存储的规范形式；单位元 00 存储为空字。由此直接得到两个推论：

  • 规范形式唯一，因此存储字的结构相等就是 N(∞)\mathbb{N}^{(\infty)} 中的相等，这就是 [1, 0] == [1] 成立的原因；
  • 多项式的元数，即其各项存储长度的最大值，是使 f∈R[x0,…,xn−1]f \in R[x_0, \dots, x_{n-1}] 成立的最小 nn。

总次数 ∣α∣=∑iαi|\alpha| = \sum_i \alpha_i 是幺半群同态 N(∞)→N\mathbb{N}^{(\infty)} \to \mathbb{N}，∣α+β∣=∣α∣+∣β∣|\alpha + \beta| = |\alpha| + |\beta|。它在构造向量时计算一次，并与指数一起存储。

设计决策

所有表示共用一种单项式类型

问题。 稠密一元存储只需要整数幂，但项数组、稀疏和绑定上下文的多项式都需要指数向量、指数向量上的序以及哈希。

方案。 每种表示可以各自定义键类型；或者由一个共享类型放在 core 中。

选择。 ExponentVector 位于 core，并由两个门面包重新导出，因此 immut 与 mutable 多项式无需转换即可交换项，并在相等和序上保持一致。该向量是不可变的（它包装了一个持久化的 @immut/vector.Vector），因此也可以安全地用作可变容器中的键。

单项式序

问题。 项数组存储必须保持各项有序，稀疏存储中的有序映射需要键的序。这个序还应当是单项式序，这样首项才具有代数意义。

选择。 ExponentVector::compare 实现了

α≺β  ⟺  ∣α∣<∣β∣   or   (∣α∣=∣β∣ and αk<βk for k=max⁡{i∣αi≠βi}).\alpha \prec \beta \iff |\alpha| < |\beta| \;\text{ or }\; \bigl( |\alpha| = |\beta| \text{ and } \alpha_k < \beta_k \text{ for } k = \max\{ i \mid \alpha_i \neq \beta_i \} \bigr).

总次数相同时，由不同的下标最大的变量决定。这是变量优先级为 x0≺x1≺x2≺⋯x_0 \prec x_1 \prec x_2 \prec \cdots 的分次字典序；它不是分次反字典序。11 Cox、Little 和 O’Shea 在 Ideals, Varieties, and Algorithms §2.2 中，对 x1>x2>⋯>xnx_1 > x_2 > \cdots > x_n 用 α−β\alpha - \beta 的最左非零分量定义 grlex。从右往左读向量，就是把变量倒序排列后的同一个序。 例如在三个变量、次数 22 的情形下，(1,0,1)−(0,2,0)=(1,−2,1)(1,0,1) - (0,2,0) = (1,-2,1) 的最后一个非零分量为正，因此 x0x2≻x12x_0 x_2 \succ x_1^2；而 x0>x1>x2x_0 > x_1 > x_2 下的分次反字典序则把 x12x_1^2 排在前面。

该序具备单项式序所需的四条性质，下面在 N(∞)\mathbb{N}^{(\infty)} 上推导。

它是全序。 若 α≠β\alpha \neq \beta 且 ∣α∣=∣β∣|\alpha| = |\beta|，则集合 {i∣αi≠βi}\{ i \mid \alpha_i \neq \beta_i \} 非空，并且由于两个向量都是有限支撑的，该集合有限，因此其最大值 kk 存在，由 αk≠βk\alpha_k \neq \beta_k 决定大小。

它与乘法相容。 对任意 γ\gamma，

∣α+γ∣−∣β+γ∣=∣α∣−∣β∣,(α+γ)i−(β+γ)i=αi−βifor every i,\begin{aligned} |\alpha + \gamma| - |\beta + \gamma| &= |\alpha| - |\beta|, \\ (\alpha + \gamma)_i - (\beta + \gamma)_i &= \alpha_i - \beta_i \quad \text{for every } i, \end{aligned}

因此次数比较、不同位置的集合、其最大值 kk 以及 kk 处的符号都不变：α≺β⇒α+γ≺β+γ\alpha \prec \beta \Rightarrow \alpha + \gamma \prec \beta + \gamma。

单位元最小。 ∣0∣=0≤∣α∣|0| = 0 \le |\alpha|，等号仅在 α=0\alpha = 0 时成立。

它是良序， 即使变量个数无界也是如此。假设存在无穷链 α(1)≻α(2)≻⋯\alpha^{(1)} \succ \alpha^{(2)} \succ \cdots。各次数构成单调不增的自然数序列，因此从某个 NN 起都等于常数 dd。令 m=ℓ(α(N))m = \ell(\alpha^{(N)})。任何其后满足 ∣β∣=d|\beta| = d 且 β≺α(N)\beta \prec \alpha^{(N)} 的 β\beta，对所有 i>mi > m 都有 βi=0\beta_i = 0：否则令 j>mj > m 为满足 βj>0\beta_j > 0 的最大下标；两个向量在 jj 之上一致（都为零），且 βj>0=αj(N)\beta_j > 0 = \alpha^{(N)}_j，于是 k=jk = j 且 β≻α(N)\beta \succ \alpha^{(N)}，矛盾。因此链的尾部落在 {β∈Nm+1∣∣β∣=d}\{ \beta \in \mathbb{N}^{m+1} \mid |\beta| = d \} 中，这是一个有 (d+mm)\binom{d+m}{m} 个元素的集合，而有限集中的严格下降链是有限的。

为什么选这个序。 按总次数分次，使项数组多项式的前几项就是其最高次部分，这正是读者最先想看到的；而在最后一个变量处打破平局，只需对两个短向量做一次反向扫描。各表示所依赖的是与乘法的相容性：TermPolynomial::scale 把每一项乘以同一个单项式，并且无需重新排序即可保留数组，因为 α↦α+γ\alpha \mapsto \alpha + \gamma 是严格递增的。

相等、序与哈希相互一致

compare 恰好在次数相等且没有位置不同时返回 00，也就是恰好在规范字相等时，这就是 equal。hash 组合了次数和存储的指数，两者都是规范字的函数，因此相等的向量哈希值相同。所以有序映射（按 compare 排序）和哈希映射（以 hash 和 equal 为键）识别的是相同的单项式。

名字存于上下文，位置存于向量

问题。 用户以具名变量（xx、yy、tt）思考；算术需要的是位置。

方案。 在每个单项式中存储名字；或者让单项式保持按位置寻址，把名字放在单独的表中。

选择。 单项式保持按位置寻址。VariableContext 是互不相同的名字组成的列表 Γ=(s0,…,sk−1)\Gamma = (s_0, \dots, s_{k-1})，变量 sis_i 是二元组 (si,i)(s_i, i)。由于名字互不相同，映射 i↦sii \mapsto s_i 与 si↦is_i \mapsto i 是 {0,…,k−1}\{0, \dots, k-1\} 与 Γ\Gamma 中名字之间互逆的双射，因此上下文可以在具名项与指数向量之间双向转换。

下标是从上下文开头起算的位置，类似 de Bruijn 层级（level）：用新名字扩展 Γ\Gamma 时将其追加到末尾，从不对已有变量重新编号。从 Γ\Gamma 得到的变量在 Γ\Gamma 的每个扩展中都保持其含义。

上下文按结构比较。由相同名字分别构造的两个上下文相等，它们的变量可以互换。这使上下文保持为普通的值，无需追踪身份或分配。

通往 type_theory 名字的桥梁，而非对其语法的依赖

Luna-Flow/type_theory 掌管名字、绑定与代换的共享词汇。Variable::to_type_theory_name 把变量映射为其名字并丢弃下标；VariableContext::variable_by_type_theory_name 在上下文中把名字解析回变量。记前一个映射为 N(v)N(v)，后一个为 LΓL_\Gamma。对 Γ\Gamma 中的每个变量 vv，

LΓ(N(v))=the variable of Γ named v.name(definition of LΓ)=Γ[v.index](names are unique, and v∈Γ)=v,(contains means Γ[v.index]=v)\begin{aligned} L_\Gamma(N(v)) &= \text{the variable of } \Gamma \text{ named } v.\text{name} && \text{(definition of } L_\Gamma) \\ &= \Gamma[v.\text{index}] && \text{(names are unique, and } v \in \Gamma) \\ &= v , && \text{(}\texttt{contains}\text{ means } \Gamma[v.\text{index}] = v) \end{aligned}

反之，只要 LΓ(t)L_\Gamma(t) 有定义，就有 N(LΓ(t))=tN(L_\Gamma(t)) = t。因此在同一个上下文内，名字与变量可以互换，这使得基于名字的代换 API 可以先解析名字，再原样复用基于变量的 API。

多项式没有绑定子：上下文中的每个变量在其上的每个多项式中都是自由的。避免捕获的代换是 type_theory 中代换的难点，在这里却是平凡的，因为不存在可以捕获替换内容的约束变量。所以 luna-poly 只从 type_theory 中取用 Name，并保留自己的项结构和规范形式。

能力是观察，而非代数

问题。 通用代码需要在不依赖存储类型的情况下询问“有多少个变量、多少项、是否为零？”，而代数结构在 luna-generic 中已有自己的词汇。

选择。 每个 Has* trait 暴露一种观察，组合 trait UnivariatePolynomial、MultivariatePolynomial、ContextualPolynomial 和 MutablePolynomial 按族将它们归组。环运算仍使用具体类型所实现的标准 Add、Mul、Neg、Sub、Zero 和 One trait。这些 trait 是 pub(open) 的，因此下游包可以为自己的表示实现它们。

PolynomialShape 使这些观察可以比较。is_compatible_with 是等价关系：它逐情形地满足自反性和对称性，并且具有传递性，因为“构造子相同”是传递的，而对 Contextual 而言上下文相等也是传递的。元数和项数被有意忽略：根据上面的嵌入，两个多元多项式总位于一个公共环 R[x0,…,xmax⁡(n,n′)−1]R[x_0, \dots, x_{\max(n, n') - 1}] 中，两个一元多项式总位于 R[x]R[x] 中。只有绑定上下文的多项式在上下文不同时才可能不在同一个环中。

用操作记录代替多参数 trait

问题。 针对“系数为 AA 的多项式类型 PP”的通用算法，需要一个带两个类型参数的 trait，或者一个关联的系数类型。

约束。 MoonBit 的 trait 只有 Self；没有多参数 trait，也没有关联类型。

选择。 UnivariateOps[P, A]、MultivariateOps[P, A] 和 ContextOps[P, A] 是函数记录，由各具体类型的 ops() 构建并显式传递（字典传递）。记录类型同时提及两个参数，因此像 fn[P, A] f(ops : MultivariateOps[P, A], ...) 这样的函数可以把多项式与系数联系起来。字段是私有的，只能通过访问器方法获取，因此记录布局可以扩展而不破坏调用者。

带检查的变体返回 Option

每个部分操作都有一个中止形式和一个 *_checked 形式，后者在违反契约（负下标、重复名字、未知变量）时返回 None。Option 不携带原因，因此需要原因的调用者应自行检查前置条件。这一点早于 Luna Flow 中 linear-algebra、arithmetic 和 type_theory 所采用的、带结构化错误值的 Result 约定；各页面如实记录当前的 Option 契约。

正确性 / 不变量

  • 规范指数向量。 存储字从不以 00 结尾；degree 等于存储指数之和。每个构造函数以及 with_exponent 都会重新去除末尾零。
  • 序。 compare 是 N(∞)\mathbb{N}^{(\infty)} 上的全单项式序和良序（上文已推导），并与 equal 和 hash 一致。
  • 上下文。 名字两两不同，位置 ii 处的变量下标为 ii。extend_checked 和 from_names_checked 保证这一点；其他任何途径都不会构造上下文。
  • 名字往返。 对 v∈Γv \in \Gamma 有 LΓ(N(v))=vL_\Gamma(N(v)) = v，且在有定义时 N(LΓ(t))=tN(L_\Gamma(t)) = t。
  • 形状相容性是等价关系。
  • 复杂度。 ExponentVector 的构造、mul 和 compare 对存储长度为 O(ℓ)O(\ell)；degree 为 O(1)O(1)。按名字查找上下文是线性扫描，需要 O(k)O(k) 次字符串比较；get 和 contains 除比较一个变量外为 O(1)O(1)。

被否决的替代方案

  • 每个多项式固定元数。 在每个向量中携带 nn 会使 [1, 0] 和 [1] 成为同一单项式的不同键，并迫使在 R[x0]R[x_0] 与 R[x0,x1]R[x_0, x_1] 之间显式提升。去除末尾零则免费得到了包含关系。
  • 字典序。 纯字典序也是单项式序，但它不是分次的：项数组多项式会把 x1x_1 排在 x0100x_0^{100} 之前，而且该序不会按次数对项分组。
  • 在单项式中存储名字。 存储名字会使每次单项式乘积都要比较字符串，并把算术绑定到某一种命名方案上；按位置的向量加上下文使算术保持纯数值。
  • 一个 Polynomial 万能 trait。 一个同时承担构造、算术和求值的 trait 无法提及系数类型，并且会掩盖函数真正需要哪些操作。小型观察 trait 加上显式操作记录能准确表达需求。
  • 实现 type_theory 的绑定语法。 多项式不绑定任何东西，因此绑定机制只会增加义务而不增加含义。

边界

  • 不涉及存储、算术或求值：这些属于各表示包。
  • 指数类型为 UInt。单项式乘积和总次数会静默地按模 2322^{32} 回绕；超出该范围后，序不再与乘法相容。
  • 只提供一种单项式序。没有选择 lex、grevlex 或权序的 API，也没有 Gröbner 基相关机制。
  • 上下文按结构比较，而非按身份；名字相同且顺序相同的两个上下文就是同一个上下文。
  • 能力 trait 只表达观察。它们不携带任何代数律，操作记录也不检查其所含函数是否满足任何代数律。
  • type_theory 只提供名字；luna-poly 不实现其绑定或重写接口。

Footnotes

  1. Cox、Little 和 O’Shea 在 Ideals, Varieties, and Algorithms §2.2 中，对 x1>x2>⋯>xnx_1 > x_2 > \cdots > x_n 用 α−β\alpha - \beta 的最左非零分量定义 grlex。从右往左读向量，就是把变量倒序排列后的同一个序。 ↩