\begin{slide}{Eigenschaften der Reduktion}

$\to$ auf $\Lambda$ ist
\begin{itemize}
\item
  konfluent,
\item
  aber nicht terminierend.

  $W=\lambda x.xx, \Omega = WW$.
\item
  es gibt Terme mit Normalform
  und unendlichen Ableitungen, $KI\Omega$ mit $K=\lambda xy.x, I=\lambda x.x$
\end{itemize}

Einige Eigenschaften klingen erstaunlich:
z. B. jeder Term $F$ besitzt einen Fixpunkt $A$,
d. h. $F A \to^* A$.

Den kann man sogar ausrechnen: es gibt $R$ mit $F(RF) \to^* RF$.
\end{slide}
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "~/edu/ws06/sym/folien/sym"
%%% End: 
