阿姆斯特朗公理

阿姆斯特朗公理系統（英語：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