LSR 007 - === 数学等价判定规范¶
基本信息¶
LSR 编号 007
标题
===数学等价判定规范作者 Ziyang-Bai
状态 草案
类型 标准规范
创建日期 04-05-2026
归属项目 编译器、CAS
摘要¶
定义 num 上 === 与 std.cas.equivalent 的三态证明语义、保域化简和局部预算 [1]。证明成立、证明不等价和证明未决必须分别返回固定状态，不以布尔假值合并后两者。
技术规范¶
1. 适用范围与返回状态¶
a === b 接受两个 num 数学值，等价于采用默认配置的 std.cas.equivalent(a, b)。Lambda 中使用该运算符同样遵循本规范 [2]。
返回类型为 std.cas.Equivalence，具有三个固定状态：
cas.Equivalent：当前假设下已证明两者具有相同定义域，并在该定义域上取相同值cas.Different：已证明不等价，例如精确常量值不同，或已证明定义域不同cas.Unknown：当前规则、假设或预算不足以证明上述任一结论
这是标准库固定状态类型，不提供用户定义代数数据类型机制。状态之间的 ==、!= 返回 bool。状态不隐式转换为 bool，尤其不得把 Unknown 当作 Different。
操作数类型不符时诊断 EqvTypeMismatch。num 包含精确数、符号表达式、关系和近似值；比较关系表达式时证明的是关系的数学等价，而不是比较其源码文本 [3]。
2. 证明语义¶
证明在当前明确给定的假设下进行：
检查操作数类型和数学支持域，提取静态量纲签名
在同一次查询的共享预算内，对数学核心执行保域规范化
若能够证明定义域及取值相同，返回
Equivalent若能够证明定义域或取值不同，返回
Different其余情况返回
Unknown
规范化后结构不同、某条规则未启用、假设缺失或预算耗尽均不能单独作为不等价的证明。根据 Richardson 定理，包含初等函数的恒等式判定不承诺完备；承诺范围为有限预算下的终止性及支持规则的可靠性。
3. 结构、关系与等价¶
三种操作具有不同用途：
a == b构造类型为num的数学等式，不是结构查询std.cas.same_structure(a, b)返回bool，比较既有数学结构，不执行有限证明 [3]a === b返回Equivalence，尝试证明数学等价
集合去重、哈希键、规则冲突检测及模式匹配必须递归使用结构相等，不能调用构造关系的 ==，也不能使用受预算影响的 ===。证明预算及规则配置不进入结构键。
4. 规范化规则与定义域¶
4.1 必选规则集（Core）¶
Core 包括：
整数、有理数和支持的精确常量折叠
在运算有定义的局部前提下应用
x + 0 -> x、x * 1 -> x等恒等式在声明支持的交换代数域中，对加法、乘法进行交换结合规范化、同类项合并和有理系数多项式标准化
具有局部可除性、非零及定义性前提的分式约分和整数幂规则
虚数单位基础规则
I^2 -> -1[4]
不得因消去项而丢失定义域限制。例如 x/x -> 1 需要 x 非零；0 * (1/x) -> 0 也需要倒数有定义。x - x -> 0 和零乘规则只在被消去子式有定义的局部前提下应用。假设不足时保留原式或返回证明未决，不能以形式约分冒充保域等价。
4.2 可选规则集（Extended，profile）¶
可选 profile 在 Core 上增加规则：
Trig-Basic：适用域内的sin(x)^2 + cos(x)^2 -> 1及三角函数奇偶性ExpLog-Basic：适用主值和定义域内的exp(log(x)) -> x，以及log(1) -> 0、exp(0) -> 1
复对数、平方根和非整数幂遵循 LSR-010 的单值主值约定 [4]；不得无条件使用跨分支的对数或幂恒等式。默认 profile 为 Core。
4.3 保域与形式代数入口¶
std.cas.simplify 与 std.cas.simplify_formal 均接收 num 并返回 num：
simplify默认保域，仅在局部成立条件满足时重写simplify_formal显式采用其声明支持的形式代数域，例如有理函数域中按形式非零元约分；该接口必须说明支持域，不接受任意数学对象的无条件消去
形式化简的结果不保证保留原表达式每个点上的定义域。调用形式入口不改变 === 的保域契约，也不设置全局模式；原表达式不能仅凭形式结果相同就判为 Equivalent。
4.4 量纲标准化¶
证明前按核心语言及 LSR-008 的静态量纲规则提取并合并量纲标签，将数学核心与量纲签名分离 [1] [5]。该处理不得擦除量纲、使非法量纲运算合法，或从运行期裸数恢复已被显式剥离的信息。
量纲签名一致时继续比较核心；对两个合法数学值，已知量纲不一致可证明不等价。量纲运算本身非法时走类型或数学错误路径，不以 Unknown 掩盖。近似工作精度不是量纲的一部分。
5. 近似值的比较¶
精确值和近似值按各自现有存储数值无损比较，不先将精确值舍入到近似值精度，也不引入隐式容差。两个近似值同样按现有表示值比较；所得结论只关于这些表示值，不证明近似前原式的相等或不等。
精确数值叶的比较不依赖小整数、大整数、有理数等内部表示。近似节点的结构查询还须区分近似类别、目标工作精度等语义结构，并与精确叶区别。结构不同不妨碍在表示值确实相等时证明数值等价。
提升工作精度不能恢复旧输入已经丢失的精度。证明和化简须保留近似标记与精度信息，不得把打印的小数重新解释为精确数并当作原数学对象。需要容差的应用应使用另行声明的查询，不得改变 === 的含义。
6. 局部预算与终止策略¶
每次查询使用独立预算；该次查询内的预处理、规范化和证明子查询共享预算，不得通过递归调用重新获得额度。默认上限为：
最大重写步数：
steps = 256最大递归深度：
depth = 64最大节点增长倍数：
growth = 4
某项预算耗尽且尚无证明时返回 cas.Unknown，可附带 EqvBudgetExceeded 诊断。取消、内存故障及其他运行时错误继续按错误通道传播，不能统称为预算未决。局部预算不影响其他查询，也不改变结构相等关系。
7. 配置接口¶
std.cas.equivalent 提供两种调用形式，均返回 Equivalence：
func equivalent(a num, b num) -> Equivalence
func equivalent(a num, b num, profile text, steps int, depth int, growth int) -> Equivalence
二参形式采用以下默认配置；显式配置形式必须提供全部四项配置，不允许任意省略。=== 使用二参形式的默认配置。
参数 |
值约束或类型 |
二参形式的配置 |
|---|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
int 是 num 上的值约束，不是另一基本类型。预算参数还须能够具体求值。显式配置形式可使用普通具名实参，按普通调用规则绑定与校验 [1]；未知 profile 或非法预算报 InvalidArgument，不得静默选用另一配置。配置只作用于本次查询，不使用无作用域的可变全局 setter 改写其他调用的行为。
8. 示例¶
import std.cas
sym x
let identity = (x + 0) === x
let polynomial = (x^2 + 2*x + 1) === (x + 1)^2
let different = 1 === 2
let unresolved = (x/x) === 1
let proved = identity == cas.Equivalent
identity、polynomial 为 cas.Equivalent，different 为 cas.Different。没有 x 非零前提时，不得仅凭约分把 unresolved 判为 cas.Equivalent：若能证明原式与常量的定义域不同，则为 cas.Different；否则为 cas.Unknown。proved 是普通 bool。
import std.cas
use std.math.{sin, cos}
sym x
let basic = cas.equivalent(sin(x)^2 + cos(x)^2, 1)
let trig = cas.equivalent(sin(x)^2 + cos(x)^2, 1,
profile="Trig-Basic", steps=256, depth=64, growth=4)
Core 不要求证明该三角恒等式；若没有其他适用证明，basic 为 cas.Unknown，而不是 cas.Different。在该规则的支持域内 trig 为 cas.Equivalent。
9. 错误与诊断¶
EqvTypeMismatch：操作数不是受支持的num数学值EqvBudgetExceeded：预算耗尽，证明未决的可选诊断，不表示不等价EqvRuleDisabled：所需规则未启用的可选诊断InvalidArgument：查询配置无效
类型、定义域和运行时故障按核心语言及 LSR-018 的错误通道传播 [6]。固定状态只表达正常完成的证明结论，不替代错误处理。
