💻 computer science

When Equality Fails as a Rewrite Principle: Provenance and Definedness for Measurement-Bearing Expressions

该论文提出了一种统一语义框架，通过追踪测量表达式的来源和定义域，证明了普通代数等式在涉及观测复用和除法运算时并非可靠的重写原则，并形式化了支持安全重写、单向简化及特定代数恢复的判定理论。

原作者： David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

发布于 2026-04-10

📖 1 分钟阅读☕ 轻松阅读

原作者： David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文探讨了一个看似简单却极其重要的问题：在科学计算中，我们什么时候可以安全地用一种公式替换另一种公式？

通常，我们认为数学是绝对的： $x - x = 0$ ， $x / x = 1$ 。但在处理带有测量数据的科学公式时，这种简单的“相等即替换”原则会失效，甚至导致灾难性的错误。

为了让你轻松理解，我们可以把科学计算想象成**“侦探破案”或“烹饪实验”**。

核心概念：两个“捣乱鬼”

论文指出，有两个主要的“捣乱鬼”会让数学等式在科学测量中失效：

1. 捣乱鬼一：身世之谜（Provenance / 来源追踪）

比喻：双胞胎 vs. 陌生人

想象你在做一道菜，食谱说：“加两勺盐，然后减去两勺盐。”

情况 A（同一个来源）： 你从同一个盐罐里舀了两次。第一次舀出的盐，第二次又放回去了。
- 结果： $盐 - 盐 = 0$ 。这是完全正确的，因为那是同一份盐。
情况 B（不同来源）： 你从两个不同的盐罐里各舀了一次。虽然两个罐子看起来一样，里面的盐量也差不多，但它们实际上是两堆不同的盐。
- 结果： $盐罐 A - 盐罐 B \neq 0$ 。它们可能有一点点差别，不能直接抵消。

论文的观点： 传统的数学公式只看数字（ $x - x$ ），却忽略了数字背后的“身世”。如果公式里有两个 $x$ ，它们到底是同一个测量值（同一个 token），还是两个长得像的测量值？如果不搞清楚“身世”，盲目地简化公式（比如把 $x-x$ 变成 0），就会掩盖真实的误差。

2. 捣乱鬼二：地雷区（Definedness / 定义域）

比喻：走钢丝 vs. 走平地

想象你在走钢丝（做除法）。

情况 A（安全区）： 你的钢丝离地面很高，永远不会掉下来。这时候， $x / x = 1$ 是安全的。
情况 B（地雷区）： 你的钢丝中间有一段是断的（分母可能为 0）。如果你把公式简化成 $1$，你就假装这段断掉的钢丝不存在了，直接走过去。
- 结果：虽然 $x/x$ 在大多数时候等于 1，但它在 $x=0$ 的地方是地雷。如果你把 $x/x$ 替换成常数 $1 $，你就**消除了地雷**（这是安全的简化）；但如果你把常数$ 1 $替换回$ x/x$，你就埋下了地雷（这是危险的，因为原本安全的公式现在可能爆炸了）。

论文的观点： 数学上的“相等”往往忽略了“在哪里相等”。有些公式在大部分地方相等，但在某些特定地方（比如分母为 0 时）会崩溃。科学计算必须知道公式的**“安全活动范围”**。

论文做了什么？（侦探的解决方案）

作者们设计了一套新的“侦探工具包”，用来给科学公式做**“安全审计”**。这套工具包有两个核心功能：

给每个数字贴“身份证”（Token-sensitive）：
不再把 $x$ 仅仅看作一个数字，而是看作一个带有“出生证明”的测量值。如果公式里有两个 $x$ ，系统会检查它们是不是同一个出生证明。如果是，就可以放心地抵消；如果不是，就不能乱动。
给公式画“安全地图”（Admissible Domains）：
系统会计算这个公式在什么情况下是安全有效的（比如分母不为零）。
- 安全替换原则： 如果你想把公式 A 换成公式 B，B 必须在 A 能工作的所有地方都能工作，而且 B 不能引入新的“地雷”。
- 结论： 简化公式通常是单向的。你可以把“带地雷的公式”简化成“没地雷的公式”（消除隐患），但绝不能反过来（制造隐患）。

论文发现了什么惊人的事实？

作者通过严密的逻辑证明（并在计算机上完成了验证），得出了几个反直觉的结论：

相等不等于可替换： 即使两个公式在它们都能算的地方结果完全一样，如果它们的“安全地图”不一样，也不能互相替换。
只靠“身世”不够，只靠“安全”也不够：
- 如果你只盯着“身世”（是不是同一个测量值），你会忽略分母为零的爆炸风险。
- 如果你只盯着“安全”（分母不为零），你会忽略两个不同测量值不能抵消的误差。
- 必须两者兼顾，才能写出真正安全的科学代码。
简化不是万能的： 很多我们认为理所当然的数学简化（比如 $x/x = 1$ ），在科学测量中其实是有风险的。只有在确认了“测量值永远不为零”且“是同一个测量值”时，这种简化才是合法的。

总结：这对我们意味着什么？

这就好比在自动驾驶或医疗诊断中，计算机不能只说“数学上这俩一样，所以可以互换”。

它必须问：“这两个数据是同一个传感器传来的吗？”（身世）
它必须问：“这个计算在所有可能的情况下都安全吗？”（安全地图）

这篇论文就像给科学计算装上了一套**“防呆系统”**。它告诉我们：在涉及真实世界的测量数据时，数学的优雅必须向物理的现实低头。只有同时追踪数据的“身世”和计算的“安全边界”，我们才能放心地让计算机自动优化科学公式。

一句话总结：
在科学世界里， $x-x$ 不一定等于 0， $x/x$ 不一定等于 1。只有搞清楚数据的“前世今生”和“安全底线”，我们才能安全地进行数学简化。

论文技术总结：当相等性作为重写原则失效时——测量表达式的来源与定义性

1. 研究背景与问题 (Problem)

在科学计算和符号简化中，通常假设代数相等性（Algebraic Equality）是安全的重写原则。然而，对于携带测量值的表达式（Measurement-bearing Expressions），这一假设经常失效。论文指出了导致重写原则失效的两种主要模式：

来源（Provenance）问题：
- 测量值不仅包含数值，还包含其观测来源（Token）。
- 如果公式中两次出现同一个测量值（例如 $x - x$ ），它们代表同一个隐藏的真实值，相减应为 0。
- 如果两次出现的是两个独立的测量值（即使仪器和区间相同，记为 $x_1 - x_2$ ），它们代表两个不同的隐藏真实值，相减不一定为 0。
- 传统的区间算术和量纲分析通常“来源盲视”（provenance-blind），无法区分这两种情况，导致不安全的简化。
定义性（Definedness）问题：
- 除法运算会引入奇点（Singularity，即分母为 0 的情况）。
- 代数上等价的表达式可能在定义域上不同。例如， $x/x$ 在 $x \neq 0$ 时为 1，但在 $x=0$ 处未定义；而常数 $1$ 处处有定义。
- 将 $1 $重写为$ x/x $会引入奇点，这是不安全的；反之，将$ x/x $简化为$ 1$ 虽然消除了奇点，但在某些上下文中可能掩盖了定义域的限制。
- 两个表达式可能在共同定义域上函数值相同，但奇点结构不可比，导致双向重写均不安全。

核心问题：在什么条件下，将一个测量表达式替换为另一个是安全的？现有的形式化方法无法同时处理来源依赖和定义域限制。

2. 方法论 (Methodology)

作者提出了一种统一的语义框架，结合了“来源敏感”和“定义域感知”两个维度，并在 Lean 4 中完成了形式化验证（无 sorry，包含 143 个定理和 45 个定义）。

2.1 语义基础

表达式语言：包含精确有理数常量和测量叶子节点。每个测量叶子 $Meas(t, I, d)$ 包含：
- 不透明令牌 $t$ （观测事件 ID）。
- 有理数区间 $I$ （隐藏真实值的边界）。
- 维度标签 $d$ 。
令牌环境（Token Environment）：将每个令牌映射到一个精确的有理数。
来源敏感语义：
- **保证包络（Warranted Enclosure, $Encl(e) $）**：在所有与表达式令牌一致的环境中，表达式可能取到的值集合。这捕捉了来源依赖（如$ x-x=0$）。
- 定义包络（Defined Enclosure, $DefinedEncl(e)$）：仅在**可接受域（Admissible Domain）**内的环境中计算的值集合。
**可接受域（Admissible Domain, $AdmDom(e) $）**：表达式$ e$ 在该环境下不仅令牌一致，且所有除法子表达式的分母均不为零。

2.2 重写判定规则

论文定义了三个层级的重写判定：

基于包络的重写（Enclosure-based）：仅考虑来源。
- $e \rightsquigarrow e'$ ： $Encl(e') \subseteq Encl(e)$ （目标比源更紧或相等）。
- $e \rightleftharpoons e'$ ：双向等价。
域感知重写（Domain-aware）：结合来源和定义性。
- 域安全重写（DomainSafeRewrite, $e \rightsquigarrow_d e'$ ）：
  1. 目标的可接受域必须包含源的可接受域（ $AdmDom(e) \subseteq AdmDom(e')$ ）。
  2. 在源的定义域内，目标计算出的值必须在源的保证包络内。
- 域相等（DomainEqual）：在共同定义域上函数值相等，但不要求定义域包含关系。
支持相对判定（Support-relative）：将可接受性限制在任意支持集 $S$ 上，用于连接局部简化规则与全局理论。

3. 主要贡献 (Key Contributions)

令牌敏感包络语义：提出了一种能区分“重用同一测量”与“使用两个相似测量”的语义模型，通过令牌一致性自动处理来源依赖。
域安全重写判定：引入了基于可接受域包含关系的重写规则。证明了域安全重写是非传递的（Non-transitive），即局部安全的简化步骤组合后可能不再安全，必须逐步验证。
还原与恢复定理（Reduction & Recovery）：
- 还原：在“普遍可接受”（无奇点风险）的片段上，域感知理论退化为基于包络的来源理论。
- 恢复：在支持相对层内，形式化了常见的正类简化规则（如相同令牌抵消、背景减法、正区间自除），证明它们作为上下文定理成立。
严格性结果（Strictness Results）：
- 一旦奇点可达，简化变为单向（只能消除奇点，不能引入）。
- 证明了“共同域相等”（Common-domain equality）对于授权替换来说太弱，因为两个表达式可能在共同定义域相等，但定义域结构不可比，导致双向重写均失败。
不充分性定理（Insufficiency Theorem）：
- 证明了仅靠来源或仅靠定义性都不足以保证重写的安全性。
- 如果抹去令牌身份，原本可区分的重写类会坍缩；如果忽略定义域，也会丢失关键信息。两者必须联合使用。
Lean 4 形式化：所有定义和定理均在 Lean 4 中完成，无 sorry，确保了逻辑的严密性。

4. 关键结果 (Key Results)

单向简化（One-way Simplification）：
- 对于 $x/x$ （ $x$ 在 $[0, 1]$ 区间），简化为 $1 $是安全的（因为$ 1 $的定义域更广），但反向替换是不安全的（引入了$ x=0$ 的奇点）。
- 对于 $x/x$ （ $x$ 在 $[0.1, 1]$ 区间，正区间）， $x/x$ 与 $1$ 是双向等价的，因为奇点不可达。
非坍缩（Non-collapse）：
- 构造了两个表达式 $e_1 = x/x$ 和 $e_2 = (x-1)/(x-1)$ 。它们在 $x \neq 0$ 且 $x \neq 1$ 时都等于 1。
- 但是， $e_1$ 在 $x=1$ 处有定义而 $e_2$ 无定义， $e_2$ 在 $x=0$ 处有定义而 $e_1$ 无定义。
- 结果：两者定义域互不包含，因此双向重写均不安全，尽管它们在共同定义域上完全相等。
来源盲视的失败：
- 如果忽略令牌，$Meas(t, I) - Meas(t, I) $和$ Meas(t_1, I) - Meas(t_2, I)$ 在盲视语义下看起来一样。但前者可简化为 0，后者只能单向简化（或不可简化）。
- 这证明了令牌身份是区分重写类的必要条件。

5. 意义与影响 (Significance)

理论突破：该论文揭示了在科学计算中，传统的代数相等性不足以作为重写规则的基础。必须同时考虑观测来源（Provenance）和定义域（Definedness）。
形式化验证：通过 Lean 4 的严格形式化，消除了人类推理中可能出现的关于定义域和奇点的直觉错误（例如误以为 $x/x$ 总是等于 1）。
实际应用：
- 为科学符号简化器（Symbolic Simplifiers）提供了理论基础，表明在进行优化时必须携带来源注释和可接受性检查。
- 解释了为什么某些局部优化在组合时会失效（非传递性），强调了逐步验证的重要性。
局限性：目前仅处理除法引起的奇点，未涉及溢出、下溢或类型错误；维度系统目前仅为语法标签，未深入物理单位代数。

总结：这篇论文建立了一个统一的数学框架，证明了对于携带测量值的表达式，没有任何单一的语义（仅值、仅来源或仅共同定义域）能支持安全的重写分类。只有结合令牌敏感性和定义域感知，才能构建出可靠的科学公式简化系统。