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

基本信息

  • LSR 编号 007

  • 标题 === 数学等价判定规范

  • 作者 Ziyang-Bai

  • 状态 草案

  • 类型 标准规范

  • 创建日期 04-05-2026

  • 归属项目 编译器、CAS

摘要

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

技术规范

1. 适用范围

  • === 仅适用于 Expr

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

2. 语义定义

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

  1. 对 a、b 执行量纲标准化预处理（见第 4.3 节）

  2. 对预处理后的纯数学核心分别执行受限规范化（见第 4 节）

  3. 若量纲签名一致且核心结构相同，则返回 true

  4. 否则返回 false

规则：

  • false 含义为“在当前规则与预算下未能证明等价”，不等价于“数学上必不等价”

  • 该定义保证判定过程总能终止

3. 判定边界

  • 根据 Richardson 定理，包含初等函数的恒等式判定采用有限规则集

  • 承诺范围限定为可终止性与规则内可靠性（soundness over supported rules）

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

4.1 必选规则集（Core）

1. 常量折叠 - 有理数与整数的精确化简 - 代数恒等式：x + 0 -> x，x * 1 -> x，x * 0 -> 0，x - x -> 0

2. 多项式标准形（交换/结合规范化） - 对 +、* 进行交换与结合归一化 - 同类项合并 - 有理系数多项式标准化

3. 分式与幂的基础化简 - 分式约分（可约分项） - 整数幂规则（在安全条件下）

4.2 可选规则集（Extended，profile）

1. Trig-Basic（可选） - 基础恒等式：sin(x)^2 + cos(x)^2 -> 1 - 奇偶性：sin(-x) -> -sin(x)，cos(-x) -> cos(x)

2. 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 中若出现 ===，同样遵循本规范