%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Termination and Efficiency of Abstract Interpretation Analysis}

{\bf Definition:} A {\bf chain} of length $n$ is a sequence $s_0, s_1, \ldots, s_n$ such that
\[
    s_0 \sqsubset s_1 \sqsubset s_2 \sqsubset \ldots \sqsubset s_n
\]
where $x \sqsubset y$ means, as usual, $x \sqsubseteq y \land x \neq y$
\vspace{20pt}\\
{\bf Definition:} A partial order has a {\bf finite height} $n$ if it has a chain of length $n$ and every chain is of length at most $n$.
\vspace{20pt}\\
A finite lattice is of finite height.

\end{frame}

%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example}
The constant propagation lattice $\mathbb{Z} \cup \{\bot, \top\}$ is an infinite lattice of \\
height 2.  One example chain of length 2 is 
\[
   \bot \sqsubset 42 \sqsubset \top
\]
Here the $\gamma$ function is given by 
\begin{itemize}
 \item $\gamma(k) = \ldots$ when $k \in \mathbb{Z}$
  \item $\gamma(\top) = \ldots$
  \item $\gamma(\bot) = \ldots$
\end{itemize}
The ordering is given by $a_1 \subseteq a_2$ iff $\gamma(a_1) \subseteq \gamma(a_2)$

\end{frame}

%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Example}
If a state of a (one-variable) program is given by an integer, then a concrete lattice element is a set of integers.  This lattice has infinite height.  There is a chain
\[
   \{ 0 \} \subset \{ 0, 1 \} \subset \{ 0, 1, 2 \}  \subset \ldots \subset \{ 0, 1, 2, \ldots, n \}
\]
for every $n$.

\end{frame}

%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Convergence in Lattices of Finite Heignth}

Consider a finite-height lattice $(L, \sqsubseteq)$ of height $n$ and function 
\[
  F : L \to L
\]

What is the maximum length of sequence $\bot, F(\bot), F^2(\bot), \ldots$ ?

Give an effectively computable expression for $lfp(F)$.
\end{frame}

%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Computing the Height when Combining Lattices}

Let $H(L,\leq)$ denote the height of the lattice $(L,\leq)$.

{\bf Product}\\
Given lattices $(L_1,\sqsubseteq_1)$ and $(L_2,\sqsubseteq_2)$, consider product lattice with set $L_1 \times L_2$ and potwise order
\[
    (x_1,x_2) \sqsubseteq (x'_1, x'_2)
\]
iff $\ldots$

What is the height of the product lattice?

{\bf Exponent}\\

Given lattice $(L, \sqsubseteq)$ and set $V$, consider the lattice $(L^V,\sqsubseteq')$ defined by
\[
    g \sqsubset' h
\]
iff $\forall v \in V. g(v) \sqsubseteq h(v)$.

What is the height of the exponent lattice?

\pause
Answer: height of $L$ times the cardinality of $V$.
\end{frame}

