Armstrong 公理系统深度解析

公理本质：Armstrong 公理系统是关系数据库理论中函数依赖推理的形式化框架，由 William W. Armstrong 于 1974 年提出。它提供了从给定函数依赖集推导出所有逻辑蕴涵依赖的完备规则集，是数据库规范化的数学基础。

---

一、核心概念体系

函数依赖表示法：

• 符号：X → Y
• 语义：属性集 X 唯一决定属性集 Y
• 示例：学号 → 姓名（学号唯一确定姓名）

---

二、Armstrong 基本公理

1. 公理三元组

公理	形式化表达	语义解释	示例
自反律 (Reflexivity)	若 Y ⊆ X，则 X → Y	子集决定自身	{学号,姓名} → {姓名}
增广律 (Augmentation)	若 X → Y，则 XZ → YZ	增加相同属性不影响依赖	学号→姓名 ⇒ {学号,年龄}→{姓名,年龄}
传递律 (Transitivity)	若 X → Y 且 Y → Z，则 X → Z	依赖关系的传递性	学号→班级, 班级→班主任 ⇒ 学号→班主任

---

三、导出推理规则

1. 规则推导体系

2. 规则详解表

规则	形式化表达	推导证明	应用场景
合并规则 (Union)	若 X → Y 且 X → Z，则 X → YZ	增广律+传递律	合并依赖项
分解规则 (Decomposition)	若 X → YZ，则 X → Y 且 X → Z	自反律+传递律	依赖项拆分
伪传递规则 (Pseudotransitivity)	若 X → Y 且 WY → Z，则 XW → Z	增广律+传递律	复杂依赖推导
聚集规则 (Composition)	若 X → Y 且 Z → W，则 XZ → YW	增广律+传递律	多依赖组合

证明伪传递规则：

1. 已知 X → Y
2. 增广律：XW → YW  (在两边添加W)
3. 已知 WY → Z
4. 增广律：YW → Z  (Y和W可交换)
5. 传递律：XW → Z  (由2和4传递)

---

四、属性闭包计算

1. 闭包算法流程

2. 闭包意义矩阵

闭包类型	符号	定义	应用
属性闭包	X⁺	{A | X → A 可由F推导}	求候选键/判断超属性
函数依赖闭包	F⁺	{所有被F逻辑蕴涵的函数依赖}	等价依赖集判断

闭包计算示例：

给定：U = {A,B,C}, F = {A→B, B→C}
求：{A}⁺步骤：
1. closure = {A}
2. A→B ⇒ closure = {A,B}
3. B→C ⇒ closure = {A,B,C}
∴ {A}⁺ = {A,B,C}

---

五、公理系统性质

1. 关键性质证明

2. 数学表示

• 正确性：∀ 推导结果 X → Y ∈ F⁺
• 完备性：∀ X → Y ∈ F⁺, 均可从F出发用Armstrong公理导出
• 最小性：三条公理相互独立，缺一不可

---

总结：

1. 设计启示：

   • 公理系统揭示了数据内在关联的传递本质
   • 闭包计算是模式分解的算法基础（BCNF/3NF分解）
   • 最小覆盖求解可消除冗余依赖

2. 形式化验证：

   • 使用Coq等证明助手可形式化验证Armstrong公理性质
   • 在分布式数据库中扩展为多版本依赖推理

历史意义：Armstrong公理为Codd关系模型提供了严格的数学基础，使数据库设计从经验主义走向形式科学。现代SQL优化器仍依赖其推理引擎实现查询重写优化。