AI 中文总结
该研究针对带来源标注的生成系统，提出三种端点充分性层次，建立严格层次关系，给出计算精确分支商的划分精化过程，为保留来源提供仅区分行为差异的准则。
AI 中文摘要
带来源标注的生成系统可能存在具有相同可见端点的不同实例，因此核心抽象问题是：何时可以忽略来源而不改变合法的未来行为？我们通过合法生成诱导的标记迁移系统和从实例到可见对象的端点投影U来研究该问题，划分出三个观察层次：启用充分性保留立即可用的规则标签；迹充分性保留所有有限合法规则标签迹；商充分性保留模端点等价的分支迁移结构，形成的层次是严格的。在线性时间层次，端点迹充分性等价于端点等价包含有限迹等价；在分支层次，当端点等价是强互模拟等价时，规范端点商与代表无关。随后提出两种规范修正：将端点等价与迹等价相交得到保留有限迹的最大端点尊重关系；最大端点尊重互模拟得到最粗的精确分支商，是所有端点尊重精确商中的通用形式，对于有限系统，可通过以端点类为初始的终止划分精化过程计算。对带来源标注的嵌套递归重组生成的自包含应用显示，两个具有相同可见图I->A->B但不同启用未来的实例，精化过程在第一轮就将它们分离。该结果将保留来源的非此即彼要求替换为仅保留行为上仍起作用的差异的精确准则。
英文摘要
A provenance-decorated generative system may contain distinct occurrences with the same visible endpoint. The central abstraction question is therefore exact: when may provenance be forgotten without changing the lawful future? We study this question through the labeled transition system induced by lawful generation and an endpoint projection U from occurrences to visible objects. Three observation levels are separated. Enabled sufficiency preserves immediately available rule labels; trace sufficiency preserves all finite lawful rule-label traces; quotient sufficiency preserves the branching transition structure modulo endpoint equivalence. The resulting hierarchy is strict. At the linear-time level, endpoint trace sufficiency is exactly inclusion of endpoint equivalence in finite-trace equivalence. At the branching level, the canonical endpoint quotient is representative-independent exactly when endpoint equivalence is a strong bisimulation equivalence. Two canonical repairs follow. Intersecting endpoint equivalence with trace equivalence gives the greatest endpoint-respecting relation preserving finite traces. The greatest endpoint-respecting bisimulation gives the maximally coarse exact branching quotient and is universal among endpoint-respecting exact quotients. For finite systems it is computed by a terminating partition-refinement procedure initialized by endpoint classes. A self-contained application to provenance-decorated nested recursive-recombinant generation exhibits two occurrences with the same visible graph I->A->B but different enabled futures; the refinement procedure separates them in its first round. The result replaces an all-or-nothing demand to retain provenance with an exact criterion for retaining only the distinctions that remain behaviorally operative.
Comments12 pages
