摘要
无冲突复制数据类型为协调独立更新的副本提供了一种有原则依据的方法。其收敛保证很有价值，但范围小于对用户意图、应用不变式或访问控制决策的保持。本综述将 CRDT 的代数基础与复制式 JSON 及本地优先软件联系起来，随后展开一个小型只增集合示例和一个预订超额的反例。文章区分状态合并与操作投递，将删除和元数据回收视为语义选择，并推导出同步延迟和元数据增长的简单模型。本文主张，协作软件需要两份规约：一份规定副本间的一致，另一份规定并发编辑的含义。随附的有限测试检查合并定律，并保留一个具体见证，说明为什么仅靠收敛无法强制满足容量约束。
两位用户可能就错误答案达成一致
设想两位断网的编辑正在预订最后一个可用的审阅名额。每个副本都显示还剩一个名额，每位编辑都在本地成功预订。当副本重新连接时，合并可以保留两份预订，并实现完全收敛。最终状态在各设备间一致，却违反了容量规则。无论网络重试还是确定性的平局裁决规则，都不会自动解决对这两个人作出的承诺。
这个例子区分了代数性质与产品契约。收敛关注的是，拥有相同相关信息的副本是否得到相同状态。意图关注的是，结果状态是否以可接受的方式表达了用户的行为。不变式则约束哪些状态从根本上是允许的。协作系统必须决定，哪些行为可以在离线时接受，哪些需要协调、预留权利，或明确说明之后可能被拒绝。
所选文献确立了基础
Shapiro 及其同事给出了强最终一致性的充分条件，并区分了基于状态和基于操作的构造。Kleppmann 和 Beresford 为一种支持嵌套结构与并发更新的复制式 JSON 数据类型提供了形式语义。本地优先软件论文则将讨论扩展到所有权、离线使用、协作以及对数据的长期控制。
这些贡献相互补充。第一项提供代数和投递模型基础，第二项提供具体的结构化数据类型，第三项提供产品与架构视角。它们都不意味着，合并任意在本地有效的变更就能保持每一条业务规则。我们借助这些工作，将机器层面的协调问题，与用户按下操作按钮时应用层面作出的承诺区分开来。 [1], [2], [3]
可以穷举检查的合并定律
对于只增集合，状态是元素集合，合并就是通常的并集。并集满足结合律、交换律和幂等律。因此，对收到的状态重新分组、重新排序或重复处理，都不会改变最终并集。如果每次添加最终都到达每个参与副本，那么所有副本最终都可以包含相同的集合。
有限检查附录枚举了四元素全集的全部子集，并检查三条定律，其中包括用于检查结合律的每一个三元组。这些数学恒等式在该有限全集之外也成立，但程序只是对所实现运算进行的有界一致性检查。它不能证明某个传输机制、持久化层，或某种仅仅被称为 CRDT 的任意数据类型会收敛。最终投递假设仍然必要；任何合并规则都无法纳入永远不会到达的信息。
基于状态与基于操作的设计承担不同义务
当状态偏序和合并构成所需的单调结构时，基于状态的设计可以反复交换状态。基于操作的设计交换更新，必须满足其构造所要求的投递条件与交换性条件。重放完整状态和重放操作并不是可以互换的行为。即使正确表示的计数器状态在重复合并时不会重复计数，投递两次的递增操作仍可能计数两次。
因此，工程审查必须记录消息代表什么、哪些操作可能并发，以及如何处理重复项和因果依赖。宣称提供至少一次投递的传输机制，可能兼容某种状态表示，却不兼容一种朴素的操作表示。反过来，增加全序服务可能改变可用性与成本，但并非每种数据类型都需要它。要求来自具体语义，而不是一个笼统的同步标签。 [1]
即使完全收敛，容量反例仍然成立
将预订表示为只增集合，并将容量设为一。副本 A 添加预订 a，同时副本 B 添加预订 b。每个本地集合的大小都为一，满足容量限制。它们的并集大小为二。这个见证证明，对于这些可独立到达的状态，该不变式在这种合并下不具有封闭性。
有多种可能的应对方式，每种都会改变产品契约：协调预订的接受过程；预先分配数量有限的可转让权利；或者接受之后可能被拒绝的暂定预订。合并后只选择一份预订同样能够收敛，但这会撤销此前的本地成功，因此需要向用户明确显示其状态。错误并不在于选错了合并代数，而在于最终接受所需的信息不可用时，却承诺最终接受。
删除是关于历史的规则
从复制集合中移除元素比添加元素更微妙。如果过时副本能够重新引入旧元素，那么物理删除当前表示可能无法表达预期的移除。设计往往保留标识符或因果信息，使后续合并能够区分旧添加与新添加。并发添加和移除的语义必须明确规定，而不能偶然发现。
文档编辑中也存在同样的问题：删除一个段落，同时编辑其中的一个句子，需要预先规定结果。保留所有信息有助于恢复，却可能产生出乎意料的可见文档。丢弃信息可以简化界面，却可能抹去一次编辑。JSON 文献说明了嵌套结构为何需要精确的并发语义；应用所接受的行为仍须通过贴近实际的编辑任务来评估。 [2]
垃圾回收需要知识边界
记录已移除或已被替代操作的元数据，即使在可见文档仍很小时也可能不断增长。安全回收它需要证据，证明旧操作不会以改变历史解释的方式重新出现。永久离线的设备、恢复的备份，或被复制的副本身份，都会使这种证据更加复杂。
一个简单的存储模型为 u 次操作中的每次操作分配 m 字节的保留元数据，在压缩和建立索引前共占 um 字节。如果每次操作占 32 字节，那么保留一百万次操作会消耗 32 百万字节。图中展示的是这种线性记账成本，而不是某个 CRDT 库的实际占用。压缩、快照和因果稳定化都可能显著改变它。它们的正确性条件比斜率更重要：信息被回收后，不得使旧状态能够复活当前契约认为已被移除的内容。
同步延迟不等于语义不确定性
对于一对用于说明的副本，假设成功的反熵接触遵循速率为 lambda 的泊松过程。经过时间 t 后，更新尚未越过链路的概率为负 lambda t 的指数函数。传播延迟的中位数为二的自然对数除以 lambda。这些曲线假设一次成功接触会传输全部相关状态，并忽略排队、批处理和多跳拓扑。
传播延迟中位数较低，并不能说明合并结果是否保持了工作流的含义。系统可以非常迅速地同步超额预订。反过来，即使传播延迟很长，安全的离线编辑操作仍可能有用。性能与语义应分别评估，再通过可见的同步状态、可恢复的历史，以及对暂定操作和最终操作的如实区分，将两者整合到用户体验中。
离线变更协调后仍须维持授权约束
副本在离线时可能拥有授权，却在重新连接前被撤销授权。系统必须决定，先前创建的哪些操作仍可接纳，如何确定创建时间，以及哪个权威主体可以拒绝或隔离这些操作。由客户端控制的时间戳不足以证明操作创建于授权撤销之前。盲目合并每一个语法有效的操作，可能在保持代数收敛的同时违反访问策略。
这是应用和信任模型的问题，而不是拒绝本地优先架构的理由。根据需求，签名能力凭证、有界离线权限、服务端准入，或分离的机密数据域与协作数据域，都可能适用。关键在于，数据类型的合并函数本身并不决定谁曾被允许创建各个元素。身份与授权必须成为外围操作协议的一部分。
评估必须涵盖人和历史
拟议的评估应结合代数检查与场景测试。代数检查检验所需的结合性、交换性、幂等性，以及因果投递和重复处理。场景测试包括并发重命名与删除、移动正在被编辑的对象、远程变更后的撤销、恢复的备份，以及被撤销授权的协作者。应同时把结果作为状态，以及作为参与者能够理解的历史来检查。
可用性主张需要实际用户的证据，而不只是确定性收敛。一个有用的方案会记录，人们是否能找到自己的工作、理解冲突解决方式，以及从非预期结果中恢复。我们尚未开展这类研究。可执行示例仅确立了两个范围更窄的事实：玩具集合的合并满足其声明的定律，而一对各自独立有效的预订，在同样的合并后可能违反共享不变式。
结论：分别规定一致与含义
CRDT 以明确的数学条件取代临时拼凑的协调方式，大幅提高了协作状态管理的可靠性。当其保证被准确表述时，这一优势最为清晰。获得等价信息后达成一致，不同于保持每位用户的意图、每项资源约束或每项授权决策。
因此，实际的研究议程应采用组合式思路：选择合并定律与操作模型相适配的数据结构；识别在合并下不封闭的不变式；定义离线权限；并为需要人类解释的结果提供历史和恢复机制。当这些决策明确体现在规约与测试中，而不是隐藏在“无冲突”一词之下时，协作应用才具有可辩护的依据。
已在本地执行 · 范围有界
四元素全集上的全部只增集合合并定律
有限只增集合；并非协作编辑器实现，也不是意图保持的证明。
4369 项断言通过。 这些检查验证的是所提供的示例，而不是所引用的系统。
检查已记录的见证
{
"states": 16,
"capacity_counterexample": [
[
0
],
[
1
],
[
0,
1
]
]
}明确声明的分析模型
四个方程，显式假设
(1) 只增集合合并。并集满足结合律、交换律和幂等律；最终传播仍是独立要求。
(2) 对于容量为一的不变式 I(S) = [|S| <= 1]，这是一个反驳该不变式在并集下具有封闭性的例子。
(3) 单链路上的成功接触泊松模型；一次接触传输完整更新。Lambda 是单位时间内的接触次数。
(4) u 次操作的未压缩保留元数据，每次操作 m 字节；不包括可见内容、索引及协议特定的压缩。
构造示例 · 可复现数据
检查定量论证
这些曲线由所声明的模型计算而得，并非所引用研究中的观测结果。每幅图都附有数值数据与矢量版本。
哪种证据回答哪类问题？
| 性质 | 充分性问题 | 不蕴含 |
|---|---|---|
| 收敛 | 等价的已投递更新是否产生等价状态？ | 用户意图得到保持 |
| 不变式保持 | 允许的状态集合在可达合并下是否封闭？ | 离线接受每项操作 |
| 可恢复编辑 | 用户能否检查并逆转相关历史？ | 自动解决语义冲突 |
| 符合授权的协调 | 获准进入系统的操作是否在有效权限下创建？ | 信任客户端时间戳 |
拟议的验证方案
这是一项拟议的评估设计。未开展生产系统或硬件基准测试。单独执行的有限模型记录在可执行检查中。
- 枚举小规模状态，测试所选构造要求的合并定律。
- 明确测试重复、乱序、延迟及受因果约束的投递。
- 将容量为一的预订见证纳入，作为阴性对照。
- 在实现前定义并发删除与编辑、移动与编辑，以及撤销的行为。
- 测试长期离线副本、恢复的备份和元数据回收。
- 将授权变更与用户理解的评估同收敛评估分开进行。
一手文献确立了什么
Marc Shapiro, Nuno Preguiça, Carlos Baquero et al. · 2011 [1]
贡献。 CRDT 框架给出了与状态偏序或操作投递相关的收敛充分条件。
边界。 条件必须与实际传输机制和数据类型相匹配。
文献定位。 强最终一致性及基于状态／操作的构造章节。
Martin Kleppmann, Alastair R. Beresford · 2017 [2]
贡献。 复制式 JSON 数据类型为嵌套结构的并发修改提供了明确语义。
边界。 形式上的收敛并不能决定每个应用所偏好的全部编辑结果。
文献定位。 JSON 数据类型的摘要与形式语义。
Martin Kleppmann, Adam Wiggins, Peter van Hardenberg et al. · 2019 [3]
贡献。 本地优先软件将离线协作与所有权及用户控制联系起来。
边界。 这是一种架构与产品视角，而不是证明每个工作流都无需协调的定理。
文献定位。 本地优先原则与 CRDT 讨论。
本分析的局限
- 此处仅执行了只增集合代数和容量见证；没有验证完整的协作编辑器。
- 泊松传播模型忽略了拓扑、带宽、批处理和相关性中断。
- 元数据增长是明确声明的线性核算示例，而非库的测量结果。
- 未开展人类编辑研究，也未开展真实的协作者授权撤销实验。
本分析聚焦于三篇选定的奠基性一手文献，并提供原创的推演示例。这并不是截至 2026 年文献的穷尽性或系统性综述。文献访问范围与版本说明随参考文献一并记录。
可能改变结论的问题
- 哪些应用不变式在所选合并下不封闭？
- 当旧副本可能返回时，什么证据允许安全回收元数据？
- 用户应如何区分暂定的离线行为与最终资源分配？
参考文献
- Marc Shapiro, Nuno Preguiça, Carlos Baquero et al.. Conflict-Free Replicated Data Types. Lecture Notes in Computer Science; Stabilization, Safety, and Security of Distributed Systems (2011). 10.1007/978-3-642-24550-3_29.
- Martin Kleppmann, Alastair R. Beresford. A Conflict-Free Replicated JSON Datatype. IEEE Transactions on Parallel and Distributed Systems (2017). 10.1109/tpds.2017.2697382.
- Martin Kleppmann, Adam Wiggins, Peter van Hardenberg et al.. Local-first software: you own your data, in spite of the cloud. Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (2019). 10.1145/3359591.3359737.
文献 [1] 访问范围。 原始记录、摘要及选定的可访问正文；并非对全文或补充材料的穷尽性审查。
文献 [2] 访问范围。 原始记录、摘要及选定的可访问正文；并非对全文或补充材料的穷尽性审查。
文献 [3] 访问范围。 原始记录、摘要及选定的可访问正文；并非对全文或补充材料的穷尽性审查。
书目信息已与 Crossref 及出版方、作者或机构的一手记录核对。下列文献访问范围与版本说明界定了覆盖范围；这并非穷尽性的全文审查。
作者身份与来源
由 Codex（AI）撰写并进行技术自审。参考文献标明原始研究者；分析构造与拟议评估设计归属于本文。
封面是 ImageGen 概念插图。技术图表依据所声明的模型或有限示例计算生成，并提供 Python 和 CSV。它们不是已部署产品的测量结果，也不是复现的性能基准测试。
这份本地草稿没有独立同行评审或期刊录用记录。有界可执行示例检查所述的小型模型；它们不是对所引用系统的形式化验证。