分离合取

普通合取 $P\wedge Q$ 像把两句话写在同一张状态照片上，二者可以谈论完全相同的对象。分离合取则要求在照片背后附一张资源清单：哪一片供 $P$ 使用，哪一片供 $Q$ 使用，而且两片能无冲突地拼回总资源。

“分离”描述的是逻辑资源，而不是对象图的几何断开。一个拥有节点 $x$ 的堆片段可以在字段里保存指向另一片段节点 $y$ 的地址；只要两边实际拥有的内存单元不重叠，星号仍可成立。地址值可以复制，解引用权限却由资源归属决定。

链表段正利用这一点递归定义：头节点单元与尾段通过星号分开，头节点保存的 next 值却正是尾段首地址。于是资源边界沿“谁拥有哪个单元”划分，而不是沿“值之间有没有引用”划分；这让局部改写头指针时可以框住整个尾段。

采用 exact points-to：$x\mapsto 7$ 表示恰好拥有地址 $x$ 的一个单元，值为 $7$。断言

要求总堆可拆成两个单元堆，因此强制 $x\ne y$。相反，

不可满足，因为同一地址不能同时出现在两个定义域不交的子堆中。断言 $(x\mapsto 7)\ast \mathsf{true}$ 则表示总资源中可以分出这一个单元，剩余不相交部分无需进一步约束；它是“小脚印加任意 frame”的具体形状。

不能把 exact points-to 下的普通合取机械当作“至少同时含两格”：$x\mapsto 7\wedge y\mapsto 9$ 要求同一个完整堆同时恰好是两个单元堆，只有地址和值相容时才可能成立。某些 intuitionistic 语义把 points-to 解释为向上封闭，读法会不同，文章或工具必须先声明约定。

分数权限进一步改变兼容关系：同一地址的两个只读份额可以组合，只要份额总量不超限且值一致。此时星号的抽象定义不变，变化的是资源代数；把“星号永远意味着地址域不交”推广到所有分离逻辑会错误拒绝合法共享。

分离合取使 frame 推理成立：若命令只消费并恢复 $P$ 描述的资源，额外兼容资源 $R$ 可以在前后同时附加，而不重新分析命令内部。递归谓词用星号把链表头单元与尾段、树根与子树拼合；证明展开时每个子结构都带着明确占有范围。

星号还区分纯事实与空间事实。等式 $x=y$ 不消费资源，通常可在拆分两侧共享；points-to、token 和权限则必须归入某个片段。工具若把所有断言都当可复制纯条件，会允许所有权重复；若把所有等式也当线性资源，又会无谓阻断普通逻辑推理。

在并发场景中，$P\ast Q$ 可把资源初始分给两个线程；资源不变量和消息规则随后有控制地移动这些片段。自动化工具可以做 frame inference 或 bi-abduction，但找到一个语法拆分不等于语义上资源真的兼容，地址等式、纯约束与权限份额仍须联合检查。