\begin{slide}{Termination und Normalisierung}

Für eine zweistellige Relation $\rho$ auf $M$

(zum Beispiel eine Ersetzungsrelation $\to_R$ auf $\Term(\Sigma)$)

\begin{itemize}
\item
  $\rho$ ist \emph{terminierend (stark normalisierend)},
  falls es keine unendliche lange $\rho$-Folge gibt

  d. h. $\rho(x_0,x_1), \rho(x_1,x_2), \rho(x_2,x_3),\ldots$
\item
  $\rho$ is \emp{schwach} normalisierend, 
  falls zu jedem $x_0\in M$
  eine $\rho$-Folge zu einer $\rho$-Normalform führt
\end{itemize}
Beachte:
es gibt $\rho$, die schwach, aber nicht stark normalisieren.

Beispiel (Wortersetzung): $ fgfg \to gfgffg $
(Alfons Geser, 2000)

\end{slide}
