查看“︁阿姆斯特朗公理”︁的源代码

{{Refimprove|time=2024-10-17T01:19:15+00:00}}
'''阿姆斯特朗公理系统'''（{{lang_en|Armstrong's axioms}}）是一组用于推导[[关系数据库]]中所有[[函数依赖]]的[[推理规则|规则]]。这一系统由威廉·W·阿姆斯特朗在1974年的论文中首次提出。<ref>William Ward Armstrong: ''[https://web.archive.org/web/20180126091352if_/https://ipfs.io/ipfs/QmWYWTGUZyTm2iRFTZY2pTr2x1vWkDiJr2CBp2PGVpSVSv Dependency Structures of Data Base Relationships]'', page 580-583. IFIP Congress, 1974.</ref> 当应用于函数依赖集（用 <math>F</math> 表示）时，这些规则在生成该集闭包（用 <math>F^{+}</math> 表示）中的函数依赖方面既[[可靠性定理|可靠]]又完备。换言之，反复应用这些规则，我们能够推导出闭包 <math>F^+</math> 中的所有函数依赖，且不会产生不属于该闭包的依赖关系。

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

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

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

:<math>
F^{*}_{A} \subseteq F^{+}
</math>

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

:<math>
F^{+} \subseteq F^{*}_{A}
</math>

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

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

===自反律===
如果<math>X</math>是一个属性集，<math>Y</math>是<math>X</math>的一个子集，那么<math>X</math>函数决定<math>Y</math>（也就是<math>Y</math>函数依赖<math>X</math>），记作<math>X \to Y</math>。

:若<math>Y \subseteq X</math>则<math>X \to Y</math>.

===增广律===
如果<math>X</math>决定<math>Y</math>，那么在<math>X</math>和<math>Y</math>中同时添加任意属性集<math>Z</math>后，这种决定关系仍然成立。这表明，增加新的属性不会改变已有的函数依赖关系。
:若<math>X \to Y</math>，则对任意属性集<math>Z</math>，都有<math>X Z \to Y Z</math>.

===传递律===
函数依赖关系具有传递性。也就是说，如果<math>X</math>决定<math>Y</math>，且<math>Y</math>决定<math>Z</math>，那么<math>X</math>必然也决定<math>Z</math>。
:若<math>X \to Y</math>且<math>Y \to Z</math>，则<math>X \to Z</math>.

==公理的推论==

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

===分解规则===

若<math>X \to Y Z</math>，则<math> X \to Y</math>且<math> X \to Z</math>。
====证明====

{|
|-
| 1. <math>X \to Y Z</math> || （已知）
|-
| 2. <math>Y Z \to Y</math> || （自反性）
|-
| 3. <math>X \to Y</math> || （1和2的传递性）
|}

===合成规则===

若<math>X \to Y</math>且<math>A \to B</math>，则<math> X A \to Y B</math>。

====证明====
{|
|-
| 1. <math>X \to Y</math> || （已知）
|-
| 2. <math>A \to B</math> || （已知）
|-
| 3. <math>X A \to Y A</math> || （1和A的增广性）
|-
| 4. <math>Y A \to Y B</math> || （2和Y的增广性）
|-
| 5. <math>X A \to Y B</math> || （3和4的传递性）
|}

===合并规则===

如果<math>X \to Y</math>且<math>X \to Z</math>，则<math>X \to YZ</math>。

====证明====
{|
| 1. <math>X \to Y</math> || （已知）
|-
| 2. <math>X \to Z</math> || （已知）
|-
| 3. <math>X \to X Z </math> || （2和X的增广性）
|-
| 4. <math>X Z \to Y Z</math> || （1和Z的增广性）
|-
| 5. <math>X \to Y Z</math> || （3和4的传递性）
|}

===伪传递规则===

若<math>X \to Y</math>且<math> Y Z \to W</math>，则<math> X Z\to W</math>。

====证明====

{|
|-
| 1. <math>X \to Y</math> || （已知）
|-
| 2. <math>Y Z \to W</math> || （已知）
|-
| 3. <math>X Z \to Y Z</math> || （1和Z的增广性）
|-
| 4. <math>XZ \to W</math>|| （3和2的传递性）
|}

===自确定性===

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

===扩展规则===

当<math>Z=X</math>时，该属性是增广性的一个特殊情况。
:若<math>X \to Y</math>，则<math>X \to X Y</math>。
在这种意义上，扩展性可以替代增广性作为公理，因为通过扩展性和其他公理可以证明增广性。

====证明====

{|
|-
| 1. <math>X Z \to X</math> || （自反性）
|-
| 2. <math>X \to Y</math> || （已知）
|-
| 3. <math>X Z \to Y</math> || （1和2的传递性）
|-
| 4. <math>X Z \to X Y Z</math> || （3的扩展性）
|-
| 5. <math>X Y Z \to Y Z</math> || （自反性）
|-
| 6. <math>X Z \to Y Z</math> || （4和5的传递性）
|}

==参考文献==
<references/>

==外部链接==
* [http://www.cs.umbc.edu/courses/461/current/burt/lectures/lec14/ UMBC CMSC 461 Spring '99] {{Wayback|url=http://www.cs.umbc.edu/courses/461/current/burt/lectures/lec14/ |date=20110927014000 }}
* [http://www-db.stanford.edu/~ullman/cs345notes/slides01-1.ps CS345 Lecture Notes from Stanford University] {{Wayback|url=http://www-db.stanford.edu/~ullman/cs345notes/slides01-1.ps |date=20060920142140 }}

{{Databases}}
[[Category:数据建模]]