关系演算

查询写出“什么条件算一个答案”，求值器寻找满足条件的元组。学生—教师查询是

$s,t$ 是要交给用户的两个值；$c$ 是内部证据，只要存在一个即可。这个公式的每个成功取值都能追溯到输入行，加入无关对象不能增加证据。

否定本身不是问题。$R(x)\wedge \mathrm{\neg }S(x)$ 从 $R$ 已有成员中排除 $S$ 的成员，等于有限差集。真正需要追问的是：候选对象来自哪里，量词会不会借助表外对象改变真值？

自由变量没有范围 ​

令 $R=\{a\}$，公式 $\mathrm{\neg }R(x)$ 在 $D=\{a\}$ 上没有答案，在 $D^{\prime }=\{a,b\}$ 上返回 $\{b\}$。表没有变化，答案却变化，所以它不是域独立查询。在无限外部论域上，答案还可能无限；把量词限制到活跃域得到空答案，只是换了语义。

只限制输出变量仍然不够 ​

令 $R=S=\{a\}$，考虑

虽然 $x$ 明确来自 $R$，但在 $\{a\}$ 上不存在不属于 $S$ 的 $y$，答案为空；扩张为 $\{a,b\}$ 后可取 $y=b$，答案变成 $\{a\}$。因此检查自由变量有无正关系原子，不能代替检查被量化变量的范围。

一种安全的改写是 $R(x)\wedge \mathrm{\exists }y(T(y)\wedge \mathrm{\neg }S(y))$：现在见证必须来自输入表 $T$，新增未使用的论域元素不起作用。不过这改变了问题，需要业务确实提供候选表 $T$，不能称为对原公式无条件等价的修补。

安全句法、语义安全与空活跃域 ​

文献中的 safe-range 条件是一套可机械检查的充分句法规则；满足规则的查询域独立，但任意域独立公式未必已经写成该规则接受的形式。表达能力定理允许先翻译成安全形式，不能倒过来说只看“每个变量在某处出现”便得到完整判定。析取分支、否定内部与量词作用域都必须纳入规则。

空活跃域特别容易暴露约定差异。没有输入值或常量时，一阶句子 $\mathrm{\exists }x(x=x)$ 在每个非空外部论域上都为真，因而域独立；若机械地把量词范围改成空活跃域，它却为假。零列真答案必须用 $\{()\}$ 保存，不能因“没有可枚举值”而丢掉。

等价翻译的两条方向 ​

关系代数公理库关系代数Relational algebra · Set relational algebra用选择、投影、积、重命名与集合运算组合有限关系查询，并在集合语义下解释连接和存在见证。到演算按表达式结构归纳：连接对应共享变量的合取，投影对应存在量词，并对应析取，差 $E-F$ 对应 ${\phi }_E\wedge \mathrm{\neg }{\phi }_F$。左边 $E$ 已给出有限候选，常量表则翻译为相应等式。每一步都保持列接口和答案。

反方向在 $A\ne \varnothing$ 时，先把所有输入列投影、重命名并求并，再加入查询常量单列表，构造一元关系 $A$。对含 $m$ 个待赋值变量的子公式，$A^m$ 给出候选元组；原子式用选择和连接，否定用相对于 $A^m$ 的差，存在量词用投影。只有当原查询域独立，才可把这一有限求值与原来的外部论域求值等同。

$A=\varnothing$ 时，所有正元输入关系均为空，查询中也没有常量，但零元输入关系仍可能为真。保持这些零元事实不变，先取两个不同的值 $a,b$。域独立性给出

若输出元数 $k>0$，两端分别包含于 $\{a{\}}^k$ 与 $\{b{\}}^k$，而这两个元组集合不相交，因此三个答案都为空。对任意非空论域 $D$，再经共同扩张 $D\cup \{a\}$ 比较，得到

这才说明任意论域上的正元输出都只能为空，包括候选元组含有多个不同坐标值的情形。零元输出则可能为真；可在一个辅助单元素论域上评价句子，按输入零元关系的真假生成相应的有限布尔组合，再用 $\mathbf{1},\mathbf{0}$ 表示。辅助元素只用于翻译证明，不会成为输出常量。以 ${\pi }_{\varnothing }(A)$ 判断非空分支、以 $\mathbf{1}-{\pi }_{\varnothing }(A)$ 判断空分支，可以把两种情况合成一个代数表达式。

这说明等价定理需要的是明确的语义约定，不能把“遍历活跃域”当作适用于所有公式和边界的口号。合取查询公理库合取查询Conjunctive query · CQ · Select-project-join query用关系事实的匹配定义集合答案，并以规范数据库与反向同态判定所有有限实例上的查询包含。提供一个更直接的安全片段：所有使用的变量都通过正关系事实获得见证。在这个片段中，还可以冻结查询变量构造规范数据库，用另一查询是否返回冻结头元组来判定全实例包含；成功赋值解冻后就是反向同态。这一判据依赖正关系原子的结构，不能由演算与代数等价直接推广到任意含否定的公式。

对涉及并发读的应用，还要由事务公理库数据库事务Database transaction · Transaction以 begin 与 commit 或 abort 划定的一次逻辑状态变换，把多项读写作为共同成功或放弃的工作单位。与隔离语义确定本次公式究竟在哪个实例上求值。