Endpoint Sufficiency Behavioral Quotients

技术摘要：何时遗忘溯源（Provenance）是合法的？

问题陈述
生成式系统通常会产生可以由多个抽象层级表示的对象。一种表示法仅捕捉“可见终点”（最终对象），而另一种表示法则保留完整的“溯源”（祖先、合并事件、依赖结构）。虽然终点表示法更小，但如果系统的容许性法则（admissibility laws）依赖于谱系，则这些表示法存在成为错误状态描述的风险。本文旨在解决的核心问题是：确定究竟何时可以安全地遗忘溯源信息，而不改变系统的合法未来行为。具体而言，本文探讨了：终点投影在何种情况下能保留足够的足够信息以确定合法的转换，以及可以丢弃的最大溯源量是多少。

本文挑战了“终点充分性”（endpoint sufficiency）是一个单一、统一概念的非正式假设。研究表明，这一概念取决于观察层级：是仅关注立即启用的规则、有限的规则标签序列（轨迹/traces），还是未来的完整分支结构。

方法论
作者使用**合法生成转换系统（Lawful Generative Transition Systems, LGTS）**将该问题形式化。一个 LGTS 定义为一个元组 $T = (S, \Sigma, \to, U, X, \cong_X)$，其中：

• $S$ 是由溯源装饰的发生（occurrences）集合。
• $\Sigma$ 是规则标签集合。
• $\to$ 是合法的标记转换关系。
• $U: S \to X$ 是将发生映射到可见对象的终点投影。
• $\cong_X$ 是可见对象上的等价关系。

本研究分析了终点等价关系（$\equiv_U$，其中 $s \equiv_U t \iff U(s) \cong_X U(t)$）与各种行为等价关系之间的关系。分析通过三个不同的观察层级进行：

1. 启用充分性（Enabled Sufficiency）： 保留立即可用的规则标签集。
2. 轨迹充分性（Trace Sufficiency）： 保留所有有限规则标签轨迹的集合。
3. 商（分支）充分性（Quotient/Branching Sufficiency）： 在模终点等价的情况下，保留分支转换结构。

本文采用了标准的进程语义工具，包括轨迹等价、强双模拟（strong bisimulation）、余归纳（coinduction）和划分细化（partition refinement），并专门应用于终点与溯源之间的边界。

核心贡献与结果

1. 严格的三层层级结构
本文确立了这三个充分性层级是截然不同的，并构成了一个严格的层级：
$$\text{商充分性 (Quotient Sufficiency)} \implies \text{轨迹充分性 (Trace Sufficiency)} \implies \text{启用充分性 (Enabled Sufficiency)}$$

• 启用充分性是最弱的；它仅要求等价的终点具有相同的下一跳可用规则集。
• 轨迹充分性要求等价的终点生成相同的有限规则标签序列集。
• 商充分性是最强的；它要求对于任何标签，可达的终点类集合仅取决于当前的终点类，而非特定的溯源历史。

2. 充分性的精确准则
本文为不同层级的投影何时具有充分性提供了精确的数学准则：

• 轨迹层级： 当且仅当终点等价是轨迹等价的子集时（$\equiv_U \subseteq \equiv_{tr}$），该投影是轨迹充分的。
• 分支层级： 当且仅当终点等价是一种强双模拟等价时，该投影是商充分的。这意味着对于任何两个终点等价的状态，其中一个的每一次转换都可以由另一个的转换来匹配，且跳转到的状态仍是终点等价的。

3. 规范修复与最大化遗忘
当原始终点等价无法实现充分性时，本文提出了两种“规范修复”（canonical repairs），用于识别在尊重可见终点的同时，能够保留所需行为的最粗细的细化状态：

• 针对线性时间（轨迹）： 关系 $E^U_{tr} = \equiv_U \cap \equiv_{tr}$ 是尊重终点且保留有限轨迹的最大等价关系。它精确地识别了那些在规则标签轨迹方面不可区分的等价终点发生。
• 针对分支时间（精确商）： 关系 $\approx_U$ 被定义为所有尊重终点的强双模拟关系的并集，它是最大的终点尊重强双模拟关系。商系统 $T / \approx_U$ 是最大粗细的精确分支商。
  • 普遍性质： 每一个其他的精确终点尊重商都是对该规范商的细化。因此，$\approx_U$ 代表了在维持精确分支语义的同时，可以遗忘的最大溯源量。

4. 算法计算
对于有限系统，本文描述了一种用于计算 $\approx_U$ 的终止划分细化程序。该算法从终点等价类划分开始，根据“后继块的签名”（即每个标签可达的块集合）迭代地细化划分。该程序在对应于 $\approx_U$ 的划分处稳定。

5. 在嵌套递归-重组生成（NRRG）中的应用
本文将这些结果应用于特定的经溯源装饰的 NRRG 框架。文中展示了一个见证案例，其中两个发生（$e_G$ 和 $e_H$）共享相同的可见图终点（$I \to A \to B$），但在重组祖先方面存在差异。

• 在 $e_G$ 中，其祖先允许一个边界接触型重写规则（$R_B$）。
• 在 $e_H$ 中，其祖先禁止 $R_B$。
• 结果： 划分细化算法在第一轮中就将 $e_G$ 和 $e_H$ 分离开来，因为它们的启用后继集不同。这证明了即使在启用层级，终点同构也不意味着行为等价，并且所提出的细化程序能正确识别必要的区别。

意义与主张
本文声称，通过提供精确的遗忘准则，取代了“全有或全无”的诉求（即要么保留全部溯源，要么完全丢弃溯源）。

• 操作残余（Operational Residue）： 原始终点类与细化类（$\approx_U$ 或 $E^U_{tr}$）之间的差异构成了溯源的“操作残余”——即在未来的转换空间中仍然活跃的历史信息。
• 抽象精确性： 本工作将抽象问题重新定义为不仅是关于可靠性（过近似），而是针对选定语义的精确性。一个在未检查双模拟的情况下合并状态的原始商系统，可能会产生对于特定发生而言是不合法的行为（膨胀）。
• 领域无关性： 结果以形式化准则的形式呈现，适用于任何依赖于谱系的系统（如软件状态、法律文书、科学主张），只要该系统可以被建模为带有终点投影的有标记转换系统。

本文得出结论：溯源可以在那些不改变所选合法未来语义的发生区别上被精确地擦除。在最大化安全擦除后留下的不再是历史装饰，而是真正的生成状态。