
%%%%%%%%%%%%%%%%%%
\begin{frame}
  \frametitle{Abstract Interpretation Big Picture}

\begin{center}
\includegraphics[height=6cm]{ai-big-idea.png}
\end{center}
\end{frame}

%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Galois Connection}

{\bf Galois connection} (named after \'{E}variste Galois) is defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between partial orders $\leq$ on $C$ and $\sqsubseteq$ on $A$, such that
\begin{equation*}
\forall c, a. \quad  \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*)
\end{equation*}
(intuitively the condition means that $c$ is approximated by $a$).
\vspace{20pt}\\
{\bf Lemma:} The condition $(*)$ holds iff the conjunction of these two conditions:
\begin{eqnarray*}
  c &\leq& \gamma(\alpha(c)) \\
  \alpha(\gamma(a)) &\sqsubseteq& a
\end{eqnarray*}
holds for all $c$ and $a$.
\end{frame}
