%%%%%%%%%%%%%%%%%%
\begin{frame}

Let $G$ be a monotonic function on a lattice.  Let $a_0 = \bot$ and $a_{n+1}=G(a_n)$.  We obtain a sequence $\bot \sqsubseteq G(\bot) \sqsubseteq G^2(\bot) \sqsubseteq \cdots$.  Let $a_* = \bigsqcup_{n \ge 0} a_n$.
\vspace{20pt}\\
{\bf Lemma:} The value $a_*$ is a prefix point.

Observation: $a_*$ need not be a fixpoint (e.g. on lattice [0,1] of real numbers).
\end{frame}


%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Omega continuity}
{\bf Definition:} A function $G$ is $\omega$-continuous if for every chain $x_0 \sqsubseteq x_1 \sqsubseteq \ldots \sqsubseteq x_n \sqsubseteq \ldots$ we have
\begin{equation*}
  G(\bigsqcup_{i \ge 0} x_i) = \bigsqcup_{i \ge 0} G(x_i)
\end{equation*}
\vspace{20pt}\\
{\bf Lemma:} For an $\omega$-continuous function $G$, the value $a_* = \bigsqcup_{n \ge 0} G^n(\bot)$ is the least fixpoint of $G$.\\
\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Iterating sequences and omega continuity}
\small
{\bf Lemma:} For an $\omega$-continuous function $G$, the value $a_* = \bigsqcup_{n \ge 0} G^n(\bot)$ is the least fixpoint of $G$.
\vspace{10pt}\\
{\bf Proof:}\\
\begin{itemize}
\item By definition of $\omega$-continuous we have $G(\bigsqcup_{n \ge 0} G^n(\bot)) = \bigsqcup_{n \ge 0} G^{n+1}(\bot)=\bigsqcup_{n \ge 1} G^n(\bot)$.
\item But $\bigsqcup_{n \ge 0} G^n(\bot) = \bigsqcup_{n \ge 1} G^n(\bot) \sqcup \bot = \bigsqcup_{n \ge 1} G^n(\bot)$ because $\bot$ is the least element of the lattice.
\item
Thus $G(\bigsqcup_{n \ge 0} G^n(\bot)) = \bigsqcup_{n \ge 0} G^n(\bot)$ and $a_*$ is a fixpoint.
\end{itemize}
Now let's prove it is the least.
Let $c$ be such that $G(c)=c$. We want $\bigsqcup_{n \ge 0} G^n(\bot) \sqsubseteq c$. This is equivalent to $\forall n \in \mathbb N . G^n(\bot) \sqsubseteq c$.\\
We can prove this by induction : $\bot \sqsubseteq c$ and if $G^n(\bot) \sqsubseteq c$, then by monotonicity of $G$ and by definition of $c$ we have $G^{n+1}(\bot) \sqsubseteq G(c) \sqsubseteq c$.
\end{frame}


%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Iterating sequences and omega continuity}

{\bf Lemma:} For an $\omega$-continuous function $G$, the value $a_* = \bigsqcup_{n \ge 0} G^n(\bot)$ is the least fixpoint of $G$.
\vspace{20pt}\\
When the function is not $\omega$-continuous, then we obtain $a_*$ as above (we jump over a discontinuity) and then continue iterating.  We then take the limit of such sequence, and the limit of limits etc., ultimately we obtain the fixpoint.
\end{frame}


\begin{frame}
\frametitle{Proving through Fixpoints of Approximate Functions}
\small
Meaning of a program (e.g. a set of reachable states) is a least fixpoint of $F$: $lfp(F)$.

Given specification $s$ (e.g. $pc=c \rightarrow i \ne 42$), prove $\mathbf{lfp(F) \subseteq s}$ 
($s$ is invariant)
\begin{itemize}
\item if $F(s) \subseteq s$ then $lfp(F) \subseteq s$ and we are done
\item $lfp(F) = \bigcup_{k \ge 0} F^k(\emptyset)$, but that is too hard to compute because 
it is infinite union unless, by some luck, $F^{n+1}(\emptyset) = F^n$ for some $n$
\end{itemize}

Instead, we search for an inductive strengthening of $s$: find $s'$ such that:
\begin{itemize}
\item $F(s') \subseteq s'$  \ \ \ ($s'$ is inductive). If so, theorem says $lfp(F) \subseteq s'$
\item $s' \subseteq s$ \ \ \ ($s'$ implies the desired specification). Then $lfp(F)\subseteq s' \subseteq s$
\end{itemize}
How to find $s'$? Iterating $F$ is hard, so we try some simpler function $\Fs$:
\begin{itemize}
\item suppose $\Fs$ is \emph{approximation}: $F(r) \subseteq \Fs(r)$ for all $r$
\item we can find $s'$ such that: $\Fs(s') \subseteq s'$  (e.g. $s' = \Fs^{n+1}(\emptyset) = \Fs^n(\emptyset)$)
\end{itemize}
Then: $F(s') \subseteq \Fs(s') \subseteq s'$. So, if $s' \subseteq s$, we have know $lfp(F) \subseteq s'$.

Abstract interpretation: automatically construct $\Fs$ using $F$ and $s$

\end{frame}
