TES

merkzettel.tex

@@ -40,7 +40,7 @@
 \theoremstyle{definition}
 \newtheorem{definition}{Definition}[section]
 
-\title{Merkzettel für \enquote{Theorie der Programmierung}}
+\title{Merkzettel für \enquote{Theorie~der~Programmierung}}
 \author{Marco Ammon}
 \date{\today}
 
@@ -48,10 +48,19 @@
 \maketitle
 \section*{Termersetzungssysteme}
 \subsection*{Terminierung}
+\satz{2.31}{15}
+Sei $>$ Reduktionsordnung, und es gelte: $\forall t,s.t\rightarrow_0 s \Rightarrow t>s$. Dann ist $\rightarrow$ stark normalisierend. 
 \subsubsection*{Polynomordnungen}
+\kor{2.44}{18}
+Wir definieren $A \subseteq \mathbb{N}$ und für jede $n$-stellige Operation $f$ ein Polynom $p_f(x_1,\ldots, x_n)$. Wenn die linken Seiten der Umformungsregeln $>_A$ den rechten sind, ist das zugehörige TES stark normalisierend.
 \subsection*{Konfluenz}
-\subsection*{Critical Pairs}
-
+\subsubsection*{Critical Pairs}
+\begin{itemize}
+	\item Definition kritisches Paar: \defin{2.55}{22}\\
+	Seien $l_1 \rightarrow_0 r_1$ und $l_2 \rightarrow r_2$ zwei Umformungsregeln des TES sowie $FV)(l_1) \cap FV(l_2) = \emptyset$ (ggf. nach Umbenennung). Sei $l_1 = C(t)$, wobei $t$ nicht nur eine Variable ist, so dass $t$ und $l_2$ unifizierbar sind. Sei $\sigma = mgu(t, l_2)$. Dann heißt $(r_1\sigma, C(r_2)\sigma)$ ein kritisches Paar.	
+	\item Ein TES $T$ ist genau dann lokal konfluent, wenn in $T$ alle kritischen Paare zusammenführbar sind. \satz{2.60}{24}
+	\item Ein stark normalisierendes und lokal konfluentes TES ist konfluent. \satz{2.51}{21}
+\end{itemize}
 \section*{$\lambda$-Kalkül}
 \subsection*{Ungetypt}
 \begin{itemize}