Luna Flow
简体中文

immut/context 设计

设计目标

ContextPolynomial[A] 让用户以具名变量书写多项式，并通过求值、部分求值和代换对其进行变换，而算术仍是按位置进行的，并复用项表示和稀疏表示。它也是 luna-poly 与 Luna-Flow/type_theory 的交汇处：代换可以以 type_theory 名字为键，但规范形式、存储和系数算术仍归本包所有。

数学背景

上下文上的多项式

VariableContext Γ=(s0,…,sk−1)\Gamma = (s_0, \dots, s_{k-1}) 为变量 x0,…,xk−1x_0, \dots, x_{k-1} 命名。上下文多项式是一个二元组 (Γ,f)(\Gamma, f)，其中

f∈R[Γ]:=R[x0,…,xk−1].f \in R[\Gamma] := R[x_0, \dots, x_{k-1}] .

诸如 [(x, 1), (y, 2), (x, 1)] 的具名项是名字上自由交换幺半群中的一个字；上下文通过把每个变量的指数加到其下标处，将它映射为指数向量。该映射是幺半群同态（字的连接对应指数向量相加），因此同一变量的重复因子合并为 x⋅x=x2x \cdot x = x^2，置换因子得到同一个单项式。

代换即泛性质

设 RR 是交换的。对任意选取的多项式 q0,…,qk−1∈R[Γ]q_0, \dots, q_{k-1} \in R[\Gamma]，恰好存在一个固定 RR 且把 xi↦qix_i \mapsto q_i 的环同态 φ:R[Γ]→R[Γ]\varphi : R[\Gamma] \to R[\Gamma]，即

φ(∑αcαxα)=∑αcα∏iqiαi.\varphi\Bigl(\sum_\alpha c_\alpha x^\alpha\Bigr) = \sum_\alpha c_\alpha \prod_{i} q_i^{\alpha_i} .

它是同态。 可加性由构造即成立。在单项式上，

φ(xαxβ)=φ(xα+β)=∏iqiαi+βi=∏iqiαi∏iqiβi(R[Γ] is commutative)=φ(xα) φ(xβ),\begin{aligned} \varphi(x^\alpha x^\beta) = \varphi(x^{\alpha+\beta}) &= \prod_i q_i^{\alpha_i + \beta_i} \\ &= \prod_i q_i^{\alpha_i} \prod_i q_i^{\beta_i} && (R[\Gamma] \text{ is commutative}) \\ &= \varphi(x^\alpha)\,\varphi(x^\beta), \end{aligned}

并且 φ(fg)=φ(f)φ(g)\varphi(fg) = \varphi(f)\varphi(g) 两边关于 (f,g)(f, g) 都是双线性的，因此该等式从单项式推广到所有多项式。

它是唯一的。 固定 RR 的同态在 xα=∏ixiαix^\alpha = \prod_i x_i^{\alpha_i} 上由乘法性确定，在和上由可加性确定，因此它在 x0,…,xk−1x_0, \dots, x_{k-1} 上的值决定了它。

代换 σ\sigma 为变量的子集 S⊆ΓS \subseteq \Gamma 指定替换项。它确定像

qi={σ(xi)xi∈S,xixi∉S,q_i = \begin{cases} \sigma(x_i) & x_i \in S, \\ x_i & x_i \notin S, \end{cases}

其中标量 a∈Ra \in R 视为常数多项式 aa，从而确定同态 φσ\varphi_\sigma。substitute(σ) 完全按照公式逐项计算 φσ(f)\varphi_\sigma(f)：每个因子 xiαix_i^{\alpha_i} 变为 xiαix_i^{\alpha_i}（未替换）、常数 aαia^{\alpha_i}（标量）或 qiαiq_i^{\alpha_i}（多项式）。

设计决策

同时、一遍式代换

问题。 给定 σ={x↦y,  y↦2}\sigma = \{x \mapsto y,\; y \mapsto 2\}，x+yx + y 应该变为 y+2y + 2 还是 44？

选择。 同时代换：每个 qiq_i 按给定原样取自 σ\sigma，替换多项式本身不再被代入。这就是上面的同态 φσ\varphi_\sigma，因此

φσ(x+y)=qx+qy=y+2.\varphi_\sigma(x + y) = q_x + q_y = y + 2 .

顺序的解读是两个同态的复合，而复合法则

φτ∘φσ=φτ⋅σ,(τ⋅σ)(xi)=φτ(qiσ),\varphi_\tau \circ \varphi_\sigma = \varphi_{\tau \cdot \sigma}, \qquad (\tau \cdot \sigma)(x_i) = \varphi_\tau\bigl(q^\sigma_i\bigr),

之所以成立，是因为两边都是固定 RR 且在每个 xix_i 上取值一致的同态。要顺序代换，调用 substitute 两次：φy↦2(φx↦y(x+y))=φy↦2(2y)=4\varphi_{y \mapsto 2}(\varphi_{x \mapsto y}(x + y)) = \varphi_{y \mapsto 2}(2y) = 4。同时代换之所以作为基本操作，是因为它与顺序无关：置换 σ\sigma 的条目不会改变结果。

重复条目是错误，而不是覆盖

把同一变量映射两次的列表并不定义一个函数 σ\sigma。substitute_checked 不会选取第一个或最后一个条目，而是返回 None（substitute 则中止）。同样的规则在名字解析之后也适用，因此文本相同的两个不同 Name 值，或同一名字出现两次，都会被拒绝。

部分求值保留上下文

问题。 在 p∈R[x,y]p \in R[x, y] 中赋值 x=3x = 3 之后，结果不再依赖于 xx。它可以属于 R[y]R[y]，也可以留在 R[x,y]R[x, y] 中。

选择。 eval_partial 是仅以标量为像的代换，因此其结果属于具有相同上下文的 R[Γ]R[\Gamma]。被赋值的变量只是次数为 00。保留 Γ\Gamma 意味着结果可以与 Γ\Gamma 上的其他多项式相加、相乘以及相互代入，而无需任何上下文改造，并且使部分求值能与完全求值复合。记 aa 为 SS 上的部分赋值，bb 为其余变量的赋值。那么

evb∘φa=eva∪b,\mathrm{ev}_b \circ \varphi_a = \mathrm{ev}_{a \cup b},

因为两边都是固定 RR 的同态 R[Γ]→RR[\Gamma] \to R，并且在生成元上，对 xi∈Sx_i \in S 有 evb(φa(xi))=evb(ai)=ai\mathrm{ev}_b(\varphi_a(x_i)) = \mathrm{ev}_b(a_i) = a_i，否则有 evb(φa(xi))=evb(xi)=bi\mathrm{ev}_b(\varphi_a(x_i)) = \mathrm{ev}_b(x_i) = b_i。bb 给已赋值变量的任何值都无关紧要，这就是示例用 x = 0 对部分结果求值的原因。

来自 type_theory 的名字先解析为变量

substitute_names 和 eval_partial_named 用 VariableContext::variable_by_type_theory_name 把每个 Name 映射到变量，然后调用基于变量的形式。名字往返保证在同一上下文内这是无损的：解析 v.to_type_theory_name() 会得回 v。未知名字会使整个调用失败，因此拼写错误绝不会悄悄地让某个变量未被替换。由于多项式没有绑定子，不会发生变量捕获。

什么使调用无效

每个带检查的操作恰好在以下情形返回 None：

操作拒绝条件
from_named_terms_*_checked, variable_checked变量不包含在上下文中
eval_named_checked变量在上下文之外；下标小于 arity() 的变量未被赋值或被赋值两次
substitute_checked, eval_partial_checked变量在上下文之外或被列出两次；替换多项式的上下文不同
*_names_checked此外，名字不在上下文中
add_checked, mul_checked上下文不同

Option 结果仅记录调用失败这一事实。会中止的形式检查相同的条件。

存储在构造时选定，结果与存储无关

多项式以项数组或稀疏映射的形式保存在一个私有枚举之后，由 from_named_terms_as_terms / _as_sparse 选定，或通过绑定已有的 TermPolynomial / SparsePolynomial 选定。两种存储满足相同的规范形式不变量，因此每个可观察结果（作为集合的项、求值、代换）都相同；只有代价和 to_terms() 的顺序不同。二元运算在两个操作数存储一致时保持该存储，混合操作数时使用稀疏存储，并转换以项存储的一方。代换以及构造器 constant 和 variable 产生稀疏存储。

上下文必须相等，而不是合并

二元运算要求上下文相等。自动合并 Γ\Gamma 和 Γ′\Gamma' 需要把两者单射到一个并上下文中，并对每个指数向量重新编号，而当同一名字出现在不同位置时，并并不唯一。要求相等使每个运算都是同一个环 R[Γ]R[\Gamma] 中的普通运算。由于上下文按结构比较，由分别创建但相同的上下文构建的多项式可以自由组合。

正确性 / 不变量

  • 上下文不变量。 上下文多项式的每个指数向量长度至多为 ∣Γ∣|\Gamma|。具名构造器保证这一点。from_term_polynomial 和 from_sparse_polynomial 不检查它；违反它的多项式会使 eval_named(_checked) 和 to_string 中止。调用者必须确保 polynomial.arity() <= context.size()。
  • 代换对交换系数计算 φσ\varphi_\sigma，即满足 xi↦qix_i \mapsto q_i 的唯一环自同态；结果是规范的（零项消失，如代换 x↦0x \mapsto 0 时）。
  • 部分求值满足 evb∘φa=eva∪b\mathrm{ev}_b \circ \varphi_a = \mathrm{ev}_{a \cup b}。
  • 具名求值等于在按下标列出的值处的按下标求值。
  • 算术即底层存储的算术，并继承其定律。
  • 代价。 代换把每一项按幂的乘积求值并加到累加器中；每次加法都会重新规范化累加器。对 mm 项且结果为 ss 项的情形，仅加法就需 O(m slog⁡s)O(m\, s \log s)，另加多项式乘积的代价。具名查找与上下文大小成线性关系。

被否决的替代方案

  • 顺序代换。 其结果依赖于条目的顺序，并且可以表示为两次同时代换。
  • 投影掉已赋值的变量。 这会改变结果的上下文，并破坏与 Γ\Gamma 上其他多项式的复合。
  • 重复条目以最后一个为准。 这会掩盖错误；拒绝重复可使 σ\sigma 保持为函数。
  • 使用 type_theory 的代换机制。 其避免捕获的代换解决的是多项式不存在的问题，而且其项不会携带多项式规范形式。
  • 隐式上下文并。 见上文：不唯一，而且会使每个二元运算都要对指数重新编号。

边界

  • 没有相等性实例；请显式比较 context() 和项列表。
  • 没有稠密一元存储；上下文多项式总是多元的。
  • 不能从上下文中消去变量，也不能对上下文重命名或重排。
  • 代换需要交换系数才是同态；代码不检查交换性。
  • 错误不携带原因（Option），并且 from_term_polynomial / from_sparse_polynomial 信任其元数。