Armstrong 公理系统是关系数据库理论中函数依赖逻辑推理的完备且可靠的公理化基础由三条基本公理自反律、增广律、传递律和三条可推导引理合并律、伪传递律、分解律构成。其核心意义在于完备性所有被函数依赖集 $ F $ 逻辑蕴含的依赖 $ X \to Y $均可通过这三条公理有限次推导得出可靠性任何由公理推导出的函数依赖必然被 $ F $ 逻辑蕴含即不会推出错误结论。各规则简要说明与验证要点如下✅自反律Reflexivity本质是平凡依赖——若 $ Y \subseteq X $则 $ X $ 的取值已完全决定 $ Y $无需依赖 $ F $✅增广律Augmentation在依赖两边同时添加相同属性集 $ Z $不破坏决定关系因 $ X \to Y $ 意味着在任意两个元组中$ X $ 相同 ⇒ $ Y $ 相同加 $ Z $ 后$ XZ $ 相同 ⇒ $ X $ 相同 ⇒ $ Y $ 相同 ⇒ $ YZ $ 相同✅传递律Transitivity函数依赖的链式传递类比于等价关系中的传递性✅合并律Union由 $ X \to Y $ 和 $ X \to Z $ 可得 $ X \to YZ $证明中需注意先用增广律得 $ X \to XY $因 $ X \to X $ 自反再增广 $ Y $但更标准证法是① $ X \to Y $已知② $ X \to Z $已知③ $ X \to XZ增广律增广律增广律X \to X $ $ Z $④ $ XZ \to YZ增广律增广律增广律X \to Y $ $ Z $⑤ $ X \to YZ $③④ 传递律✅伪传递律Pseudotransitivity若 $ X \to Y $ 且 $ WY \to Z $则 $ XW \to Z $。证明① $ X \to Y $ ⇒ $ XW \to YW $增广律② $ WY \to Z $即 $ YW \to Z $③ $ XW \to YW $ 且 $ YW \to Z $ ⇒ $ XW \to Z $传递律✅分解律Decomposition由 $ X \to Y $ 和 $ Z \subseteq Y $得 $ X \to Z $。证明① $ Z \subseteq Y $ ⇒ $ Y \to Z $自反律② $ X \to Y $ 且 $ Y \to Z $ ⇒ $ X \to Z $传递律这些规则共同支撑了函数依赖闭包 $ F^ $、属性集闭包 $ X^ $、候选键求解、无损连接分解及BCNF/3NF规范化等核心算法。# 示例计算属性集闭包 X^用于求候选键、验证函数依赖等defcompute_closure(X,F,U):X: 初始属性集字符串或集合F: 函数依赖列表如 [(A, B), (B, C)]X_plusset(X)changedTruewhilechanged:changedFalseforlhs,rhsinF:ifset(lhs).issubset(X_plus)andnotset(rhs).issubset(X_plus):X_plus.update(rhs)changedTruereturnX_plus# 示例调用R(A,B,C), F {A→B, B→C}# compute_closure(A, [(A,B), (B,C)], {A,B,C}) → {A,B,C}判断函数依赖 $ X \to Y $ 是否属于函数依赖集 $ F $ 的逻辑闭包 $ F^ $等价于验证 $ Y \subseteq X^ $其中 $ X^ $ 是属性集 $ X $ 关于 $ F $ 的闭包即在 $ F $ 下所有能被 $ X $ 函数决定的属性组成的集合。✅判定原理充要条件$ X \to Y $ 被 $ F $ 逻辑蕴含即 $ X \to Y \in F^ $⇔ 在所有满足 $ F $ 的关系实例中$ X $ 相同的元组其 $ Y $ 值必相同⇔ $ Y $ 中每个属性都可由 $ X $ 通过 Armstrong 公理从 $ F $ 推出⇔$ Y \subseteq X^ $操作步骤算法级初始化 $ X^ \leftarrow X $重复执行对每个 $ U \to V \in F $若 $ U \subseteq X^ $则将 $ V $ 加入 $ X^ $即 $ X^ \leftarrow X^ \cup V $直至 $ X^ $ 不再变化检查是否 $ Y \subseteq X^ $。若是则 $ X \to Y \in F^ $否则不属于。关键说明该方法正确性由 Armstrong 公理的完备性保证所有 $ F^ $ 中的依赖均可通过闭包计算发现时间复杂度为 $ O(|F| \cdot |U|) $高效实用闭包计算是求候选键、检验无损连接、判断范式如BCNF要求对所有非平凡 $ X \to A \in F^X $ 为超键的基础。# 精简版闭包计算字符串属性如 XABF[(A,B), (B,C)])defclosure(X,F):X_plusset(X)changedTruewhilechanged:changedFalseforlhs,rhsinF:ifset(lhs).issubset(X_plus)andnotset(rhs).issubset(X_plus):X_plus|set(rhs)changedTruereturnX_plus# 示例F [(A,B), (B,C), (C,D)]# 判断 A→D 是否成立→ 计算 closure(A, F) {A,B,C,D} ⊇ {D} → 成立 ✅