Una FD è un vincolo tra due insiemi di attributi del database
Supponiamo che lo schema di db relazionale abbia $n$ attributi $A_1,..,A_n$ e che l’intero database sia descritto da uno schema di relazione universale $R= \{A_1,..,A_n\}$
Una dipendenza funzionale, denotata da $X \to Y$, tra due insiemi di attributi $X$ e $Y$ che sono sottoinsiemi di $R$, specifica un vincolo sulle possibili tuple che possono formare un’istanza di relazione $r$ di $R$
<aside> <img src="/icons/report_purple.svg" alt="/icons/report_purple.svg" width="40px" />
Il vincolo stabilisce che se $X \to Y$, allora $\forall t_1,t_2 \in r$ tali che $t_1[X] = t_2[X]$ deve valere $t_1[Y] = t_2[Y]$
</aside>
Ciò significa che i valori della componente $Y$ di una tupla di $r$ dipendono dai valori della componente $X$, o alternativamente i valori della componente $X$ di una tupla determinano univocamente i valori della componente $Y$
Se un vincolo su $R$ stabilisce che non può esistere più di una tupla con un dato valore per $X$ in ogni istanza di relazione $r(R)$, cioè $X$ è una chiave candidata di $R$, ciò implica che $X \to Y$ per ogni sottoinsieme $Y$ di attributi di $R$
Il fatto che $X \to Y$ in $R$ non implica nulla circa $Y \to X$ in $R$
Una FD è una proprietà dello schema di relazione (intenzione) $R$ e non di un particolare stato di relazione (estensione $r$ di $R$)
Una FD non può essere inferita automaticamente da un’estensione di relazione $r$, ma deve essere definita esplicitamente da chi conosce la semantica degli attributi
Sia $F$ l’insieme delle dipendenze funzionali di uno schema di relazione $R$, il progettista dello schema specifica le dipendenze funzionali semanticamente ovvie $F$
In tutte le istanze di relazione legali però valgono numerose altre dipendenze funzionali → queste possono essere inferite da $F$
L’insieme di tali dipendenze è detto chiusura di $F$ ed è denotato da $F^+$
Una FD $X \to Y$ è inferita da un insieme di dipendenze $F$ su $R$ se $X \to Y$ vale in ogni stato di relazione $r$ che è estensione legale di $R$
<aside> <img src="/icons/exclamation-mark_purple.svg" alt="/icons/exclamation-mark_purple.svg" width="40px" /> $F \models X\to Y$ denota che la FD $X\to Y$ è inferita da F
</aside>