\begin{frame}
\frametitle{Fixpoints}

{\bf Definition:} Given a set $A$ and a function $f : A \to A$ we say that $x \in A$ is a fixed point (fixpoint) of $f$ if $f(x)=x$.
\vspace{20pt}\\
{\bf Definition:} Let $(A,\le)$ be a partial order, let $f : A \to A$ be a monotonic function on $(A,\le)$, and let the set of its fixpoints be $S = \{ x \mid f(x)=x \}$.  If the least element of $S$ exists, it is called the {\bf least fixpoint}, if the greatest element of $S$ exists, it is called the {\bf greatest fixpoint}.

\end{frame}

%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Fixpoints}
Let $(A,\sqsubseteq)$ be a complete lattice and $G : A \to A$ a monotonic function.
\vspace{20pt}\\
{\bf Definition:}\\

$\mbox{Post} = \{x \mid G(x) \sqsubseteq x \}$ - the set of {\em postfix points} of $G$ \\
(e.g. $\top$ is a postfix point)

$\mbox{Pre} = \{x \mid x \sqsubseteq G(x) \}$ - the set of {\em prefix points} of $G$

$\mbox{Fix} = \{x \mid G(x) = x\}$ - the set of {\em fixed points} of $G$. 
\vspace{10pt}\\
Note that $\mbox{Fix} \subseteq \mbox{Post}$.

\end{frame}


%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Tarski's fixed point theorem}

{\bf Theorem}: Let $a = \sqcap \mbox{Post}$.  Then $a$ is the least element of $\mbox{Fix}$ (dually, $\sqcup \mbox{Pre}$ is the largest element of $\mbox{Fix}$).
\vspace{20pt}\\
{\bf Proof:}\\
Let $x$ range over elements of $\mbox{Post}$.
\begin{itemize}
\item applying monotonic $G$ from $a \sqsubseteq x$ we get $G(a) \sqsubseteq G(x) \sqsubseteq x$ 
 \item so $G(a)$ is a lower bound on $\mbox{Post}$, but $a$ is the greatest lower bound, so $G(a) \sqsubseteq a$ 
 \item therefore $a \in \mbox{Post}$
 \item $\mbox{Post}$ is closed under $G$, by monotonicity, so $G(a) \in \mbox{Post}$
 \item $a$ is a lower bound on $\mbox{Post}$, so $a \sqsubseteq G(a)$
  \item from $a \sqsubseteq G(a)$ and $G(a) \sqsubseteq a$ we have $a = G(a)$, so $a \in \mbox{Fix}$
  \item $a$ is a lower bound on $\mbox{Post}$ so it is also a lower bound on a smaller 
  set $\mbox{Fix}$ 
\end{itemize}

In fact, the set of all fixpoints $\mbox{Fix}$ is a lattice itself.
\end{frame}


%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Tarski's fixed point theorem}

Tarski's Fixed Point theorem shows that in a complete lattice with a monotonic function $G$ on this lattice, there is at least one fixed point of $G$, namely the least fixed point $\sqcap \mbox{Post}$.
\begin{itemize}
\item
Tarski's theorem guarantees fixpoints in complete lattices, but the above proof does not say how to find them.
\item
How difficult it is to find fixpoints depends on the structure of the lattice.
\end{itemize}

\end{frame}

% continue with file 2022/lecture12-ai/part2b.tex
