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

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

\begin{frame}
\frametitle{Abstract Domains are Partial Orders}

Program semantics is given by certain sets
(e.g. sets of reachable states).
\begin{itemize}
\item subset relation $\subseteq$: used to compare sets
\item union of states: used to combine sets coming from different executions
(e.g. if statement)
\end{itemize}
Our goal is to approximate such sets. We introduce a domain of elements $d \in D$
where each $d$ represents a set.
\begin{itemize}
\item $\gamma(d)$ is a set of states. $\gamma$ is called \textbf{concretization function}
\item given $d_1$ and $d_2$, it could happen that there is \textbf{no element} $d$ representing union
\[
   \gamma(d_1) \cup \gamma(d_2) = \gamma(d)
\]
Instead, we use a set $d$ that approximates union, and denote it $d_1 \sqcup d_2$
\end{itemize}

This leads us to review the theory of \textbf{partial orders} and \textbf{(semi)lattices}.
\end{frame}


%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Partial Orders}
\small
{\bf Partial ordering relation} is a binary relation $\leq$ that is reflexive, antisymmetric, 
and transitive, that is, the following properties hold for all $x,y,z$:
\begin{itemize}
\item $x \leq x$ \ (reflexivity)
\item $x \leq y \land y \leq x \rightarrow x=y$ \ (antisymmetry)
\item $x \leq y \land y \leq z \rightarrow x \leq z$ \ (transitivity)
\end{itemize}

If $A$ is a set and $\le$ a binary relation on $A$, we call the pair $(A,\le)$ a {\bf partial order}.
\vspace{10pt}\\
Given a partial ordering relation $\le$, the corresponding {\bf strict ordering relation} 
$x < y$ is defined by $x \le y \land x \neq y$ and can be viewed as a shorthand for 
this conjunction.
%\vspace{10pt}\\
%We can view the partial order $(A,r)$ as a first-order interpretation $I=(A,\alpha)$ of 
%language ${\cal L}=\{\le\}$ where $\alpha({\le})=r$.
\begin{itemize}
\item Orders on integers, rationals, reals are all special cases of partial orders called
 {\em linear orders}.

\item Given a set $U$, let $A$ be any set of subsets of $U$, that is $A \subseteq 2^U$.  Then $(A,\subseteq)$ is a partial order.
%$\vspace{20pt}\\
\end{itemize}
{\bf Example:} Let $U = \{ 1,2,3\}$ and let $A = \{ \emptyset, \{1\}, \{2\}, \{3\}, \{2,3\} , \{1,2,3\}\}$.  
Then $(A, \subseteq)$ is a partial order.  We can draw it as a {\em Hasse diagram}.
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Hasse diagram}
presents the relation as a directed graph in a plane, such that
\begin{itemize}
\item the direction of edge is given by which nodes is drawn above
\item transitive and reflexive edges are not represented (they can be derived)
\end{itemize}
\begin{figure}
  \centering
\includegraphics[height=6cm]{hasse1.pdf}
\end{figure}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Extreme Elements in Partial Orders}
\small
Given a partial order $(A,\le)$ and a set $S \subseteq A$, we call an element $a \in A$
\begin{itemize}
\setlength{\itemindent}{-1em}
 \item {\bf upper bound} of $S$ if for all $a' \in S$ we have $a' \le a$
 \item {\bf lower bound} of $S$ if for all $a' \in S$ we have $a \le a'$
 \item {\bf minimal element} of $S$ if $a \in S$ and there is no element $a' \in S$ such that $a' < a$
 \item {\bf maximal element} of $S$ if $a \in S$ and there is no element $a' \in S$ such that $a < a'$
 \item {\bf greatest element} of $S$ if $a \in S$ and for all $a' \in S$ we have $a' \le a$
 \item {\bf least element} of $S$ if $a \in S$ and for all $a' \in S$ we have $a \le a'$
 \item {\bf least upper bound} (lub, supremum, join, $\sqcup$) of $S$ if $a$ is the least element in the set of all upper bounds of $S$
 \item {\bf greatest lower bound} (glb, infimum, meet, $\sqcap$) of $S$ if $a$ is the greatest element in the set of all lower bounds of $S$
\end{itemize}
Taking $S=A$ we obtain minimal, maximal, greatest, least elements for the entire partial order.

\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Extreme Elements in Partial Orders}

Notes
\begin{itemize}
 \item minimal element need not exist: $(0,1)$ interval of rationals
  \item there may be multiple minimal elements: $\{\{a\},\{b\},\{a,b\}\}$
  \item if minimal element exists, it need not be least: above example
  \item there are no two distinct least elements for the same set
  \item least element is always glb and minimal
  \item if glb belongs to the set, then it is always least and minimal
  \item on a family of relations closed under $\cap$ and $\cup$,  $glb$ is $\cap$ and $lub$ is $\cup$ for the partial order $\subseteq$;
not all families of sets are closed; these are:
    \begin{itemize}
    \item the set of all subsets
    \item the family of open sets from topology
    \end{itemize}
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Least upper bound (lub, supremum, join, $\sqcup$)}
Denoted $lub(S)$, least upper bound of $S$ is an element $M$, if it exists, such that $M$ is the 
least element of the set
$$
U = \{x \;|\; x \text{ is upper bound on } S\}
$$

In other words:
\begin{itemize}
\item $M$ is an upper bound on $S$
\item for every other upper bound $M'$ on $S$, we have that $M \le M'$
\end{itemize}

Note: this is the same definition as supremum in real analysis.
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Least upper bound (glb, infimum, meet, $\sqcap$)}

$a_1 \sqcup a_2$ denotes $lub(\{a_1, a_2\})$
\vspace{20pt}\\
$$
(\dots (a_1 \sqcup a_2)\dots) \sqcup a_n  \quad \text{ is in fact } lub(\{a_1, \dots, a_n\})
$$
\vspace{20pt}\\
So the operation is
\begin{itemize}
\item associative
\item commutative
\item idempotent
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Real Analysis}
Take as $S$ the open interval of reals $(0, 1) = \{x \;|\; 0 < x < 1\}$ 

Then
\begin{itemize}
\item $S$ has no maximal element
\item $S$ thus has no greatest element
\item 2, 2.5, 3,... are all upper bounds on $S$
\item $lub(S) = 1$
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Execise: subsets of $U$}
Consider 
$$
A = 2^U = \{S \;|\; S \subseteq U\} \quad \quad \text{ and } \quad  (A, \subseteq)
$$
\vspace{20pt}

Do these exist, and if so, what are they?
\begin{itemize}
\item $s_1 \subseteq S, s_2 \subseteq S, lub(\{s_1, s_2\}) = ?$
\item $lub(S) = ?$
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Partial order for the domain of intervals}
{\bf Domain:} $D = \{\bot\} \cup \{ (L, U) \;|\; L \in \{-\infty\} \cup \mathbb{Z}, U \in \{+ \infty\}\cup\mathbb{Z} \}
$\\
such that $L \le U$.
\vspace{10pt}\\
The associated set of elements is given by the function $\gamma$:
$$
\gamma : D \to 2^\mathbb{Z}, \quad \quad \gamma((L, U)) = \{x\;|\; L \le x \wedge x \le U\}
$$
{\bf Lub: } for $d_1, d_2 \in D$, 
$d_1 \sqsubseteq d_2 \quad \leftrightarrow \quad \gamma(d_1) \subseteq \gamma(d_2)$\\
hence
\begin{align*}
(L_1, U_1) \sqsubseteq (L_2, U_2) \quad &\leftrightarrow \quad L_2 \le L_1 \wedge U_1 \le U_2\\
\bot \sqsubseteq d& \quad \forall d \in D\\
 (L_1, U_1) \sqcup (L_2, U_2) &= (min(L_1, L_2), max(U_1, U_2))
\end{align*}
\end{frame}

\begin{frame}
\frametitle{Remark on constructing orders using inverse images}

Suppose $\gamma : D \to C$ where $C$ is some collection of sets.

If we define relation $\sqsubseteq$ by:
\[
    d_1 \sqsubseteq d_2 \ \iff \ \gamma(d_1) \subseteq \gamma(d_2)
\]
then
\begin{enumerate}
\item $\sqsubseteq$ is reflexive
\item $\sqsubseteq$ is transitive
\item $\sqsubseteq$ is antisymmetric if and only iff $\gamma$ is injective
\end{enumerate}
If $\sqsubseteq$ is not antisymmetric then we can define equivalence relation
\[
    d_1 \sim d_2   \ \iff \ \gamma(d_1) = \gamma(d_2)
\]
and then take $D'$ to be equivalence classes of such new set.

Example: suppose we defined intervals as all possible pairs of integers $(L,U)$. Then
there would be many representations of the empty set, all those intervals where $L > U$.
\end{frame}

\begin{frame}
\frametitle{Example: Assignments that Make Propositional Formulas True}

Let $A$ be the set of all propositional formulas containing only variables $p,q$.  For a formula $F \in A$ define
\[
   [F] = \{ (u,v).\ u,v \in \{0,1\} \land F \mbox{ is true for } p\mapsto u, q \mapsto v \}
\]
i.e. $[F]$ denotes the set of assignments for which $F$ is true. Note that $F \implies G$ is a tautology iff $[F] \subseteq [G]$. Define ordering on formulas $A$ by
\[
    F \le G  \iff [F] \subseteq [G]
\]
Is $\le$ a partial order? Which laws does $\le$ satisfy?

\

Remark: you can generalize this question to Lindenbaum–Tarski algebra.

\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Lattices}

{\bf Definition:} A lattice is a partial order in which every two-element set has a least upper bound and a greatest lower bound.
\vspace{10pt}\\
{\small
{\bf Lemma:} In a lattice every non-empty finite set has a lub ($\sqcup$) and glb ($\sqcap$).
\pause
\vspace{10pt}\\
{\bf Proof:} is by induction!\\
Case where the set S has three elements x,y and z:\\
Let $a=(x \sqcup y) \sqcup z$. \\ By definition of $\sqcup$ we have $z \sqsubseteq a$ and $ x \sqcup y \sqsubseteq a $.\\
Then we have again by definition of $\sqcup$, $x \sqsubseteq x \sqcup y$ and $y \sqsubseteq x \sqcup y$. Thus by transitivity we have $x \sqsubseteq a$ and $y \sqsubseteq a$.\\
Thus we have $S \sqsubseteq a$ and a is an upper bound.\\
Now suppose that there exists $a^\prime$ such that $S \sqsubseteq a^\prime$. We want $a \sqsubseteq a^\prime$ (a least upper bound):\\
We have $x \sqsubseteq a^\prime $ and $y \sqsubseteq a^\prime $, thus $x \sqcup y \sqsubseteq a^\prime$. But $z \sqsubseteq a^\prime $, thus $((x \sqcup y) \sqcup z) \sqsubseteq a^\prime $.\\
Thus $a$ is the lub of our 3 elements set.
}
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Examples of Lattices}

{\bf Lemma:} Every linear order is a lattice.
\vspace{10pt}\\
{\bf Example:} Every bounded subset of the set of real numbers has a lub.  This is an axiom of real numbers, the way they are defined (or constructed from rationals).

\begin{itemize}
\item If a lattice has least and greatest element, then every finite set (including empty set) has a lub and glb.
\item This does not imply there are lub and glb for infinite sets. \\
{\bf Example:} In the oder $([0,1),\le)$ with standard ordering on reals is a lattice, the entire set has no lub.
The set of all rationals of interval $[0,10]$ is a lattice, but the set $\{ x \mid 0 \le x \land x^2 < 2 \}$ has no lub.
\end{itemize}

\end{frame}
