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 * y`` - 预处理：``(x * y)`` 判定规则： - 量纲签名一致时进入核心比较；其他情况结果为 ``false`` 作用： - 降低符号重写图规模 - 减少 ``EqvBudgetExceeded`` 发生概率 5. 预算与终止策略 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 为保证终止，``===`` 必须设置预算上限： - 最大重写步数：``maxRewriteSteps = 256`` - 最大递归深度：``maxRewriteDepth = 64`` - 最大节点增长倍数：``maxNodeGrowthFactor = 4`` 任一预算耗尽即停止化简并返回 ``false`` （可附带诊断标记 ``EqvBudgetExceeded`` ）。 6. 决策流程 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: text 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 下必然成立 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ .. code-block:: text sym x x + 0 === x # true x^2 + 2*x + 1 === (x + 1)^2 # true 7.2 Core 下不保证成立 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ .. code-block:: text sin(pi/4)^2 + cos(pi/4)^2 === 1 # 在 Core profile 下通常为 false 7.3 开启 Trig-Basic 后可成立 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ .. code-block:: text # 假设 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 中若出现 ``===``，同样遵循本规范