Anmerkungen am Rand, Makros

This commit is contained in:
Marco Ammon 2018-10-03 14:22:06 +02:00
parent ede8472ae3
commit 3d1a0f1a4d
2 changed files with 11 additions and 2 deletions

Binary file not shown.

View File

@ -20,7 +20,14 @@
\usetikzlibrary{positioning} \usetikzlibrary{positioning}
\usetikzlibrary{arrows.meta} \usetikzlibrary{arrows.meta}
%Anmerkungen am Rand
\newcommand{\siehe}[1]{\marginpar{\footnotesize \textit{#1}}} \newcommand{\siehe}[1]{\marginpar{\footnotesize \textit{#1}}}
\newcommand{\satz}[2]{\marginpar{\footnotesize \textit{Satz~#1 (#2)}}}
\newcommand{\defin}[2]{\marginpar{\footnotesize \textit{Def.~#1 (#2)}}}
\newcommand{\kor}[2]{\marginpar{\footnotesize \textit{Kor.~#1 (#2)}}}
\newcommand{\lem}[2]{\marginpar{\footnotesize \textit{Lem.~#1 (#2)}}}
%Abkürzungen für Symbole, Reduktionen, etc.
\newcommand{\app}{\ensuremath{\rightarrow_a}} \newcommand{\app}{\ensuremath{\rightarrow_a}}
\newcommand{\norm}{\ensuremath{\rightarrow_n}} \newcommand{\norm}{\ensuremath{\rightarrow_n}}
@ -44,19 +51,21 @@
\subsubsection*{Rekursion} \subsubsection*{Rekursion}
\subsubsection*{Auswertungsstrategien} \subsubsection*{Auswertungsstrategien}
\begin{itemize} \begin{itemize}
\item applikativ (\textit{leftmost-innermost}) \app \item applikativ (\textit{leftmost-innermost}) \app \defin{3.13}{33}
\begin{itemize} \begin{itemize}
\item $\lambda x.t \app \lambda x.t'$, wenn $t \app t'$ \item $\lambda x.t \app \lambda x.t'$, wenn $t \app t'$
\item $ts \app t's$, wenn $t \app t'$ \item $ts \app t's$, wenn $t \app t'$
\item $ts \app ts'$, wenn $s\app s'$ und $t$ normal ist \item $ts \app ts'$, wenn $s\app s'$ und $t$ normal ist
\item $(\lambda x.t)s \app t\lbrack s/x\rbrack$, wenn $t$ und $s$ normal sind \item $(\lambda x.t)s \app t\lbrack s/x\rbrack$, wenn $t$ und $s$ normal sind
\item effizient
\end{itemize} \end{itemize}
\item normal (\textit{leftmost-outermost}) \norm \item normal (\textit{leftmost-outermost}) \norm \defin{3.14}{34}
\begin{itemize} \begin{itemize}
\item $(\lambda x.t) s \norm t\lbrack s/x\rbrack$ \item $(\lambda x.t) s \norm t\lbrack s/x\rbrack$
\item $\lambda x.t \norm \lambda x.t'$, wenn $t\norm t'$ \item $\lambda x.t \norm \lambda x.t'$, wenn $t\norm t'$
\item $ts \norm t's$m wenn $t\norm t'$ und $t$ keine $\lambda$-Abstraktion ist \item $ts \norm t's$m wenn $t\norm t'$ und $t$ keine $\lambda$-Abstraktion ist
\item $ts \norm ts'$, wenn $s\norm s'$ und $t$ normal und keine $\lambda$-Abstraktion ist \item $ts \norm ts'$, wenn $s\norm s'$ und $t$ normal und keine $\lambda$-Abstraktion ist
\item terminiert immer, falls Normalform existiert (nach Standardisierungssatz) \satz{3.17}{35}
\end{itemize} \end{itemize}
\end{itemize} \end{itemize}
\subsection*{Getypt} \subsection*{Getypt}