LSR 007 - `===` 数学等价判定规范

基本信息

LSR 编号 007
标题 === 数学等价判定规范
作者 Ziyang-Bai
状态草案
类型标准规范
创建日期 04-05-2026
归属项目编译器、CAS

摘要

定义 === 在 Expr 上的判定语义、化简边界与终止策略。采用有限规则与预算：可证明返回 true，否则 false。

技术规范

1. 适用范围

=== 仅适用于 Expr
非 Expr 操作数使用 === 必须在类型检查阶段报错 EqvTypeMismatch

2. 语义定义

对 a === b 执行有限证明流程：

对 a、b 执行量纲标准化预处理（见第 4.3 节）
对预处理后的纯数学核心分别执行受限规范化（见第 4 节）
若量纲签名一致且核心结构相同，则返回 true
否则返回 false

规则：

false 含义为“在当前规则与预算下未能证明等价”，不等价于“数学上必不等价”
该定义保证判定过程总能终止

3. 判定边界

根据 Richardson 定理，包含初等函数的恒等式判定采用有限规则集
承诺范围限定为可终止性与规则内可靠性（soundness over supported rules）

4. 规范化规则与化简深度

4.1 必选规则集（Core）

常量折叠
有理数与整数的精确化简
代数恒等式：x + 0 -> x，x * 1 -> x，x * 0 -> 0，x - x -> 0
多项式标准形（交换/结合规范化）
对 +、* 进行交换与结合归一化
同类项合并
有理系数多项式标准化
分式与幂的基础化简
分式约分（可约分项）
整数幂规则（在安全条件下）

4.2 可选规则集（Extended，profile）

Trig-Basic（可选）
基础恒等式：sin(x)^2 + cos(x)^2 -> 1
奇偶性：sin(-x) -> -sin(x)，cos(-x) -> cos(x)
ExpLog-Basic（可选）
在定义域安全前提下：exp(log(x)) -> x
常量级规则：log(1) -> 0，exp(0) -> 1

默认 profile：Core。

4.3 量纲标准化预处理（Canonicalization）

在进入 === 核心化简前，必须执行“量纲提取”步骤：

将表达式中的量纲标签提取并合并到最外层
纯数学核心与量纲签名分离后再进入重写系统

示意：

输入：x<m> * y<s>
预处理：(x * y)<m*s>

判定规则：

量纲签名一致时进入核心比较；其他情况结果为 false

作用：

降低符号重写图规模
减少 EqvBudgetExceeded 发生概率

5. 预算与终止策略

为保证终止，=== 必须设置预算上限：

最大重写步数：maxRewriteSteps = 256
最大递归深度：maxRewriteDepth = 64
最大节点增长倍数：maxNodeGrowthFactor = 4

任一预算耗尽即停止化简并返回 false（可附带诊断标记 EqvBudgetExceeded）。

6. 决策流程

eqv(a, b):
  if type(a) != Expr or type(b) != Expr: type error
  (ua, ca) = canonicalize_units(a)
  (ub, cb) = canonicalize_units(b)
  if ua != ub: return false
  na = normalize(ca, profile, budget)
  nb = normalize(cb, profile, budget)
  if structurally_equal(na, nb): return true
  else: return false

7. 示例

7.1 Core 下必然成立

sym x
x + 0 === x                       # true
x^2 + 2*x + 1 === (x + 1)^2       # true

7.2 Core 下不保证成立

sin(pi/4)^2 + cos(pi/4)^2 === 1   # 在 Core profile 下通常为 false

7.3 开启 Trig-Basic 后可成立

# 假设 profile = Trig-Basic
sin(pi/4)^2 + cos(pi/4)^2 === 1   # true

8. 配置接口

set_eqv_profile("Core" | "Trig-Basic" | "ExpLog-Basic")
set_eqv_budget(steps, depth, growth)

未设置时采用默认值：Core + 第 5 节预算。

9. 错误与诊断

EqvTypeMismatch: === 作用于非 Expr
EqvBudgetExceeded: 达到预算上限，停止证明
EqvRuleDisabled: 依赖的规则集未启用（可选诊断）

10. 与其他 LSR 的关系

LSR-000：声明 === 存在并引用本规范作为唯一语义来源
LSR-005：match 守卫中的 === 语义依赖本规范
LSR-006：Lambda 中若出现 ===，同样遵循本规范

LSR 007 - === 数学等价判定规范