traat.tex

\documentclass{cheat-sheet}

\pdfinfo{
  /Title (Zusammenfassung Term Rewriting and All That)
  /Author (Tim Baumann)
}

\usepackage{algorithmicx}
\usepackage[noend]{algpseudocode}
\usepackage{framed}

\input{include/cats} % Kategorientheorie-Makros

\newcommand{\from}{\leftarrow}
\newcommand{\reducesTo}{\xrightarrow{*}}
\newcommand{\strictlyReducesTo}{\xrightarrow{+}}
\newcommand{\reducesFrom}{\xleftarrow{*}}
\newcommand{\toOrEq}{\xrightarrow{=}}
\newcommand{\fromOrEq}{\xleftarrow{=}}
\newcommand{\joinable}{\downarrow}
\newcommand{\zzEq}{\xleftrightarrow{*}} % Zigzag-Equivalent
\newcommand{\NF}[1]{{{#1}\!\downarrow}} % Normalform
\newcommand{\Multisets}{\mathcal{M}} % Multimengen über einer Menge
\DeclareMathOperator{\arity}{arity} % Arität (einer Funktion)
\DeclareMathOperator{\Pos}{Pos} % Menge der Positionen eines Terms
\newcommand{\size}[1]{\abs{{#1}}} % Größe eines Terms
\DeclareMathOperator{\Var}{Var} % Menge der Variablen eines Terms
\DeclareMathOperator{\Dom}{Dom} % Domain einer Ersetzung
\DeclareMathOperator{\Subst}{Sub} % Menge der Ersetzungen
\newcommand{\ident}{\approx} % Identität
\renewcommand{\Alg}{\mathcal{A}} % Sigma-Algebra
\newcommand{\SigmaAlgC}{\text{$\Sigma$-$\mathbf{Alg}$}} % Kategorie der Sigma-Algebren
\newcommand{\Variety}{\mathcal{V}} % Sigma-Varietät
\DeclareMathOperator{\CongClos}{CC} % kongruente Hülle
\newcommand{\inferrule}[2]{\frac{{#1}}{{#2}}} % logische Inferenzregel
\DeclareMathOperator{\Subterms}{Subterms} % Unterterme
\newcommand{\Unifiers}{\mathcal{U}} % Lösungen eines Unifikationsproblems
\newcommand{\emb}{\trianglerighteq_\text{emb}} % homöomorphe Einbettung
\newcommand{\strictlyEmb}{>_\text{emb}} % strikte homöomorphe Einbettung
\newcommand{\lpo}{\geq_\text{lpo}} % lexikographische Pfadordnung
\newcommand{\strictLpo}{>_\text{lpo}} % lexikographische Pfadordnung
\newcommand{\strictMpo}{>_\text{mpo}} % Multimengenpfadordnung
\newcommand{\kbo}{>_\text{kbo}} % Knuth-Bendix-Ordnung
\newcommand{\parallelTo}{\rightrightarrows} % parallele Reduktion

% Kleinere Klammern
\delimiterfactor=701

\setlength{\tabcolsep}{2pt}

\begin{document}

\raggedcolumns % stretche Inhalt nicht über die gesamte Spaltenhöhe

\maketitle{Zusammenfassung Term Rewriting aAT}

Dies ist eine übersetzte Zusammenfassung des Buches Term Rewriting and All That von Franz Baader und Tobias Nipkow.

% §2. Abstrakte Reduktionssysteme
\section{Abstrakte Reduktionssysteme}

\begin{defn}
  Ein \emph{abstraktes Reduktionssystem} ist ein Tupel $(A, {\to})$, wobei ${\to} \in A \times A$ eine Relation auf $A$ ist.
\end{defn}

% §2.1. Äquivalenz und Reduktion

\begin{defn}
  \,
  \begin{minipage}[t]{0.88 \linewidth}
    \begin{tabular}[t]{ r l l }
      $\xrightarrow{0}$ & $\coloneqq \Set{(a, a)}{a \in A}$ & Identität \\
      $\xrightarrow{i+1}$ & $\coloneqq {\xrightarrow{i}} \circ {\to}$ & $(i+1)$-fache Komposition, $i \geq 0$ \\
      $\from$ & $\coloneqq \Set{(t, s)}{(s, t) \in {\to}}$ & Inverse Relation \\
      $\toOrEq$ & $\coloneqq (\to) \cup (\xrightarrow{0})$ & refl. Hülle \\
      $\reducesTo$ & $\coloneqq \cup_{i \geq 0} (\xrightarrow{i})$ & refl. trans. Hülle \\
      $\strictlyReducesTo$ & $\coloneqq \cup_{i \geq 1} (\xrightarrow{i})$ & refl. trans. Hülle \\
      $\xleftrightarrow{}$ & $\coloneqq {\to} \cup {\from}$ & symm. Hülle \\
      $\zzEq$ & $\coloneqq (\xleftrightarrow{})^{*}$ & refl. trans. symm. Hülle
    \end{tabular}
  \end{minipage}
\end{defn}

\begin{defn}
  Sei $x \in A$ ein Term.
  \begin{itemize}
    \item Der Term $x$ heißt \emph{reduzibel}, falls ein $y \in A$ mit $x \to y$ existiert,
    \item \emph{irreduzibel} (oder in \emph{Normalform}) falls $x$ nicht reduzibel ist.
    \item Ein Term $y \in A$ heißt \emph{Normalform} von~$x$, falls $x \reducesTo y$ und~$y$ irreduzibel ist.
    \item Eine Term~$y$ heißt \emph{direkter Nachfolger} von~$x$, falls $x \to y$.
    \item Eine Term~$y$ heißt \emph{Nachfolger} von~$x$, falls $x \strictlyReducesTo y$.
    \item $x$ und~$y$ heißen \textit{joinable}, notiert \emph{$x \joinable y$}, falls $\ex{z} x \reducesTo z \reducesFrom y$.
  \end{itemize}
\end{defn}

\begin{defn}
  Eine Reduktion ${\to}$ heißt
  \begin{tabular}{r l l}
    \emph{Church-Rosser} & $\coloniff$ & $x \zzEq y \implies x \joinable y$ \\
    \emph{konfluent} & $\coloniff$ & $y_1 \reducesFrom y \reducesTo y_2 \implies y_1 \joinable y_2$ \\
    \emph{semi-konfluent} & $\coloniff$ & $y_1 \from y \reducesTo y_2 \implies y_1 \joinable y_2$ \\
    \emph{terminierend} & $\coloniff$ &
      \begin{minipage}[t]{0.8 \linewidth}
        es gibt keine unendlich absteigende Kette \\
        $x_0 \to x_1 \to x_2 \to \ldots$
        \quad (auch: \textit{noethersch})
      \end{minipage} \\
    \emph{normalisierend} & $\coloniff$ & jeder Term besitzt eine Normalform \\
    \emph{konvergent} & $\coloniff$ & konfluent $\wedge$ normalisierend \\
  \end{tabular}
\end{defn}

\begin{lem}
  Für eine Reduktion ${\to}$ sind äquivalent:
  \begin{itemize}
    \item ${\to}$ ist Church-Rosser
    \item ${\to}$ ist konfluent
    \item ${\to}$ ist semi-konfluent
  \end{itemize}
\end{lem}

\begin{lem}
  Ist die Reduktion ${\to}$ konfluent/terminierend/konvergent, so besitzt jeder Term höchstens/mindestens/genau eine Normalform.
\end{lem}

\begin{nota}
  Falls~$x$ eine NF~$y$ besitzt, so schreibe $x \NF \coloneqq y$.
\end{nota}

\begin{thm}
  Ist ${\to}$ konvergent, so gilt $x \zzEq y \iff \NF{x} = \NF{y}$.
\end{thm}

\begin{bem}
  Dies liefert einen einfachen Algorithmus, um $x \zzEq y$ zu entscheiden:
  Reduziere die Terme~$x$ und~$y$ zu Normalformen~$\NF{x}$ bzw.~$\NF{y}$ und vergleiche diese.
\end{bem}

% §2.2. Wohlfundierte Induktion
\subsection{Terminierungsbeweise}

\begin{lem}
  ${\to}$ ist terminierend $\iff$ ${\to}$ ist eine Wohlordnung
\end{lem}

\begin{defn}
  Eine Relation ${\to}$ heißt
  \begin{itemize}
    \item \emph{endlich verzweigend}, falls jeder Term nur endlich viele direkte Nachfolger besitzt,
    \item \emph{global endlich}, falls jeder Term nur endl. viele Nachfolger hat,
    \item \emph{azyklisch}, falls kein Term~$a$ mit $a \strictlyReducesTo a$ existiert.
  \end{itemize}
\end{defn}

\begin{lem}
  \begin{itemize}
    \item Eine endlich verzweigende Relation ist global endlich, falls sie terminierend ist.
    \item Eine azykl. Relation ist terminierend, falls sie global endlich ist.
  \end{itemize}
\end{lem}

% §2.3. Terminierungsbeweise

\begin{lem}
  Sei $(A, {\to})$ ein Reduktionssystem und $(B, {>})$ eine wohlgeordnete Menge.
  Gibt es eine streng monotone Abbildung $\varphi : A \to B$, so ist~$A$ terminierend.
\end{lem}

\begin{lem}
  Ein endlich verzweigendes Reduktionssystem~$(A, {\to})$ ist genau dann terminierend, falls es eine streng monotone Abbildung $\varphi : (A, {\to}) \to (\N, >)$ gibt.
\end{lem}

% §2.4. Lexikographische Ordnungen

\begin{defn}
  Seien $(A_i, >_i)_{i = 1, \ldots, n}$ geordnete Mengen.
  Die \emph{lexikalische Ordnung}~$>_{\text{lex}}$ auf $A_1 \times \ldots \times A_n$ ist definiert durch
  \[
    (x_1, \nldots, x_n) >_{\text{lex}} (y_1, \nldots, y_n) \!\!\coloniff\! \ex{k {\leq} n\!}\! (\fa{i {<} k\!}\! x_i \!=\! y_i) \,\wedge\, x_k <_k y_k.
  \]
\end{defn}

\begin{lem}
  Ist $>$ eine strikte (Wohl-) Ordnung, so auch $>_{\textit{lex}}$.
\end{lem}

% ausgelassen: $>_{lex}^*$, $>_{Lex}$

% §2.5. Multimengen-Ordnungen

\begin{defn}
  Eine \textit{Multimenge}~$M$ über einer Menge~$A$ ist eine Abbildung $M : A \to \N$.
  Sie ist endlich, falls ${\sum}_{a \in A} M(a) < \infty$.
\end{defn}

\begin{nota}
  \begin{minipage}[t]{0.8 \linewidth}
    $\Multisets(A) \coloneqq \{ \text{ Multimengen über $A$ } \}$ \\
    $a \in M \coloniff M(a) \geq 1$
  \end{minipage}
\end{nota}

\begin{defn}
  Die \textit{Differenz} von Multimengen~$M, N \in \Multisets(A)$ ist $M - N \in \Multisets(A)$ mit
  $(M - N)(a) \coloneqq \max \{ 0, M(a) - N(a) \}$.
\end{defn}

\begin{defn}
  Sei ${>}$ eine strikte Ordung auf~$A$.
  Die \emph{Multimengenordnung} $>_{\text{mul}}$ auf $\Multisets(A)$ ist dann definiert durch
  \[
    M >_{\text{mul}} N \coloniff M \neq N \wedge \fa{n \in N - M} \ex{m \in M - N} m > n.
  \]
\end{defn}

\begin{lem}
  Ist $>$ eine strikte (Wohl-) Ordnung, so auch $>_{\textit{mul}}$.
\end{lem}

% §2.6. Ordnungen in ML (ausgelassen)

% §2.7. Konfluenzbeweise
\subsection{Konfluenzbeweise}

% TODO: ist die Diamant-Eigenschaft relevant?
\begin{defn}
  Eine Relation ${\to}$
  \begin{itemize}
    \item heißt \emph{lokal konfluent}, falls $y_1 \!\from\! y \to y_2 \implies y_1 \joinable y_2$.
    \item heißt \emph{stark konfluent}, falls $y_1 \!\from\! y \!\to\! y_2 \implies \ex{z\!}\! y_1 \reducesTo z \fromOrEq y_2$.
    \item besitzt die \emph{Diamant-Eigenschaft}, falls
    \[
      y_1 \!\from\! y \!\to\! y_2 \implies \ex{z} y_1 \to z \from y_2.
    \]
  \end{itemize}
\end{defn}

\begin{lem}
  starke Konfluenz $\implies$ Konfluenz
\end{lem}

\begin{lem}
  \begin{minipage}[t]{0.8 \linewidth}
    Falls ${\to_1} \leq {\to_2} \leq {\xrightarrow{*}_1}$, so gilt ${\xrightarrow{*}_1} = {\xrightarrow{*}_2}$. \\
    Ist zusätzlich~$\to_2$ (stark) konfluent, so auch ${\to_1}$.
  \end{minipage}
\end{lem}

% 2.7.2
\begin{lem}[\emph{Newman}]
  Eine terminierende Relation ist genau dann konfluent, falls sie lokal konfluent ist.
\end{lem}

% §2.7.1. Kommutation

% TODO: sind die beiden letzen Definitionen relevant?
\begin{defn}
  Zwei Relationen~${\to_1}$ und~${\to_2}$ auf~$A$
  \begin{itemize}
    \item \emph{kommutieren}, falls $y_1 \reducesFrom_1 x \reducesTo_2 y_2 \implies \ex{z} y_1 \reducesTo_2 z \reducesFrom_1 y_2$.
    \item \emph{kommutieren stark}, falls
    \[
      y_1 \from_1 x \to_2 y_2 \implies \ex{z} y_1 \toOrEq_2 z \reducesFrom_1 y_2.
    \]
    \item besitzen die \emph{Kommutierender-Diamant-Eigenschaft}, falls
    \[
      y_1 \from_1 x \to_2 y_2 \implies \ex{z} y_1 \to_2 z \from_1 y_2.
    \]
  \end{itemize}
\end{defn}

\begin{lem}
  Angenommen, $\to_1$ und~$\to_2$ sind konfluent und kommutieren. \\
  Dann ist auch ${\to_1} \cup {\to_2}$ konfluent.
\end{lem}

% §3. Universelle Algebra
\section{Universelle Algebra}

% §3.1. Terme, Ersetzungen und Identitäten

\begin{defn}
  Eine \emph{Signatur}~$\Sigma$ ist eine Menge von \textit{Funktionssymbolen} zusammen mit einer Aritätsabbildung $\arity : \Sigma \to \N$.
  % Elemente von $\Sigma^{(0)}$ heißen \emph{konstante Symbole}
\end{defn}

\begin{nota}
  $\Sigma^{(n)} \coloneqq \mathrm{arity}^{-1}(n)$
\end{nota}

\begin{defn}
  Sei~$\Sigma$ eine Signatur und~$X$ eine Menge von Variablen (\dh{} es gilt $X \cap \Sigma = \emptyset$).
  Die Menge~$T(\Sigma, X)$ der \emph{$\Sigma$-Terme über~$X$} ist induktiv definiert durch
  \begin{itemize}
    \item $X \subseteq T(\Sigma, X)$
    \item $\fa{f \in \Sigma^{(n)}, t_1 \in T(\Sigma, X), \nldots, t_n \in T(\Sigma, X)} f(t_1, \nldots, t_n) \in T(\Sigma, X)$
  \end{itemize}
\end{defn}

\begin{bem}
  Falls $X \subseteq Y$, $Y \cap \Sigma = \emptyset$, so gilt $T(\Sigma, X) \subseteq T(\Sigma, Y)$.
\end{bem}

\begin{defn}
  Terme~$t$ ohne freie Variablen (\dh{} $t \in T(\Sigma, \emptyset)$) heißen \emph{Grundterme} oder \emph{geschlossene Terme}.
\end{defn}

\begin{defn}
  Die Menge der \emph{Positionen}~$\Pos(s)$ eines Terms~$s \in T(\Sigma, X)$ ist folgende Menge von Listen von natürlichen Zahlen
  \begin{itemize}
    \item Falls $s = x \in X$: $\Pos(s) \coloneqq \{ \epsilon \}$
    \item Falls $s = f(s_1, \ldots, s_n)$: $\Pos(s) \coloneqq \{ \epsilon \} \cup {\bigcup}_{i=1}^n \Set{i p}{p \in \Pos(s_i)}$
  \end{itemize}
\end{defn}

\begin{defn}
  Die \emph{Größe} eines Terms~$s \in T(\Sigma, X)$ ist $\size{s} \coloneqq \abs{\Pos(s)}$.
\end{defn}

\begin{defn}
  Der \emph{Subterm}~$s|_p$ an der Position~$p \in \Pos(s)$ eines Terms~$s$ ist
  \[
    s|_\epsilon \coloneqq s, \qquad
    f(s_1, \ldots, s_n)|_{i q} \coloneqq s_i|_q.
  \]
  Die \emph{Ersetzung}~$s[t]_p$ von~$s|_p$ durch einen Term~$t \in T(\Sigma, X)$ ist
  \[
    s[t]_\epsilon \coloneqq t, \qquad
    f(s_1, \ldots, s_n)[t]_{i q} \coloneqq s_i[t]_q.
  \]
\end{defn}

\begin{defn}
  Die \emph{Menge der Variablen} in~$s \in T(\Sigma, X)$ ist
  \[
    \Var(s) \coloneqq \Set{x \in X}{\ex{p \in \Pos(s)} s|_p = x}.
  \]
\end{defn}

\begin{bem}
  Für jeden Term~$t \in T(\Sigma, X)$ gilt $t \in T(\Sigma, \Var(t))$.
\end{bem}

% Ausgelassen: Lemma 3.1.4 über Gleichheiten mit Subtermen, Termersetzung

\begin{defn}
  Sei~$\Sigma$ eine Signatur und~$V$ eine abzählbar unendliche Menge von Variablen.
  Eine $T(\Sigma, V)$-\emph{Ersetzung} ist eine Abbildung $\sigma : V \to T(\Sigma, V)$, für die gilt:
  \[
    \Dom(\sigma) \coloneqq \Set{v \in V}{\sigma(v) \neq v}
  \]
  ist endlich.
  Die Menge der $T(\Sigma, V)$-Ersetzungen ist $\Subst(T(\Sigma, V))$.
  % Ausgelassen: Ran, VRan
  Wir können~$\sigma$ ausdehnen zu einer Abb.~$\hat{\sigma} : T(\Sigma, V) \to T(\Sigma, V)$ durch
  \[
    \hat{\sigma}(v) \coloneqq \sigma(v), \qquad
    \hat{\sigma}(f(s_1, \ldots, s_n)) \coloneqq f(\hat{\sigma}(s_1), \ldots, \hat{\sigma}(s_n)).
  \]
  Die \textit{Komposition} zweier Ersetzungen~$\sigma$ und~$\tau$ ist $\sigma \circ \tau \coloneqq \hat{\sigma} \circ \tau$.
\end{defn}

\begin{defn}
  Eine \emph{$\Sigma$-Identität} ist ein Paar $(s, t) \in T(\Sigma, V) \times T(\Sigma, V)$, auch geschrieben $s \ident t$.
\end{defn}

% 3.1.8
\begin{defn}
  Die \emph{Reduktionsrelation}~$\to_E$ zu einer Menge~$E$ von $\Sigma$-Identitäten ist
  \begin{align*}
    s \to_E t \coloniff \, & \ex{(l \ident r) \in E, p \in \Pos(s), \sigma \in \Subst(T(\Sigma, V))} \\
    & s|_p = \sigma(l) \wedge t = s[\sigma(r)]_p.
  \end{align*}
\end{defn}

% 3.1.9
\begin{defn}
  Eine Relation~$\equiv$ auf~$T(\Sigma, V)$ heißt
  \begin{itemize}
    \item \emph{abgeschlossen unter Ersetzungen}, falls $s \equiv t \implies \sigma(s) \equiv \sigma(t)$
    \item \emph{abgeschlossen unter $\Sigma$-Operationen}, falls
    \[
      s_1 \equiv t_1, \ldots, s_n \equiv t_n \implies f(s_1, \ldots, s_n) \equiv f(t_1, \ldots, t_n)
    \]
    \item \emph{kompatibel mit $\Sigma$-Operationen}, falls
    \[
      \begin{array}{r c l}
        s \equiv t \implies &&
        f(s_1, \ldots, s_{i-1}, s, s_{i+1}, \ldots, s_n) \\
        &\equiv& f(s_1, \ldots, s_{i-1}, t, s_{i+1}, \ldots, s_n)
      \end{array}
    \]
    \item \emph{kompatibel mit $\Sigma$-Kontexten}, falls
    \[
      s \equiv s' \implies t[s]_p \equiv t[s']_p
    \]
    % 4.2.2
    \item \emph{Umschreibungsrelation}, falls sie kompatibel mit $\Sigma$-Operationen und abgeschlossen unter Ersetzungen ist.
  \end{itemize}
\end{defn}

% 3.1.11
\begin{lem}
  Es sind äquivalent:
  \begin{itemize}
    \item $\equiv$ ist kompatibel mit $\Sigma$-Operationen
    \item $\equiv$ ist kompatibel mit $\Sigma$-Kontexten
  \end{itemize}
  Ist~$\equiv$ reflexiv und transitiv, so ist außerdem äquivalent:
  \begin{itemize}
    \item $\equiv$ ist abgeschlossen unter $\Sigma$-Operationen
  \end{itemize}
\end{lem}

\begin{thm}
  Sei~$E$ eine Menge von $\Sigma$-Identitäten.
  \begin{itemize}
    % 3.1.10
    \item ${\to_E}$, ${\strictlyReducesTo_E}$ und ${\reducesTo_E}$ sind Umschreibungsrelationen.
    % 3.1.12
    \item Die Relation $\zzEq_E$ ist die kleinste Äquivalenzrelation, die~$E$ enthält und abg. ist unter Ersetzungen und $\Sigma$-Operationen.
  \end{itemize}
\end{thm}

% §3.2. Algebren, Homomorphismen und Kongruenzen

% 3.2.1
\begin{defn}
  Eine \emph{$\Sigma$-Algebra}~$\Alg$ besteht aus
  \begin{itemize}
    \item einer \textit{Trägermenge}~$A$ und
    \item einer Abbildung $f^\Alg : A^n \to A$ für alle $f \in \Sigma^{(n)}$.
  \end{itemize}
\end{defn}

% 3.4.1
\begin{bsp}
  $T(\Sigma, V)$ ist eine $\Sigma$-Algebra mit
  \[
    f^{T(\Sigma, V)} : T(\Sigma, V)^n \to T(\Sigma, V), \quad
    (t_1, \ldots, t_n) \mapsto f(t_1, \ldots, t_n).
  \]
\end{bsp}

% 3.2.2
\begin{defn}
  \begin{itemize}
    \item Eine \emph{$\Sigma$-Subalgebra} von~$A$ ist eine Teilmenge~$B \subset A$, sodass $f^\Alg(b_1, \ldots, b_n) \in B$ für alle $f \in \Sigma^{(n)}$ und $b_1, \ldots, b_n \in B$.
    \item Die von $X \subseteq A$ \emph{erzeugte $\Sigma$-Subalgebra} ist die kleinste $\Sigma$-Subalgebra, die~$X$ enthält.
  \end{itemize}
\end{defn}

% 3.2.3
\begin{defn}
  Ein \textit{Homomorphismus}~$\phi$ zwischen $\Sigma$-Algebren~$\Alg$ und~$\mathcal{B}$ (mit Trägermengen~$A$ bzw.~$B$) ist eine Abbildung $\phi : A \to B$, sodass
  \[
    \phi(f^\Alg(a_1, \ldots, a_n)) = f^\mathcal{B}(\phi(a_1), \ldots, \phi(a_n)).
  \]
\end{defn}

\begin{bem}
  Damit bilden $\Sigma$-Algebren eine Kategorie.
\end{bem}

% 3.2.4
\begin{defn}
  %Sei~$\Alg$ eine $\Sigma$-Algebra.
  Eine Äquivalenzrelation~$\equiv$ auf~$A$ heißt \emph{Kongruenz} auf~$\Alg$, falls
  \[
    a_1 \equiv b_1, \ldots, a_n \equiv b_n \implies f^\Alg(a_1, \ldots, a_n) \equiv f^\Alg(b_1, \ldots, b_n).
  \]
\end{defn}

\begin{lemdefn}
  Ist $\equiv$ eine Äquivalenz, so wird $A/\equiv$ mit
  \[
    f^{\Alg/\equiv}([a_1], \ldots, [a_n]) \coloneqq [f^\Alg(a_1, \ldots, a_n)]
  \]
  eine $\Sigma$-Algebra, die \emph{Quotientenalgebra} $\Alg/\equiv$.
\end{lemdefn}

% ausgelassen: Lemma 3.2.5 (Eigenschaften der Quotientenalgebra)

% Def 3.2.6 umformuliert und verallgemeinert
\begin{lem}
  Die Kategorie der $\Sigma$-Algebren enthält kleine Limiten.
\end{lem}

% §3.3. Freie Algebren

\begin{defn}
  Eine $\Sigma$-Algebra heißt \emph{frei}, falls sie isomorph ist zu $F(X) \coloneqq T(\Sigma, X)$ für eine Menge~$X$ von Variablen.
\end{defn}

\begin{bem}
  Diese Setzung definiert einen Funktor $F : \SetC \to \SigmaAlgC$.
\end{bem}

\begin{lem}
  $F \ladj U$, wobei $U : \SetC \to \SigmaAlgC$ der Vergissfunktor ist.
\end{lem}

\begin{kor}
  $F(\emptyset) = T(\Sigma, \emptyset)$ ist das initiale Objekt in~$\SigmaAlgC$.
\end{kor}

% Lemma 3.3.3. ausgelassen, da es allein daraus folgt, dass initiale Objekte eindeutig bis auf eindeutige Isomorphie sind

% §3.4. Termalgebren

% Def 3.4.1 ist vorgezogen worden

% Lem 3.4.2 ist redundant

% §3.5. Gleichheitsklassen

% 3.5.1 und 3.5.2
\begin{defn}
  \begin{itemize}
    \item Eine $\Sigma$-Identität $s \ident t$ \emph{gilt in einer $\Sigma$-Algebra}~$\Alg$, falls für alle Homomorphismen $\phi : T(\Sigma, V) \to \Alg$ gilt: $\phi(s) = \phi(t)$.
    \item $\Alg$ ist ein \emph{Modell} einer Menge~$E$ von $\Sigma$-Algebren (notiert $\Alg \models E$), falls jede Identität aus~$E$ in~$\Alg$ gilt.
    \item Die Subkategorie von~$\SigmaAlgC$ der Modelle von~$E$ heißt \textit{durch~$E$ definierte} \emph{$\Sigma$-Varietät}~$\Variety(E)$.
  \end{itemize}
\end{defn}

\begin{defn}
  \begin{itemize}
    \item Die Identität $s \ident t$ ist eine \emph{semantische Konsequenz} von~$E$ (notiert $E \models s \ident t$), falls $s \ident t$ in allen $\Alg \in \Variety(E)$ gilt.
    \item ${\ident_E} \coloneqq \Set{(s,t)}{E \models s \approx t}$ heißt von~$E$ \emph{induzierte Theorie}. % von Gleichheiten
  \end{itemize}
\end{defn}

% 3.5.4
\begin{defn}
  Eine Relation~$\equiv$ auf~$T(\Sigma, V)$ heißt \emph{voll invariant}, falls $s \equiv t \implies \phi(s) \equiv \phi(t)$ für alle Mor. $\phi : T(\Sigma, V) \to T(\Sigma, V)$.
\end{defn}

% 3.5.4
\begin{lem}
  $\ident_E$ ist eine voll invariante Kongruenz.
  % zweiter Teil weggelassen
\end{lem}

% 3.5.5
\begin{lemdefn}
  Es sind äquivalent:
  \begin{itemize}
    \item $E$ heißt \emph{trivial}
    \item $\ident_E = T(\Sigma, V) \times T(\Sigma, V)$
    \item $x \ident_E y$ gilt für Variablen $x, y \in V$, $x \neq y$
    \item $\Variety(E)$ besteht aus Algebren der Kardinalität $\leq 1$.
  \end{itemize}
\end{lemdefn}

\begin{thm}
  Sei~$V$ eine abzählbar unendliche Menge von Variablen.
  \begin{itemize}
    % 3.5.6
    \item $T(\Sigma, V)/{\ident_E}$ ist eine freie Algebra in~$\Variety(E)$ mit erz. Menge~$V/{\ident_E}$. Falls~$E$ nicht trivial ist, so ist $V/{\ident_E}$ abzählbar unendlich.
    % 3.5.7
    \item $T(\Sigma, V)/{\ident_E} \models s \ident t \iff s \ident_E t$
  \end{itemize}
\end{thm}

% ausgelassen: 3.5.8

\begin{defn}
  Die durch~$E$ \emph{induzierte induktive Theorie} ist
  \[
    {\ident_E^I} \coloneqq \Set{(s, t)}{T(\Sigma, \emptyset) \models s \ident t} \subseteq T(\Sigma, V) \times T(\Sigma, V).
  \]
\end{defn}

\begin{bem}
  ${\ident_E} \subseteq {\ident_E^I}$
\end{bem}

% ausgelassen: 3.5.11

% 3.5.12
\begin{umformulierung}
  Die Relation $\zzEq_E$ ist die kleinste voll invariante Kongruenz auf $T(\Sigma, V)$, die~$E$ enthält.
\end{umformulierung}

% 3.5.13
\begin{lem}
  Für eine voll invariante Kongruenz~$\equiv$ auf $T(\Sigma, V)$ gilt:
  \[ E \subseteq {\equiv} \implies {\ident_E} \subseteq {\equiv}. \]
\end{lem}

\begin{kor}[\emph{Birkhoffs Lemma}]
  $\zzEq_E \enspace = \enspace \ident_E$
\end{kor}

% 3.5.15
\begin{thm}
  Für eine Klasse~$\mathcal{K}$ von $\Sigma$-Algebren sind äquivalent:
  \begin{itemize}
    \item $\mathcal{K}$ ist eine Varietät, \dh{} $\mathcal{K} = \Variety(E)$ für eine Menge~$E$ von Identitäten.
    \item $\mathcal{K}$ ist abgeschlossen unter dem Bilden von Unteralgebren, Bildalgebren und direkten Produkten.
  \end{itemize}
\end{thm}

% §4. Gleichheitsprobleme
\section{Gleichheitsprobleme}

\begin{defn}
  Sei~$E$ eine Menge von Identitäten.
  Eine Gleichheit~$s \ident t$ heißt
  \begin{itemize}
    \item \emph{gültig} in~$E$, falls $s \ident_E t$,
    \item \emph{erfüllbar} in~$E$, falls es eine Ersetzung~$\sigma$ mit $\sigma(s) \ident_E \sigma(t)$ gibt.
  \end{itemize}
\end{defn}

% §4.1. Eine Entscheidungsprozedur für $\ident_E$

\begin{problem}[\emph{matching problem}]
  Gegeben Terme~$s$ und~$l$, gibt es eine Ersetzung~$\sigma$, sodass $\sigma(s) = l$?
\end{problem}

% 4.1.1
\begin{thm}
  Ist~$E$ endlich und $\to_E$ konvergent, so ist ${\approx_E}$ entscheidbar.
\end{thm}

\begin{alg}
  Seien~$x$ und~$y$ gegeben.
  Wegen der Endlichkeit von~$E$ sind~$\NF{x}$ und $\NF{y}$ berechenbar.
  Es gilt $x \ident_E y \iff \NF{x} = \NF{y}$.
\end{alg}

% 4.1.2.
\begin{defn}
  \begin{itemize}
    \item \emph{Wortproblem}: \,\,Gegeben $x, y \in T(\Sigma, V)$, gilt $x \ident_E y$?
    \item \emph{Grundwortproblem}: Gegeben $x, y \in T(\Sigma, \emptyset)$,\,\, gilt $x \ident_E y$?
  \end{itemize}
\end{defn}

% Bsp 4.1.3
\begin{bem}
  Das Wortproblem ist im Allgemeinen unentscheidbar, denn:
  \begin{itemize}
    \item Man kann den turingvollständigen SKI-Kalkül als Reduktions- system durch Angabe einer Menge von Gleichheiten spezifizieren.
    \item Gleichheit von Programmen ist unentscheidbar.
  \end{itemize}
\end{bem}

% §4.2. Termumschreibungssysteme

\begin{defn}
  \begin{itemize}
    \item Eine \emph{Umschreibungsregel} ist eine Identität $l \ident r$ bei der~$s$ keine Variable ist und $\Var(l) \supseteq \Var(r)$.
    \item Ein \emph{Termumschreibungssystem} (TUS) ist eine Menge von Umschreibungsregeln.
  \end{itemize}
  % ausgelassen: regex, contraction
\end{defn}

\begin{samepage}

\begin{bem}
  Die zwei Bedingungen für Umschreibungsregeln sind notwendig (aber nicht hinreichend) dafür, dass Termumschreibungssysteme terminierend sind.
\end{bem}

% §4.3. Die kongruente Hülle
\subsection{Die kongruente Hülle}
  
\end{samepage}

\begin{defn}
  Die \emph{kongruente Hülle}~$\CongClos(E)$ von~$E \subseteq T(\Sigma, V) \times T(\Sigma, V)$ ist die kleinste Kongruenzrelation, die $\equiv$ enthält.
\end{defn}

\begin{bem}
  $(s, t) \in \CongClos(E)$ gilt genau dann, wenn die Aussage aus folgenden Inferenzregeln herleitbar ist:
  \[
    \inferrule
      {\,}
      {(t, t) \in \CongClos(E)} \quad
    \inferrule
      {(t, s) \in \CongClos(E)}
      {(s, t) \in \CongClos(E)} \quad
    \inferrule
      {(r, s) \in \CongClos(E) \quad
       (s, t) \in \CongClos(E)}
      {(r, t) \in \CongClos(E)}
  \]
  \[
    \inferrule
      {(s, t) \in E}
      {(s, t) \in \CongClos(E)} \quad
    \inferrule
      {f \in \Sigma^{(n)} \quad
       (s_1, t_1) \in \CongClos(E), \ldots, (s_n, t_n) \in \CongClos(E)}
      {(f(s_1, \ldots, s_n), f(t_1, \ldots, t_n)) \in \CongClos(E)}
  \]
\end{bem}

\begin{defn}
  Eine Id. $l \ident r$ heißt \emph{Grundidentität}, falls $\Var(l) \!=\! \Var(r) \!=\! \emptyset$.
\end{defn}

\begin{nota}
  Sei~$G$ im Folgenden eine Menge von Grundidentitäten.
\end{nota}

\begin{lem}
  $\CongClos(G) = {\ident_G}$
\end{lem}

\begin{defn}
  Die Menge der \emph{Unterterme} ist
  \begin{align*}
    \Subterms(t) & \coloneqq \Set{t|_p}{p \in \Pos(t)} \quad \text{für $t \in T(\Sigma, V)$ bzw.} \\
    \Subterms(G) & \coloneqq {\bigcup}_{l \ident r} \Subterms(l) \cup \Subterms(r).
  \end{align*}
\end{defn}

% ausgelassen: Lemma 4.3.4

% 4.3.5
\begin{thm}
  Fixiere zwei Terme $s, t \in T(\Sigma, V)$.
  Setze
  \[
    S \coloneqq \Subterms(s) \cup \Subterms(t) \cup \Subterms(G).
  \]
  Es gilt $G \subseteq S \times S$.
  Es sei $\CongClos_S(G)$ die kongruente Hülle von~$G$ innerhalb von~$S \times S$.
  Dann gilt:
  \[
    \CongClos_S(G) = {\ident_G} \cap (S \times S).
  \]
\end{thm}

% 4.3.6
\begin{kor}
  Das Wortproblem ist für endliche Mengen~$G$ von Grundidentitäten entscheidbar.
\end{kor}

\begin{beweisidee}
  Seien~$s$ und~$t$ gegeben. Berechne die endliche Menge~$\CongClos_S(G)$.
  Es gilt dann:
  $s \ident_G t \iff (s, t) \in \CongClos_S(G)$.
\end{beweisidee}

\begin{bem}
  Dies liefert einen Entscheidungsalgorithmus mit polynomieller Laufzeit in~$G$, $s$ und~$t$.
\end{bem}

% §4.4 Kongruente Hülle auf Graphen

\begin{samepage}

\begin{alg}
  Effiziente Realisierung:

  \begin{itemize}
    \item Repräsentiere die Termmenge~$S$ als gerichteter Graph, wobei jeder Knoten~$v$ mit einem Symbol~$f \in \Sigma$ beschriftet ist und dessen Auskanten mit $i = 1, \ldots, \arity(f)$ nummeriert sind.
    \item Wir repräsentieren Identifikationen von Knoten im Graph über Zeiger wie in der Union-Find-Datenstruktur.
    Wir definieren $u \sim v \coloniff \Call{find}{u} = \Call{find}{v}$ für Knoten~$u$ und~$v$.
  \end{itemize}

  \begin{algorithmic}[1]
    \Function{merge}{$u$, $v$}
      \If{$u \not\sim v$}
        \State $P \coloneqq \Call{pred}{u}$, $Q \coloneqq \Call{pred}{v}$
        \State $\Call{union}{u, v}$
        \For{$(p, q) \in P \times Q$}
          \If{$p \not\sim q \wedge \Call{congruent}{p, q}$} \State $\Call{merge}{p, q}$ \EndIf
        \EndFor
      \EndIf
    \EndFunction
    \Function{congruent}{$p = f(p_1, \ldots, p_n)$, $q = g(q_1, \ldots, q_m)$}
      \If{$f \not= g \in \Sigma$} \Return false \EndIf
      \For{$i = 1, \ldots, n$}
        \If{$p_i \not\sim q_i$} \Return false \EndIf
      \EndFor
      \Return true
    \EndFunction
  \end{algorithmic}

  \begin{itemize}
    \item Rufe zu Beginn des Algorithmus $\Call{merge}{l, r}$ für alle Grundidentitäten $(l \ident r) \in G$ auf.
    \item Das Ergebnis ist nun $s \sim t$.
  \end{itemize}
\end{alg}

% §4.5 Syntaktische Unifikation
\subsection{Syntaktische Unifikation}
  
\end{samepage}

% 4.5.1
\begin{defn}
  Eine Substitution~$\sigma$ heißt \emph{allgemeiner} (notiert $\sigma \lesssim \sigma'$) als~$\sigma'$, falls eine Substitution~$\delta$ mit $\sigma' = \delta \sigma$ existiert.
\end{defn}

% 4.5.2
\begin{lem}
  $\lesssim$ ist eine Quasiordnung
\end{lem}

\begin{defn}
  Eine \emph{Umbenennung} ist eine Ersetzung~$\rho$ mit $\im(\rho) \subseteq V$ ($\implies \im(\rho) = V$).
\end{defn}

% 4.5.3
\begin{lem}
  $\sigma \lesssim \sigma' \wedge \sigma' \lesssim \sigma \iff \ex{\text{Umbenennung~$\rho$}} \sigma = \rho \sigma'$
\end{lem}

% 4.5.4
\begin{defn}
  Ein \emph{Unifikationsproblem} ist gegeben durch eine endliche Menge von Gleichungen
  \[
    S = \{ s_1 \overset{?}= t_1, \ldots, s_n \overset{?}= t_n \}.
  \]
  Eine \textit{Lösung} von~$S$ ist eine Ersetzung~$\sigma$ mit $\hat{\sigma}(s_i) = \hat{\sigma}(t_i)$ für $i = 1, \ldots, n$.
  Notation: $\Unifiers(S) \coloneqq \{ \text{ Lösungen von~$S$ } \}$
\end{defn}

\begin{gesucht}
  Eine \emph{allgemeinste Lösung} von~$S$, das ist ein bezüglich~$\lesssim$ kleinstes Element in~$\Unifiers(S)$.
\end{gesucht}

% 4.5.8
\begin{thm}
  Hat ein Unifikationsproblem eine Lösung, so hat es auch eine idempotente, allgemeinste Lösung.
\end{thm}

% §4.6 Unifikation durch Transformation

% 4.6.1
\begin{defn}
  Ein Unifikationsproblem $S = \{ x_1 \overset{?}= t_1, \ldots, x_n \overset{?}= t_n \}$ ist in \emph{gelöster Form}, falls $x_1, \ldots, x_n$ paarweise verschieden Variablen sind, die nicht in den Termen $t_1, \ldots, t_n$ auftreten.
  In diesem Fall ist
  \[
    \vec{S} \coloneqq \{ x_1 \mapsto t_1, \ldots, x_n \mapsto t_n \}.
  \]
\end{defn}

% 4.6.2 und 4.6.3
\begin{lem}
  Sei~$S$ in gelöster Form.
  Dann gilt:
  \begin{itemize}
    \item $\fa{\sigma \in \Unifiers(S)} \sigma = \sigma \vec{S}$
    \item $\vec{S}$ ist eine idempotente, allgemeinste Lösung von~$S$.
  \end{itemize}
\end{lem}

\begin{alg}[$\Call{unify}{S}$]
  Wende wiederholt folgende Transformationsregeln (in beliebiger Reihenfolge) auf~$S$ an:
  \FrameSep0pt
  \begin{framed}
    \[
      \begin{array}{l r c l}
        \text{Delete}
          & \{ t \overset{?}= t \} \sqcup S
          & \rightsquigarrow
          & S \\
        \text{Decompose}
          & \{ f(\vec{s}) \overset{?}= f(\vec{t})
          & \rightsquigarrow
          & \{ s_1 \overset{?}= t_1, \ldots, s_n \overset{?}= t_n \} \cup S \\
        \text{Orient}
          & \{ t = x \} \sqcup S
          & \rightsquigarrow
          & \{ x = t \} \cup S \text{falls $t \not\in V$} \\
        \text{Eliminate}
          & \{ x \overset{?}= t \} \sqcup S
          & \rightsquigarrow
          & \{ x \overset{?}= t \} \cup [t/x]S \\
          &&& \text{ falls $x \in \Var(S) \setminus \Var(t)$}
      \end{array}
    \]
  \end{framed}
  Wenn keine Tranformationsregel mehr angewandt werden kann, so
  \begin{itemize}
    \item gib $\vec{T}$ zurück, falls die nach Anwendung aller Transformationen erhaltene Gleichungsmenge~$T$ in gelöster Form ist,
    \item ansonsten gib $\bot$ zurück.
  \end{itemize}
\end{alg}

% 4.6.6
\begin{lem}
  Falls $S \rightsquigarrow T$, so gilt $\Unifiers(S) = \Unifiers(T)$.
\end{lem}

% 4.6.7 und 4.6.10
\begin{thm}
  $\Call{unify}{S}$ ist korrekt:
  \begin{itemize}
    \item Der Algorithmus terminiert für alle Eingaben.
    \item Die Ausgabe ist eine idempotente, allgemeinste Lösung von~$S$ oder~$\bot$, falls~$S$ keine Lösung besitzt.
  \end{itemize}
\end{thm}

\begin{bem}
  Folgende Regeln bewirken einen frühen Abbruch:
  \begin{framed}
    \[
      \begin{array}{l r c l l}
        \text{Clash}
          & \{ f(\vec{s}) \overset{?}= g(\vec{t}) \} \sqcup S
          & \rightsquigarrow
          & \bot
          & \text{falls $f \neq g$} \\
        \text{Occurs-Check}
          & \{ x \overset{?}= t \} \sqcup S
          & \rightsquigarrow
          & \bot
          & \text{falls $x \in \Var(t)$} \\
          &&&& \text{und $x \neq t$}
      \end{array}
    \]
  \end{framed}
\end{bem}

% §4.7 Unifikation und Termumschreibung in ML

% (ausgelassen)

% §4.8 Unifikation auf Termgraphen

\begin{bem}
  Naive Implementierungen von Unifikation benötigen exponentielle Zeit.
  Es gibt einen Algorithmus auf Termgraphen, der nur (fast) lineare Zeit benötigt.
\end{bem}

% §5. Terminierung
\section{Terminierung}

% §5.1 Das Entscheidungsproblem

% §5.1.1 Unentscheidbarkeit des allgemeinen Falls

% ausgelassen: Def 5.1.1 (Turingmaschine)

\begin{problem}
  Gegeben ein Termumschreibungssystem~$R$, gibt es einen Algorithmus, der entscheidet, ob~$R$ terminierend ist oder nicht?
\end{problem}

% 5.1.7
\begin{thm}
  Dieses Problem ist im Allgemeinen unentscheidbar.
\end{thm}

\begin{beweisidee}
  Man kann Turingmaschinen als Termumschreibungs- systeme kodieren.
  Die Aussage folgt daraus, dass das das Halteproblem für Turingmaschinen unentscheidbar ist.
\end{beweisidee}

% §5.1.2 Ein entscheidbarer Unterfall

\begin{defn}
  Ein TUS~$R$ heißt \emph{rechtsseitig geschlossen}, falls für alle $(l \to r) \in R$ der rechte Term~$r$ geschlossen ist (\dh{} $\Var(r) = \emptyset$).
\end{defn}

% 5.1.8
\begin{lem}
  Sei~$R$ ein endliches, rechtsseitig geschlossenes Termumschreibungssystem.
  Dann sind äquivalent:
  \begin{itemize}
    \item $R$ ist \textit{nicht} terminierend
    \item Es gibt eine Regel $(l \to r) \in R$ und einen Term~$t$, sodass $r \strictlyReducesTo_R{t}$ und~$t$ den Subterm~$r$ besitzt.
  \end{itemize}
\end{lem}

% 5.1.9
\begin{thm}
  Für endliche, rechtsseitig geschlossene TUSe ist das Terminierungsproblem entscheidbar.
\end{thm}

\begin{beweisidee}
  Führe Breitensuche (gemäß $\to_R$) auf der Menge der Terme durch, beginnend bei der Wurzelmenge $\Set{r}{(l \to r) \in R}$.
  Falls~$R$ terminiert, so endet diese Suche.
  Ansonsten findet man bei der Suche in endlicher Zeit eine Verletzung von Punkt zwei aus dem vorherigen Lemma.
\end{beweisidee}

% §5.2 Reduktionsordnungen

% 5.2.1
\begin{defn}
  Eine strikte Ordnung~$>$ auf $T(\Sigma, V)$ heißt \emph{Umschreibungsordnung} (UO), falls sie
  \begin{itemize}
    \item \textit{kompatibel mit $\Sigma$-Operationen} ist, \dh{} aus $s > t$ folgt
    \[
      f(s_1, \ldots, s_{i-1}, s, s_{i+1}, \ldots, s_n) > f(s_1, \ldots, s_{i-1}, t, s_{i+1}, \ldots, s_n)
    \]
    \item und \textit{abgeschlossen unter Ersetzungen} ist, \dh{}
    \[
      s_1 > s_2 \implies \sigma(s_1) > \sigma(s_2).
    \]
  \end{itemize}
  Eine \emph{Reduktionsordnung} ist eine wohlfundierte Umschreibungsordnung.
\end{defn}

\begin{samepage}

% 5.2.3
\begin{thm}
  Für eine Termumschreibungssystem~$R$ sind äquivalent:
  \begin{itemize}
    \item $R$ terminiert.
    \item Es gibt eine Reduktionsordnung~$>$ mit $l > r$ für alle $(l \to r) \in R$.
  \end{itemize}
\end{thm}

% §5.3 Die Interpretationsmethode
\subsection{Die Interpretationsmethode}
  
\end{samepage}

% 5.3.3
\begin{lemdefn}
  Sei~$\Alg$ eine nichtleere $\Sigma$-Algebra und~$>$ eine wohlfundierte Ordnung auf deren Trägermenge~$A$.
  Angenommen, $f^\Alg : A^n \to A$ ist in jedem Argument streng monoton für alle $n \in \N$, $f \in \Sigma^{(n)}$.
  Dann definiert
  \[
    s >_\Alg t \coloniff \pi(s) > \pi(t) \text{ für alle Mor. $\pi : T(\Sigma, V) \to \Alg$}
  \]
  eine Reduktionsordnung auf $T(\Sigma, V)$.
\end{lemdefn}

% Polynomielle Ordnungen

\begin{defn}
  Eine \emph{polynomielle Interpretation} von~$\Sigma$ ist eine $\Sigma$-Algebra~$\Alg$ mit
  \begin{itemize}
    \item Trägermenge $A \subseteq \N \setminus \{ 0 \}$
    \item Es gilt $f^\Alg(a_1, \ldots, a_n) = P_f(a_1, \ldots, a_n)$ mit einem Polynom $P_f \in \N[X_1, \ldots, X_n]$ für alle $n \in \N$, $f \in \Sigma^{(n)}$.
  \end{itemize}
\end{defn}

\begin{defn}
  Ein Polynom $P \in \N[X_1, \ldots, X_n]$ heißt \emph{strikt monoton}, falls $P \not\in \N[X_1, \ldots, \widehat{X_i}, \ldots, X_n]$ für $i = 1, \ldots, n$.
\end{defn}

\begin{lemdefn}
  Sei~$\Alg$ eine polynomielle Interpretation~$\Alg$, deren Polynome~$P_f$ alle strikt monoton sind.
  Dann ist die von~$\Alg$ induziert Ordnung~$>_\Alg$ eine Reduktionsordnung.
  Solche Ordnungen auf~$T(\Sigma, V)$ heißen \emph{Polynomordnungen}.
\end{lemdefn}

% ausgelassen: Lemma 5.3.8

% 5.3.10
\begin{prop}
  Angenommen, die Terminierung eines TUS~$R$ kann mit einer Polynomordnung gezeigt werden.
  Dann gibt es eine Konstante $C > 0$, sodass für alle Terme~$t$ gilt, dass jede Reduktionssequenz ausgehend von~$t$ eine Länge $\leq 2^{2^{C \size{t}}}$ hat.
\end{prop}

% §5.4 Vereinfachungsordnungen
\subsection{Vereinfachungsordnungen}

% 5.4.1
\begin{defn}
  Eine Umschreibungsordnung~$>$ auf $T(\Sigma, V)$ heißt \emph{Verein- fachungsordnung}, falls sie die \emph{Subtermeigenschaft} erfüllt:
  \[
    \fa{t \in T(\Sigma, V)} \fa{p \in \Pos(t) \setminus \{ \epsilon \}} t > t|_p
  \]
\end{defn}

% 5.4.2
\begin{defn}
  Die \emph{homöomorphe Einbettung} ${\emb} \subseteq T(\Sigma, X) \times T(\Sigma, X)$ ist definiert durch die Schlussregeln
  \[
    \inferrule
      {x \in X}
      {x \emb x} \quad
    \inferrule
      {s_1 \emb t_1 \enspace \cdots \enspace s_n \emb t_n}
      {f(s_1, \ldots, s_n) \emb f(t_1, \ldots, t_n)} \quad
    \inferrule
      {s_j \emb t \enspace (1 \leq j \leq n)}
      {f(s_1, \ldots, s_n) \emb t}
  \]
\end{defn}

\begin{bem}
  Es gilt ${\emb} = {\reducesTo}_R$ mit dem Termumschreibungssystem
  \[
    R \coloneqq \Set{f(x_1, \ldots, x_n) \to x_i}{n \in \N, f \in \Sigma^{(n)}, 1 \leq i \leq n}
  \]
  Da~$R$ terminiert ist ${\emb}$ wohlfundiert.
  Für $\Sigma$, $X$ endlich gilt sogar:
\end{bem}

\begin{lem}
  Eine \emph{Wohlpartialordnung} ist eine Partialordnung~$\geq$ mit der Eigenschaft, dass es in jeder unendlichen Folge $x_1, x_2, \ldots$ Indizes $i < j$ mit $x_i \leq x_j$ gibt.
\end{lem}

\begin{bem}
  Wohlpartialordnungen sind wohlfundiert.
\end{bem}

% ausgelassen: Lemmas 5.4.4 und 5.4.5

\begin{thm}[\emph{Kruskal}]
  Sei~$\Sigma$ eine endliche Signatur und~$X$ eine endliche Variablenmenge.
  Dann ist ${\strictlyEmb}$ eine Wohlpartialord. auf~$T(\Sigma, X)$.
\end{thm}

\begin{lem}
  Sei~${>}$ eine Vereinfachungsordnung auf~$T(\Sigma, V)$.
  Dann gilt
  \[
    s \emb t \implies s \geq t \qquad
    \text{für alle $s, t \in T(\Sigma, V)$.}
  \]
\end{lem}

% 5.4.8
\begin{thm}
  Sei~$\Sigma$ endlich.
  Jede Vereinfachungsordnung~${>}$ auf $T(\Sigma, V)$ ist wohlfundiert, also eine Reduktionsordnung.
\end{thm}

% 5.4.10
\begin{prop}
  Sei~${>}$ eine Reduktionsord. auf~$T(\Sigma, V)$, deren Einschränkung auf~$T(\Sigma, \emptyset)$ total ist.
  Dann erfüllt~${>}$ die Subtermeig. für~$t \in T(\Sigma, \emptyset)$.
\end{prop}

% §5.4.1 Polynomielle Vereinfachungsordnungen

\begin{defn}
  Eine \emph{polynomielle Interpretation über~$\R$} von~$\Sigma$ ist eine $\Sigma$-Algebra~$\Alg$ mit
  \begin{itemize}
    \item nichtleerer Trägermenge $A \subseteq \R$ und
    \item $f^\Alg(a_1, \ldots, a_n) = P_f(a_1, \ldots, a_n)$ mit einem Polynom $P_f \in \R[X_1, \ldots, X_n]$ für alle $n \in \N$, $f \in \Sigma^{(n)}$
  \end{itemize}
  sodass folgende Eigenschaften erfüllt sind:
  \begin{itemize}
    \item Für alle $n \in \N$, $f \in \Sigma^{(n)}$ und $a, b, a_1, \ldots, a_n \in A$ mit $a > b$ gilt
    \[
      P_f(a_1, \nldots, a_{i-1}, a, a_{i+1}, \nldots, a_n) > P_f(a_1, \nldots, a_{i-1}, b, a_{i+1}, \nldots, a_n).
    \]
    \item Für alle $n \in \N$, $f \in \Sigma^{(n)}$ und $a_1, \ldots, a_n \in A$ gilt
    \[
      P_f(a_1, \ldots, a_n) > \max \{ a_1, \ldots, a_n \}.
    \]
  \end{itemize}
\end{defn}

\begin{beob}
  Sei~$\Sigma$ endlich.
  Dann ist die von~$A$ induzierte \emph{polynomielle Vereinfachungsordnung}~$>_\Alg$ eine Reduktionsordnung.
\end{beob}

\begin{bem}
  Ist $A$ in der Theorie der reellen Zahlen in Prädikatenlogik erster Stufe beschrieben, so sind die beiden Eigenschaften aus der Definition sowie ${>_\Alg}$ entscheidbar.
\end{bem}

% §5.4.2 Rekursive Pfadordnungen

\begin{defn}
  Die durch eine strikte Ordnung~${>}$ auf~$\Sigma$ induzierte \emph{lexiko- graphische Pfadordnung}~${\strictLpo}$ ist def. durch $s \strictLpo t \coloniff\,$
  \begin{itemize}
    \item $t \in \Var(s)$ und $s \neq t$ \textit{oder}
    \item $s = f(s_1, \ldots, s_m)$, $t = g(t_1, \ldots, t_n)$ und
    \begin{itemize}
      \item $\ex{i} s_i \lpo t$ \textit{oder}
      \item $f > g$ und $\fa{j} s \strictLpo t_j$ \textit{oder}
      \item $f = g$ und $\fa{j} s \strictLpo t_j$ und \\
      \emph{($\star$)} $\ex{i} s_1 = t_1 \wedge \ldots \wedge s_{i-1} = t_{i-1} \wedge s_i \strictLpo t_i$
    \end{itemize}
  \end{itemize}
\end{defn}

\begin{thm}
  Sei~$\Sigma$ endlich.
  Die lexikographische Pfadordnung ${\lpo}$ ist eine Vereinfachungsordnung auf~$T(\Sigma, V)$.
\end{thm}

% 5.4.16
\begin{prop}
  $s \lpo t$ ist in polynomieller Zeit (in~$s$ und~$t$) entscheidbar.
  % ausgelassen: Teil 2
\end{prop}

\begin{bemn}
  \begin{itemize}
    \item Ersetzt man \emph{($\star$)} in der Def. der lex. Pfadordnung durch
    \[
      \{ s_1, \ldots, s_m \} \strictMpo^\text{mul} \{ t_1, \ldots, t_n \},
    \]
    wobei ${\strictMpo^\text{mul}}$ die von ${\strictMpo}$ induzierte Multimengenordnung ist, so erhält man die \emph{Multimengenpfadordnung}~${\strictMpo}$.
    \item Man kann auch "`gemischte"' Pfadordnungen bilden, bei denen je nach Signatur~$f = g \in \Sigma$ die lexikographische oder die Multimengenordnung für die Subterme $s_1, \ldots, s_m, t_1, \ldots, t_n$ verwendet wird.
  \end{itemize}
\end{bemn}

% §5.4.3 Pfadordnungen in ML

% (ausgelassen)

% §5.4.4 Knuth-Bendix-Ordnungen

\begin{defn}
  Sei~$\Sigma$ endlich, $w : \Sigma \cup V \to \R_{\geq 0}$ eine \emph{Gewichtsfunktion} und~${>}$ eine strikte Ordnung auf~$\Sigma$.
  Es gelte:
  \begin{itemize}
    \item $\ex{w_0 > 0} \fa{v \in V} w(v) = w_0 \wedge \fa{c \in \Sigma^{(0)}} w(c) \geq w_0$
    \item $\fa{f \in \Sigma^{(1)}} w(f) = 0 \implies f \geq g$
  \end{itemize}
  Die \emph{Knuth-Bendix-Ordnung}~${\kbo}$ induziert durch~${>}$ und~$w$ ist definiert durch: $s \kbo t \coloniff\,$
  \begin{itemize}
    \item $\fa{x \in V} \size{s}_x \geq \size{t}_x$ und $w(s) > w(t)$ \textit{oder}
    \item $\fa{x \in V} \size{s}_x \geq \size{t}_x$ und $w(s) = w(t)$ \textit{und}
    \begin{itemize}
      \item $\ex{f \in \Sigma^{(1)}} \ex{n \in \N_{> 0}} s = f^n(t)$ und $t \in X$ \textit{oder}
      \item $s = f(\cdots)$, $t = g(\cdots)$ und $f > g$ \textit{oder}
      \item $s = f(s_1, \ldots, s_n)$, $t = f(t_1, \ldots, t_n)$ und $\ex{i} s_1 = t_1 \wedge \ldots \wedge s_{i-1} = t_{i-1} \wedge s_i \kbo t_i$
    \end{itemize}
  \end{itemize}
\end{defn}

% ausgelassen: Prop 5.4.19

% 5.4.20
\begin{thm}
  ${\kbo}$ ist eine Vereinfachungsordnung.
\end{thm}

% ausgelassen: Lemmas 5.4.21, 5.4.22, 5.4.23, 5.4.

% 5.4.26
\begin{prop}
  $s \kbo t$ ist in polynomieller Zeit (in~$s$ und~$t$) entscheidbar.
  % zweiter Teil ausgelassen
\end{prop}

% §6. Konfluenz
\section{Konfluenz}

% §6.1 Das Entscheidungsproblem

\begin{problem}[\emph{Konfluenz}]
  Gegeben ein TUS~$R$.
  Frage: Ist~$R$ konfluent?
\end{problem}

% 6.1.1
\begin{satz}
  Das Konfluenz-Problem ist unentscheidbar.
\end{satz}

\begin{beweisskizze}
  Sei $E$ eine Gleichungsmenge mit $\Var(l) = \Var(r)$ für alle $l \ident r \in E$ und unentscheidbarem Grundwortproblem über~$E$.
  Für Terme $t, s \in T(\Sigma, \emptyset)$ betrachte das TUS
  \[ R_{st} \coloneqq E \cup E^{-1} \cup \{ a \to s, a \to t \}. \]
  Dann gilt: $R_{st}$ ist konfluent $\iff$ $t \ident_E s$
\end{beweisskizze}

% §6.2
\subsection{Kritische Paare}

\begin{situation}
  Angenommen, der Term $s$ wird für $i = 1, 2$ mittels $l_i \to r_i \in R$ zu~$t_i$ umgeschrieben, \dh{} es gibt je eine Position~$p_i$ und eine Ersetzung $\sigma_i$ mit
  \[
    s|_{p_i} = \sigma_i l_i
    \enspace \text{und} \enspace
    t_i = s [\sigma_i r_i]_{p_i}.
  \]
  Um lokale Konfluenz nachzuweisen, müssen wir zeigen, dass $t_1 \joinable t_2$. \\
  Wir können drei Fälle unterscheiden:
  \begin{enumerate}
    \item
      $s|_{p_1}$ und $s|_{p_2}$ sind zwei disjunkte Subterme von~$s$, \\
      \dh{} weder~$p_1$ ist ein Präfix von~$p_2$, noch umgekehrt
    \item
      $s|_{p_2}$ ist ein Subterm von $s|_{p_1}$ (bzw. umgekehrt), \\
      \dh{} $p_2 = p_1 p$ für ein möglicherweise leeres $p \in \N^*$
      \begin{enumerate}
        \item
          \emph{Nichkritischer Überlapp}:
          $s|_{p_2}$ ist Subterm einer ersetzten Variable in~$l_1$,
          \dh{} $p = q_1 q_2$, wobei $l_i|_{q_1} \in V$.
        \item
          \emph{Kritischer Überlapp}:
          $l_1$ und $l_2$ überlappen, \\
          \dh{} $p \in \Pos(l_1)$ und $l_1|_p \not\in V$.
      \end{enumerate}
  \end{enumerate}
\end{situation}

\begin{lem}
  \begin{itemize}
    \item In den Fällen 1 und 2a gilt $t_1 \joinable t_2$.
    \item Im Fall 2b gilt $t_1 \joinable t_2$, falls $t_1|_{p_1} \!\!=\! \sigma_1 r_1 \,\,\joinable\,\, t_2|_{p_1} \!=\! (s|_{p_1}) [\sigma_2 r_2]_p$.
  \end{itemize}
\end{lem}

% 6.2.1
\begin{defn}
  Seien $l_1 \to r_1, l_2 \to r_2 \in E$ Regeln mit so umbenannten Variablen, dass $(\Var(l_1) \cup \Var(r_1)) \cap (\Var(l_2) \cup \Var(r_2)) = \emptyset$. \\
  Sei $p \in \Pos(l_1)$ mit $l_1|_p \not\in V$ und~$\theta$ eine allgemeinste Lösung von $l_1|_p =^{?} l_2$.
  Dann heißt $(\theta r_1, (\theta l_1)[\theta r_2]_p)$ ein \emph{kritisches Paar}.
\end{defn}

\begin{acht}
  Bei den beiden Regeln $l_1 \to r_1$ und $l_2 \to r_2$ kann es sich auch um Kopien derselben Regel handeln!
\end{acht}

% Lemma 6.2.3
\begin{beob}
  Im Fall 2b gibt es ein kritisches Paar $(k_1, k_2)$ (konstruiert aus den beiden gegebenen Gleichungen zusammen mit~$p$ wie oben) und eine Ersetzung~$\tau$ mit $t_1|_{p_1} = \tau k_1$ und $t_2|_{p_1} = \tau k_2$.
\end{beob}

% 6.2.4
\begin{satz}
  Ein TUS ist genau dann lokal konfluent, falls für alle kritischen Paare $(k_1, k_2)$ gilt, dass $k_1 \joinable k_2$.
\end{satz}

% 6.2.5
Da für terminierende TUS Konfluenz und lokale Konfluenz übereinstimmen, folgt:

% 6.2.6
\begin{kor}
  Die Konfluenz eines endlichen, terminierenden TUS ist entscheidbar.
\end{kor}

\begin{beweisskizze}
  Es gibt nur endlich viele kritische Paare $(k_1, k_2)$ bis auf $\alpha$-Äquivalenz.
  Prüfe für jedes solche Paar, ob $\NF{k_1} = \NF{k_2}$.
  \begin{itemize}
    \item Falls ja: Dann gilt $k_1 \joinable k_2$.
    \item Falls nein: Dann ist das TUS nicht konfluent, denn es gilt: \\
    $(\NF{k_1}) \reducesFrom k_1 \from l_1 \to k_2 \reducesTo (\NF{k_2})$ aber nicht $(\NF{k_1}) \joinable (\NF{k_2})$.
  \end{itemize}
\end{beweisskizze}

% ausgelassen: Abschnitt über kritische Paare in ML

% §6.3 Orthogonalität
\subsection{Orthogonalität}

% 6.3.1
\begin{defn}
  Eine Umschreibungsregel $l \to r$ heißt \emph{links-/ rechts-linear}, falls jede Variable auf der linken/rechten Seite höchstens ein Mal auftritt.
  Sie heißt \emph{linear}, falls sie links- und rechts-linear ist. \\
  Ein TUS~$R$ ist (links-/rechts-) linear, falls alle Regeln es sind.
\end{defn}

% 6.3.2
\begin{defn}
  Zwei Terme $s_1$, $s_2$ heißen \emph{stark zusammenführbar}, falls
  \[
    \ex{t_1, t_2} \quad
    s_1 \toOrEq{} t_1 \reducesFrom{} s_2
    \quad \wedge \quad
    s_1 \reducesTo{} t_2 \fromOrEq{} s_2.
  \]
\end{defn}

% 6.3.3
\begin{lem}[\emph{Starke-Konfluenz-Lemma}]
  Ist $R$ linear und ist jedes kritische Paar in~$R$ stark zusammenführbar, so ist~$R$ stark konfluent.
\end{lem}

% 6.3.6
\begin{defn}
  Ein TUS heißt \emph{orthogonal}, falls es links-linear ist und keine kritischen Paare besitzt.
\end{defn}

% 6.3.7
\begin{defn}
  \begin{itemize}
    \item Eine Menge~$P$ von Positionen heißt \emph{parallel}, falls $p \parallel q$ für alle $p, q \in P$ mit $p \not= q$.
    \item
      Sei $s$ ein Term und $P = \{ p_1, \ldots, p_n \} \subseteq \Pos(s)$ parallel. \\
      Sei ein Term $t_p$ für jedes $p \in P$ gegeben.
      Dann ist
      \[ s[t_p]_{p \in P} \coloneqq s[t_{p_1}]_{p_1} \cdots [t_{p_n}]_{p_n} \]
    \item
      Sei für jedes $p \in P$ eine Regel $l_p \to r_p \in R$ und eine Ersetzung~$\sigma_p$ mit $s|_p = \sigma_p l_p$ gegeben.
      Dadurch ist ein
      \[
        \text{\emph{paralleler Reduktionsschritt}} \qquad
        s \, \parallelTo_R^P \, s [\sigma_p r_p]_{p \in P}
      \]
      gegeben.
      Die so definierte Reduktion ist
      \[
        {\parallelTo} \coloneqq {\parallelTo_R} \coloneqq \cup_{s \in T(\Sigma, V)} \cup_{P \subseteq \Pos(s)} \Set{(s, t)}{s \parallelTo_R^P t}.
      \]
  \end{itemize}
\end{defn}

\begin{fakt}
  ${\to} \subseteq {\parallelTo} \subseteq {\reducesTo}$
\end{fakt}

% ausgelassen: Lemma 6.3.9

\begin{thm}
  Ist~$R$ orthogonal, so hat ${\parallelTo}_R$ die Diamant-Eigenschaft.
\end{thm}

% 6.3.11
\begin{kor}
  Jedes orthogonale TUS ist konfluent.
\end{kor}

% 6.3.13
\begin{defn}
  Ein TUS~$R$ ist ein \emph{Konstruktor-TUS}, falls eine Zerlegung $\Sigma = \Sigma_c \sqcup \Sigma_d$ existiert, sodass
  $l = f(t_1, \ldots, t_m)$ mit $f \in \Sigma_d^{(n)}$ und $t_1, \ldots, t_m \in T(\Sigma_c, V)$ für jedes $l \to r \in R$.
\end{defn}

\begin{bem}
  Jedes Programm in einer ML-artigen funktionalen Programmiersprache lässt sich als Konstruktor-TUS schreiben.
  Dieses hat genau dann keine kritischen Paare, falls keine zwei Definitionen überlappen.
  Es folgt, dass die Auswertung in funktionalen Programmiersprachen deterministisch ist.
\end{bem}

% §6.4. Beyond orthogonality

% 6.4.5
\begin{defn}
  Ein TUS heißt \emph{parallel abgeschlossen}, falls $u_2 \parallelTo u_1$ für alle kritischen Paare $(u_1, u_2)$ gilt.
\end{defn}

% ausgelassen: Definition 6.4.6 und Lemma 6.4.7

% 6.4.8
\begin{thm}
  Ist $R$ links-linear und parallel abgeschlossen, so besitzt ${\parallelTo}$ die Diamant-Eigenschaft.
\end{thm}

% 6.4.9
\begin{kor}
  Links-lineare, parallel abgeschlossene TUSe sind konfluent.
\end{kor}

\end{document}