\begin{slide}{Existenz von Fixpunkten}

Fixpunkt von $f :: C \to C$ ist $x :: C$ mit $f x=x$.

Existenz? Eindeutigkeit? Konstruktion?

Satz: Wenn $C$ \emph{pointed CPO} und $f$ \emph{stetig},
dann besitzt $f$ genau einen kleinsten Fixpunkt.

Begriffe:
\begin{itemize}\itemsep 0pt \parskip 1pt
\item CPO $=$ complete partial order $=$ vollständige
  Halbordnung
\item complete $=$ jede monotone Folge besitzt
  Supremum ($=$ kleinste obere Schranke)
\item pointed: $C$ hat kleinstes Element $\bot$
\item stetig: $f (\sup \vec{x})=\sup \vec{f(x)}$
\end{itemize}
Dann $\text{fix} (f)= \sup [\bot,f(\bot),f^2(\bot),\ldots]$

\end{slide}

\begin{slide}{Funktionen als CPO}

  \begin{itemize}
  \item 
partielle Funktionen $C = (B\to B)$
\item
Bereich $B\cup{\bot}$ geordnet 
durch $\forall x\in B: \bot < x$
\item
$C$ geordnet durch 
$f\le g \iff \forall x\in B: f(x) \le g(x)$,
\item
d. h. $g$ ist Verfeinerung von $f$
\item
Das Bottom-Element von $C$
ist die überall undefinierte Funktion.
  \end{itemize}

\end{slide}

\begin{slide}{Funktionen als CPO, Beispiel}
Wert von
\begin{verbatim}
rec f ( \ x -> if (x==0) then 1 
               else x * f (x - 1) )
\end{verbatim}
ist Fixpunkt der Funktion $F = $
\begin{verbatim}
\ f -> ( \ x -> if (x==0) then 1 
                else x * f (x - 1) )
\end{verbatim}
  
Iterative Berechnung des Fixpunktes:
\begin{eqnarray*}
\bot &=& \emptyset \quad \text{überall undefiniert} \\
F \bot &=& \{ (0,1) \} \quad \text{sonst $\bot$} \\
F (F \bot) &=& \{ (0,1),(1,1) \} \quad \text{sonst $\bot$} \\
F^3 \bot &=& \{ (0,1),(1,1),(2,2) \} \quad \text{sonst $\bot$} 
\end{eqnarray*}

\end{slide}
