阿姆斯特朗公理

阿姆斯特朗公理系统（英語：Armstrong's axioms）是一组用于推导关系数据库中所有函数依赖的规则。这一系统由威廉·W·阿姆斯特朗在1974年的论文中首次提出。 当应用于函数依赖集（用 $F$ 表示）时，这些规则在生成该集闭包（用 $F^{+}$ 表示）中的函数依赖方面既可靠又完备。换言之，反复应用这些规则，我们能够推导出闭包 $F^{+}$ 中的所有函数依赖，且不会产生不属于该闭包的依赖关系。

让我们用更严谨的方式来描述这个概念。假设 $\langle R(U),F\rangle$ 代表一个关系模式，其中 $U$ 是属性集，$F$ 是函数依赖集。如果所有满足 $F$ 中函数依赖的，$R$ 的实例 $r$，也都同时满足函数依赖 $f$，那么我们就说 $f$ 被 $F$ 逻辑蕴含，记作 $F\models f$。我们用 $F^{+}$ 来表示所有被 $F$ 逻辑蕴含的函数依赖的集合。

再来看推理规则集 $A$ 的作用。如果我们能够通过反复运用 $A$ 中的规则，从 $F$ 中推导出函数依赖 $f$，我们就说 $f$ 可由 $F$ 通过 $A$ 所推导，记作 $F\vdash _{A}f$。我们用 $F_{A}^{*}$ 表示所有可以通过 $A$ 从 $F$ 推导出的函数依赖的集合。

那么，当且仅当以下条件成立时，推理规则集 $A$ 是可靠的：

$F_{A}^{*}\subseteq F^{+}$

也就是说，使用 $A$ 推导出的函数依赖不能超出由 $F$ 逻辑蕴含的函数依赖范围。 推理规则集 $A$ 的完备性当且仅当以下条件成立：

$F^{+}\subseteq F_{A}^{*}$

更简单地说，推理规则集 $A$ 能够推导出所有由 $F$ 逻辑蕴含的函数依赖。

公理（基本规则）

设$R(U)$是定义在属性集$U$上的关系模式。在接下来的讨论中，我们将用$X$、$Y$、$Z$表示$U$的任意子集。为了简洁，我们用$XY$代替常规的$X\cup Y$来表示两个属性集$X$和$Y$的并集。这种记法在处理資料庫理論中的属性集合时是相当常见的。

自反律

如果$X$是一个属性集，$Y$是$X$的一个子集，那么$X$函数决定$Y$（也就是$Y$函数依赖$X$），记作$X\to Y$。

若$Y\subseteq X$则$X\to Y$.

增广律

如果$X$决定$Y$，那么在$X$和$Y$中同时添加任意属性集$Z$后，这种决定关系仍然成立。这表明，增加新的属性不会改变已有的函数依赖关系。

若$X\to Y$，则对任意属性集$Z$，都有$XZ\to YZ$.

传递律

函数依赖关系具有传递性。也就是说，如果$X$决定$Y$，且$Y$决定$Z$，那么$X$必然也决定$Z$。

若$X\to Y$且$Y\to Z$，则$X\to Z$.

公理的推论

这些推论可以从上述公理中推导出来。

分解规则

若$X\to YZ$，则$X\to Y$且$X\to Z$。

证明

1. $X\to YZ$	（已知）
2. $YZ\to Y$	（自反性）
3. $X\to Y$	（1和2的传递性）

合成规则

若$X\to Y$且$A\to B$，则$XA\to YB$。

证明

1. $X\to Y$	（已知）
2. $A\to B$	（已知）
3. $XA\to YA$	（1和A的增广性）
4. $YA\to YB$	（2和Y的增广性）
5. $XA\to YB$	（3和4的传递性）

合并规则

如果$X\to Y$且$X\to Z$，则$X\to YZ$。

证明

1. $X\to Y$	（已知）
2. $X\to Z$	（已知）
3. $X\to XZ$	（2和X的增广性）
4. $XZ\to YZ$	（1和Z的增广性）
5. $X\to YZ$	（3和4的传递性）

伪传递规则

若$X\to Y$且$YZ\to W$，则$XZ\to W$。

证明

1. $X\to Y$	（已知）
2. $YZ\to W$	（已知）
3. $XZ\to YZ$	（1和Z的增广性）
4. $XZ\to W$	（3和2的传递性）

自确定性

对于任意$I$，$I\to I$。这直接由自反性公理得到。

扩展规则

当$Z=X$时，该属性是增广性的一个特殊情况。

若$X\to Y$，则$X\to XY$。

在这种意义上，扩展性可以替代增广性作为公理，因为通过扩展性和其他公理可以证明增广性。

证明

1. $XZ\to X$	（自反性）
2. $X\to Y$	（已知）
3. $XZ\to Y$	（1和2的传递性）
4. $XZ\to XYZ$	（3的扩展性）
5. $XYZ\to YZ$	（自反性）
6. $XZ\to YZ$	（4和5的传递性）

外部链接

• UMBC CMSC 461 Spring '99
• CS345 Lecture Notes from Stanford University