diff --git a/merkzettel.pdf b/merkzettel.pdf index 4141eb4..d2c5758 100644 Binary files a/merkzettel.pdf and b/merkzettel.pdf differ diff --git a/merkzettel.tex b/merkzettel.tex index 9ab7113..7d013ba 100644 --- a/merkzettel.tex +++ b/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}