阿姆斯特朗公理体系与属性闭包算法：机械化验证函数依赖的两层工具

判断某个函数依赖是否能从已知的函数依赖集合里推导出来，不能靠”感觉 合理”，需要一套可机械执行的推理规则。阿姆斯特朗公理体系给出三条 最基础、不需要证明的推理规则（自反律：子集天然被决定，属于平凡依赖； 增广律：在依赖两端同时添加相同属性，依赖依然成立；传递律：α决定β、 β决定γ，则α决定γ），这三条被证明既有效（推出的每条依赖确实成立） 又完备（所有成立的依赖都能靠反复套用这三条推出），因此是判断函数 依赖蕴涵关系的理论基础。但直接套用这三条基础规则来验证一个具体依赖 往往要绕很多步，于是从这三条基础规则又派生出合并律、分解律、伪 传递律三条更常用的规则，本质是”基础公理的组合快捷方式”，不提供新的 推理能力，只是用得更方便。属性集闭包算法则是把这套理论转化成一个 可以直接跑的算法：从某个属性集α出发，不断用已知函数依赖左部匹配、 右部并入的方式扩张α能决定的属性范围，直到不再增长为止——算出的 闭包如果包含了要验证的目标属性，这个依赖就成立。这个算法的实际价值 在于把”验证一个函数依赖是否被逻辑蕴涵”“判断一个属性集是否是候选码” 这类原本需要枚举所有可能依赖的问题，都转化成一次闭包计算就能完成， 不需要真的把函数依赖集的全部逻辑蕴涵都列出来。