Аксиомы Армстронга

Аксиомы Армстронга — это набор аксиом (или, точнее, правил вывода ), используемых для вывода всех функциональных зависимостей в реляционной базе данных . Они были разработаны Уильямом У. Армстронгом в его статье 1974 года. ^[1] Аксиомы являются обоснованными в создании только функциональных зависимостей в замыкании набора функциональных зависимостей (обозначаемого как ) при применении к этому набору (обозначаемому как ). Они также являются полными в том, что повторное применение этих правил будет генерировать все функциональные зависимости в замыкании . ${\displaystyle F^{+}}$ ${\displaystyle F}$ ${\displaystyle F^{+}}$

Более формально, пусть обозначает реляционную схему над набором атрибутов с набором функциональных зависимостей . Мы говорим, что функциональная зависимость логически подразумевается , и обозначаем ее тогда и только тогда, когда для каждого экземпляра , который удовлетворяет функциональным зависимостям в , также удовлетворяет . Мы обозначаем набор всех функциональных зависимостей, которые логически подразумеваются . ${\displaystyle \langle R(U),F\rangle }$ ${\displaystyle U}$ ${\displaystyle F}$ ${\displaystyle f}$ ${\displaystyle F}$ ${\displaystyle F\models f}$ ${\displaystyle r}$ ${\displaystyle R}$ ${\displaystyle F}$ ${\displaystyle r}$ ${\displaystyle f}$ ${\displaystyle F^{+}}$ ${\displaystyle F}$

Кроме того, относительно набора правил вывода мы говорим, что функциональная зависимость выводима из функциональных зависимостей в с помощью набора правил вывода , и мы обозначаем ее через тогда и только тогда, когда она получается посредством многократного применения правил вывода в к функциональным зависимостям в . Мы обозначаем через набор всех функциональных зависимостей, которые выводимы из с помощью правил вывода в . ${\displaystyle A}$ ${\displaystyle f}$ ${\displaystyle F}$ ${\displaystyle A}$ ${\displaystyle F\vdash _{A}f}$ ${\displaystyle f}$ ${\displaystyle A}$ ${\displaystyle F}$ ${\displaystyle F_{A}^{*}}$ ${\displaystyle F}$ ${\displaystyle A}$

Тогда набор правил вывода является обоснованным тогда и только тогда, когда выполняется следующее: ${\displaystyle A}$

${\displaystyle F_{A}^{*}\subseteq F^{+}}$

то есть, мы не можем вывести посредством функциональных зависимостей, которые логически не подразумеваются из . Набор правил вывода считается полным, если выполняется следующее: ${\displaystyle A}$ ${\displaystyle F}$ ${\displaystyle A}$

${\displaystyle F^{+}\subseteq F_{A}^{*}}$

Проще говоря, мы можем вывести все функциональные зависимости, которые логически подразумеваются . ${\displaystyle A}$ ${\displaystyle F}$

Аксиомы (основные правила)

Пусть будет схемой отношений над набором атрибутов . В дальнейшем мы будем обозначать буквами , , любое подмножество и, для краткости, объединение двух наборов атрибутов и вместо обычного ; эта нотация довольно стандартна в теории баз данных при работе с наборами атрибутов. ${\displaystyle R(U)}$ ${\displaystyle U}$ ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle Z}$ ${\displaystyle U}$ ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle XY}$ ${\displaystyle X\cup Y}$

Аксиома рефлексивности

Если — набор атрибутов и — подмножество , то выполняется . При этом выполняется [ ] означает, что функционально определяет . ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle X\to Y}$ ${\displaystyle X}$ ${\displaystyle Y}$

Если тогда . ${\displaystyle Y\subseteq X}$ ${\displaystyle X\to Y}$

Аксиома приращения

Если удерживает и является набором атрибутов, то удерживает . Это означает, что атрибут в зависимостях не изменяет базовые зависимости. ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle Z}$ ${\displaystyle XZ}$ ${\displaystyle YZ}$

Если , то для любого . ${\displaystyle X\to Y}$ ${\displaystyle XZ\to YZ}$ ${\displaystyle Z}$

Аксиома транзитивности

Если держится и держится , то держится . ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle Y}$ ${\displaystyle Z}$ ${\displaystyle X}$ ${\displaystyle Z}$

Если и , то . ${\displaystyle X\to Y}$ ${\displaystyle Y\to Z}$ ${\displaystyle X\to Z}$

Дополнительные правила (Вторичные правила)

Эти правила можно вывести из приведенных выше аксиом.

Разложение

Если то и . ${\displaystyle X\to YZ}$ ${\displaystyle X\to Y}$ ${\displaystyle X\to Z}$

Доказательство

Состав

Если и тогда . ${\displaystyle X\to Y}$ ${\displaystyle A\to B}$ ${\displaystyle XA\to YB}$

Доказательство

Союз

Если и тогда . ${\displaystyle X\to Y}$ ${\displaystyle X\to Z}$ ${\displaystyle X\to YZ}$

Доказательство

Псевдотранзитивность

Если и тогда . ${\displaystyle X\to Y}$ ${\displaystyle YZ\to W}$ ${\displaystyle XZ\to W}$

Доказательство

Самоопределение

${\displaystyle I\to I}$для любого . Это следует непосредственно из аксиомы рефлексивности. ${\displaystyle I}$

Экстенсивность

Следующее свойство является частным случаем аугментации, когда . ${\displaystyle Z=X}$

Если , то . ${\displaystyle X\to Y}$ ${\displaystyle X\to XY}$

Экстенсивность может заменить аугментацию как аксиома в том смысле, что аугментация может быть доказана из экстенсивности вместе с другими аксиомами.

Доказательство

отношение Армстронга

При заданном наборе функциональных зависимостей отношение Армстронга — это отношение, которое удовлетворяет всем функциональным зависимостям в замыкании и только этим зависимостям. К сожалению, отношение Армстронга минимального размера для заданного набора зависимостей может иметь размер, который является экспоненциальной функцией числа атрибутов в рассматриваемых зависимостях. ^[2] ${\displaystyle F}$ ${\displaystyle F^{+}}$

Ссылки

1. Уильям Уорд Армстронг: Структуры зависимостей в связях баз данных , стр. 580-583. Конгресс IFIP, 1974.
2. Бири, К.; Дауд, М.; Фагин, Р.; Статман, Р. (1984). «О структуре отношений Армстронга для функциональных зависимостей» (PDF) . Журнал ACM . 31 : 30–46. CiteSeerX  10.1.1.68.9320 . doi :10.1145/2422.322414. Архивировано из оригинала (PDF) 2018-07-23.

Внешние ссылки

• UMBC CMSC 461 Весна '99
• Конспект лекций CS345 из Стэнфордского университета