Аксіоми Армстронга — множина аксіом (або, точніше, правил висновування), що використовуються для висновування всіх функціональних залежностей у реляційній базі даних. Їх розробив Вільям В. Армстронг[en] у своїй газетній статті 1974 року[1]. Аксіоми правильні в генеруванні тільки функціональних залежностей у замиканні множини функціональних залежностей (позначеному ), коли застосовані до цієї множини (позначеній ). Також вони повні в тому, що повторне застосування цих правил генеруватиме всі функціональні залежності в замиканні .

Формальніше, нехай позначає реляційну схему над множиною атрибутів зі множиною функціональних залежностей . Скажемо, що функціональна залежність логічно слідує з , і позначимо це , якщо й тільки якщо для кожного примірника із , що задовольняє функціональні залежності в , також задовольняє . Позначимо множину всіх функціональних залежностей, які логічно слідують із .

Більше того, з повагою до множини правил висновування , скажемо, що функціональна залежність є похідною з функціональних залежностей у за множиною правил висновування , і позначимо це , якщо й тільки якщо можна отримати шляхом повторного застосування правил висновування в до функціональних залежностей у . Позначимо множину всіх функціональних залежностей, які є похідними від за правилами висновування в .

Тоді множина правил висновування правильна, якщо й тільки якщо має місце наступне:

інакше кажучи, ми не можемо вивести за допомогою функціональні залежності, які логічно не слідують з . Множину правил висновування називають повною, якщо має місце наступне:

простіше кажучи, ми здатні вивести за всі функціональні залежності, які логічно слідують із .

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

ред.

Нехай   — схема відношення над множиною атрибутів  . Надалі позначатимемо літерами  ,  ,   будь-яку підмножину  , а, для стислості, об'єднання двох множин атрибутів   та   як   замість звичайного  ; ця нотація є достатньо стандартною в теорії баз даних[en] при роботі зі множинами атрибутів.

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

ред.

Якщо   — множина атрибутів, а   — підмножина  , то   вміщує  . Тоді   вміщує   [ ] означає, що   функціонально визначає  .

Якщо  , то  .

Аксіома доповнення

ред.

Якщо   вміщує  , а   — множина атрибутів, то   вміщує  . Це означає, що атрибут у залежностях не змінює основних залежностей.

Якщо  , то   для будь-якого  .

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

ред.

Якщо   вміщує  , а   вміщує  , то   вміщує  .

Якщо   та  , то  .

Додаткові (другорядні) правила

ред.

Ці правила можуть виводитися від вищенаведених аксіом.

Декомпозиція

ред.

Якщо  , то   та  .

Доведення

ред.
1.   (Дано)
2.   (Рефлексивність)
3.   (Транзитивність 1 і 2)

Композиція

ред.

Якщо   та  , то  .

Доведення

ред.
1.   (Дано)
2.   (Дано)
3.   (Доповнення 1 і A)
4.   (Декомпозиція 3)
5.   (Доповнення 2 і X)
6.   (Декомпозиція 5)
7.   (Об'єднання 4 і 6)

Об'єднання (нотація)

ред.

Якщо   та  , то  .

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

ред.

Якщо   та  , то  .

Доведення

ред.
1.   (Дано)
2.   (Дано)
3.   (Доповнення 1 і Z)
4.   (Транзитивність 3 і 2)

Самовизначення

ред.

  для будь-якої  . Це слідує прямо з аксіоми рефлексивності.

Екстенсивність

ред.

Наступна властивість є особливим випадком доповнення, коли  .

Якщо  , то  .

Екстенсивність може замінити доповнення як аксіому в сенсі, що доповнення може бути доведене з екстенсивності разом з іншими аксіомами.

Доведення

ред.
1.   (Рефлексивність)
2.   (Дано)
3.   (Транзитивність 1 і 2)
4.   (Екстенсивність 3)
5.   (Рефлексивність)
6.   (Транзитивність 4 і 5)

Відношення Армстронга

ред.

Дано множину функціональних залежностей  , відношення Армстронга — відношення, яке задовольняє всім функціональним залежностям у замиканні   й тільки цим залежностям. На жаль, мінімальний розмір відношення Армстронга для даної множини залежностей може бути експоненційною функцією від кількості атрибутів у залежностях, які розглядаються[2].

Примітки

ред.
  1. Armstrong William Ward. Dependency Structures of Data Base Relationships. — IFIP Congress, 1974. Архівовано з джерела 26 січня 2018.
  2. Beeri, C.; Dowd, M.; Fagin, R.; Statman, R. (1984). On the Structure of Armstrong Relations for Functional Dependencies (PDF). Journal of the ACM. 31: 30—46. CiteSeerX 10.1.1.68.9320. doi:10.1145/2422.322414. Архів оригіналу (PDF) за 12 березня 2006. Процитовано 11 серпня 2020.

Посилання

ред.