状态型 CRDT 的并半格

把 $x⊑y$ 读作“$y$ 至少包含 $x$ 已知的全部信息”。合并不是在两个冲突版本中任意选赢家，而是寻找同时覆盖二者、又不添加无根据内容的最小状态。副本沿不同网络路径收到同一批信息，最终都落在这些信息的 join；消息树怎样分叉、重传和重组不再影响结果。

“向上”是由信息语义决定的，不必等同数值变大。集合删除可以通过增加“某个 add 已被删除”的因果证据实现；寄存器覆盖也可通过增加带新 dot 的版本并记录旧 dot 已见来实现。若直接从集合里拿掉元素而不保留证据，偏序信息会倒退，旧状态稍后到达便可能把元素复活。

半格只解决确定合并。它没有规定本地更新一定向上，也没有保证每份信息最终传播，更没有规定读操作的业务含义；这三项分别由膨胀更新、传播协议和 query 函数承担。

取状态空间 ${\mathbb{N}}^2$，偏序与 join 都逐分量定义：

三个副本状态分别为 $x=(2,0)$、$y=(1,3)$、$z=(2,1)$。先合并 $x,y$ 得 $(2,3)$，再合并 $z$ 仍为 $(2,3)$；先合并 $y,z$ 也得 $(2,3)$，重复加入 $x$ 不变。这个计算同时见证结合、交换与幂等，并构成 G-Counter 的两副本状态空间。

若误把 merge 定为逐分量加法，则 $(2,0)$ 与自身重传一次会从 $(2,0)$ 变成 $(4,0)$，幂等性失败。若 merge 取“收到的右参数”，结果又随消息顺序变化。若状态是普通整数而 merge 取最大值，本地允许从 $5$ 更新成 $3$，稍后与旧状态 $5$ 合并会恢复成 $5$；算法仍收敛，却没有实现用户以为的覆盖语义。

全格比本页要求更强：meet 是否存在与状态合并无关。相反，只有某些状态对拥有上界也不够；并发可达的任意两状态都必须能合并，否则分区期间合法产生的版本可能在愈合时无定义。

并半格为状态压缩提供明确责任：压缩函数若保持相同的抽象信息顺序与 join 结果，便可更换表示；若丢掉删除证据或把不同点误合并，就会破坏收敛或语义。产品半格、映射半格与带因果上下文的 powerset 半格分别支撑计数器、按键对象和 observed-remove 集合。

该代数还让测试超越几组网络轨迹。对有限生成状态可做 property-based testing，随机验证 join 的三条定律与 query 在等价状态上的一致性；但有限测试不能替代对无界 dot、整数溢出和回收协议的证明。