SQL
PostgreSQL

SQLを学びます(9) EXISTS述語について

More than 1 year has passed since last update.

前回の続き。

SQLのEXISTSは要するに$(\emptyset \ne)$のこと。
例えば$\left\{ d\;\mathrm{mgr} : d \in \mathrm{Dep} \right\} \subseteq \left\{ e\;\mathrm{eno} : e \in \mathrm{Emp} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\}$をSQLで表現するには次のように変形すれば良い。

\begin{align}
&\left\{ d\;\mathrm{mgr} : d \in \mathrm{Dep} \right\} \subseteq \left\{ e\;\mathrm{eno} : e \in \mathrm{Emp} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\}
\\
=& \left\{ \subseteq \textrm{の定義} \right\}
\\
&\left\langle \forall m : m \in \left\{ d\;\mathrm{mgr} : d \in \mathrm{Dep} \right\} : m \in \left\{ e\;\mathrm{eno} : e \in \mathrm{Emp} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\} \right\rangle
\\
=& \left\{ \textrm{要素関係} \right\}
\\
&\left\langle \forall m : \left\langle \exists d : d \in \mathrm{Dep} : m = d\;\mathrm{mgr} \right\rangle : m \in \left\{ e\;\mathrm{eno} : e \in \mathrm{Emp} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\} \right\rangle
\\
=& \left\{ \textrm{制限域分割} \right\}
\\
&\left\langle \forall d : d \in \mathrm{Dep} : \left\langle \forall m : m = d\;\mathrm{mgr} : m \in \left\{ e\;\mathrm{eno} : e \in \mathrm{Emp} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\} \right\rangle  \right\rangle
\\
=& \left\{ \textrm{一点規則} \right\}
\\
&\left\langle \forall d : d \in \mathrm{Dep} : d\;\mathrm{mgr} \in \left\{ e\;\mathrm{eno} : e \in \mathrm{Emp} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\} \right\rangle
\\
=& \left\{ \textrm{要素関係} \right\}
\\
&\left\langle \forall d : d \in \mathrm{Dep} : \left\langle \exists e : e \in \mathrm{Emp} : d\;\mathrm{mgr} = e\;\mathrm{eno} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\rangle \right\rangle
\\
=& \left\{ \textrm{De Morgan律} \right\}
\\
&\neg \left\langle \exists d : d \in \mathrm{Dep} : \neg \left\langle \exists e : e \in \mathrm{Emp} : d\;\mathrm{mgr} = e\;\mathrm{eno} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\rangle \right\rangle
\\
=& \left\{ \textrm{要素関係} \right\}
\\
&\neg \left\langle \exists d :: d \in \left\{ d \in \mathrm{Dep} : \neg \left\langle \exists e :: \left\{ e \in \mathrm{Emp} : d\;\mathrm{mgr} = e\;\mathrm{eno} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\} \right\rangle \right\} \right\rangle
\\
=& \left\{ \textrm{空集合の定義} \right\}
\\
&\neg \left( \emptyset \ne \left\{ d \in \mathrm{Dep} : \neg \left(\emptyset \ne \left\{ e \in \mathrm{Emp} : d\;\mathrm{mgr} = e\;\mathrm{eno} \wedge e\;\mathrm{job} \ne \textrm{'PRESIDENT'} \right\} \right)\right\} \right)
\end{align}

そのままSQLの式で書き直せば、

NOT EXISTS (SELECT d.* FROM Dep d
                WHERE NOT EXISTS (SELECT e.* FROM Emp e
                                      WHERE d.mgr = e.eno AND e.job <> 'PRESIDENT'))