minor bugfixes
This commit is contained in:
parent
e628beea2e
commit
0c6a8c5622
Binary file not shown.
@ -1919,8 +1919,10 @@ Variablen:
|
|||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
|
|
||||||
Komplexe Datenstrukturen:
|
Komplexe Datenstrukturen:
|
||||||
|
\begin{lstlisting}
|
||||||
|
[{{person,'Joe', 'Armstrong'}, {telephoneNumber, [3,5,9,7]}, {shoeSize, 42}, {pets, [{cat, tubby},{cat, tiger}]}, {children,[{thomas, 5},{claire,1}]}}, {{person,'Mike','Williams'}, {shoeSize,41}, {likes,[boats, beer]}, ...}]
|
||||||
|
\end{lstlisting}
|
||||||
\begin{itemize*}
|
\begin{itemize*}
|
||||||
\item $[\{\{person,'Joe', 'Armstrong'\}, \{telephoneNumber, [3,5,9,7]\}, \{shoeSize, 42\}, \{pets, [\{cat, tubby\},\{cat, tiger\}]\}, \{children,[\{thomas, 5\},\{claire,1\}]\}\}, \{\{person,'Mike','Williams'\}, \{shoeSize,41\}, \{likes,[boats, beer]\}, ... \}]$
|
|
||||||
\item Erläuterungen:
|
\item Erläuterungen:
|
||||||
\begin{itemize*}
|
\begin{itemize*}
|
||||||
\item Beliebig komplexe Strukturen können erzeugt werden
|
\item Beliebig komplexe Strukturen können erzeugt werden
|
||||||
@ -2253,13 +2255,14 @@ Ein Lambda-Term ohne freie Variablen heißt Kombinator
|
|||||||
|
|
||||||
\subitem\colorbox{lightgray}{
|
\subitem\colorbox{lightgray}{
|
||||||
\begin{minipage}[h]{0.9\linewidth}
|
\begin{minipage}[h]{0.9\linewidth}
|
||||||
$\lambda$-Terme\\ \\
|
$\lambda$-Terme\\
|
||||||
\begin{tabular}[h]{lcr}
|
\begin{tabular}[h]{lcr}
|
||||||
\textbf {Bezeichnung} & \textbf{Notation} & \textbf{Beispiele} \\
|
\textbf {Bezeichnung} & \textbf{Notation} & \textbf{Beispiele} \\
|
||||||
Variablen & $x$ & $x \enspace y$ \\
|
Variablen & $x$ & $x \enspace y$ \\
|
||||||
Abstraktion & $\lambda$x.t & $\lambda y.0 \enspace \lambda f. \lambda x. \lambda y.fyx$ \\
|
Abstraktion & $\lambda$x.t & $\lambda y.0 \enspace \lambda f. \lambda x. \lambda y.fyx$ \\
|
||||||
Funktionsanwendung & $t_1t_2$ & $f 42 \enspace ( \lambda x.x+5)7$
|
Funktionsanwendung & $t_1t_2$ & $f 42 \enspace ( \lambda x.x+5)7$
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
|
|
||||||
(weitere primitive Operationen nach Bedarf) 17, True, +, ·
|
(weitere primitive Operationen nach Bedarf) 17, True, +, ·
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
}
|
}
|
||||||
@ -2328,13 +2331,13 @@ $$(\lambda x.\lambda y.\lambda z.f( \lambda x.z+x)(y x)) (\lambda y.y+x)$$
|
|||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
|
|
||||||
\subsubsection{Ausführung von $\lambda$ Termen}
|
\subsubsection{Ausführung von Lambda-Termen}
|
||||||
\colorbox{lightgray}{ \begin{minipage}[h]{1.0\linewidth}
|
\colorbox{lightgray}{ \begin{minipage}[h]{.9\linewidth}
|
||||||
\begin{tabular}{|p{4cm}|p{7cm}|}
|
\begin{tabular}{ l | l }
|
||||||
Redex & Ein $\lambda$-Term der Form ($\lambda x.t_1)t_2$ heißt Redex. \\[\normalbaselineskip]
|
Redex & Ein $\lambda$-Term der Form ($\lambda x.t_1)t_2$ heißt Redex. \\
|
||||||
$\beta$-Reduktion & entspricht der Ausführung der Funktionanwendung auf einem Redex: \\[\normalbaselineskip]
|
$\beta$-Reduktion & entspricht der Ausführung der Funktionanwendung auf einem Redex: \\
|
||||||
& ($\lambda x.t_1)t_2 \Rightarrow t_1[x \rightarrow t_2]$ \\[\normalbaselineskip]
|
& ($\lambda x.t_1)t_2 \Rightarrow t_1[x \rightarrow t_2]$ \\
|
||||||
Substitution & $t_1[x \rightarrow t_2]$ erhält man aus dem Term $t_1$, wenn man alle freien Vorkommen von x durch $t_2$ ersetzt. \\[\normalbaselineskip]
|
Substitution & $t_1[x \rightarrow t_2]$ erhält man aus dem Term $t_1$, wenn man alle freien Vorkommen von x durch $t_2$ ersetzt. \\
|
||||||
Normalform & Ein Term, der nicht weiter reduziert werden kann, heißt in Normalform
|
Normalform & Ein Term, der nicht weiter reduziert werden kann, heißt in Normalform
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
@ -2364,7 +2367,7 @@ Namen gebundener Variablen
|
|||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
|
|
||||||
\colorbox{lightgray}{
|
\colorbox{lightgray}{
|
||||||
\begin{minipage}[h]{1.0\linewidth}
|
\begin{minipage}[h]{.9\linewidth}
|
||||||
$\alpha$-Äquivalenz \\
|
$\alpha$-Äquivalenz \\
|
||||||
$t_1$ und $t_2$ heißen $\alpha$-Äquivalent ($t_1 \stackrel{\alpha}{=} t_2$), wenn $t_1$ in $t_2$ durch konsistente Umbenennung der $\lambda$-gebundenen Variablen überführt werden kann.
|
$t_1$ und $t_2$ heißen $\alpha$-Äquivalent ($t_1 \stackrel{\alpha}{=} t_2$), wenn $t_1$ in $t_2$ durch konsistente Umbenennung der $\lambda$-gebundenen Variablen überführt werden kann.
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
@ -2388,9 +2391,9 @@ Extensionalitäts-Prinzip:
|
|||||||
\item Zwei Funktionen sind gleich, falls Ergebnis gleich für alle Argumente
|
\item Zwei Funktionen sind gleich, falls Ergebnis gleich für alle Argumente
|
||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
\colorbox{lightgray} {
|
\colorbox{lightgray} {
|
||||||
\begin{minipage}[h]{1.0\linewidth}
|
\begin{minipage}[h]{.9\linewidth}
|
||||||
$\eta$-Äquivalenz \\
|
$\eta$-Äquivalenz \\
|
||||||
Terme $\lambda$x.fx und f heißen $\eta$-äquivalent ($\lambda$x.fx $\stackrel{\eta}{=}$ f), falls x nicht freie Variable von f ist.
|
Terme $\lambda x.fx$ und f heißen $\eta$-äquivalent ($\lambda x.fx \stackrel{\eta}{=} f$), falls x nicht freie Variable von f ist.
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -2520,7 +2523,7 @@ $$\omega = (\lambda \color{blue}x.x x\color{black})\color{red}(\lambda x.x x) \c
|
|||||||
$\lambda x.xx$ wendet sein Argument auf das Argument selbst an $\Rightarrow$ dadurch reproduziert $\omega$ sich selbst.
|
$\lambda x.xx$ wendet sein Argument auf das Argument selbst an $\Rightarrow$ dadurch reproduziert $\omega$ sich selbst.
|
||||||
|
|
||||||
\colorbox{lightgray}{
|
\colorbox{lightgray}{
|
||||||
\begin{minipage}[h]{1.0\linewidth}
|
\begin{minipage}[h]{.9\linewidth}
|
||||||
Divergenz: \\
|
Divergenz: \\
|
||||||
Terme, die nicht zu einer Normalform auswerten, divergieren.
|
Terme, die nicht zu einer Normalform auswerten, divergieren.
|
||||||
Diese modellieren unendliche Ausführungen.
|
Diese modellieren unendliche Ausführungen.
|
||||||
@ -2529,7 +2532,7 @@ $\lambda x.xx$ wendet sein Argument auf das Argument selbst an $\Rightarrow$ dad
|
|||||||
|
|
||||||
\subsubsection{Der Fixpunktsatz}
|
\subsubsection{Der Fixpunktsatz}
|
||||||
\colorbox{lightgray}{
|
\colorbox{lightgray}{
|
||||||
\begin{minipage}[h]{1.0\linewidth}
|
\begin{minipage}[h]{.9\linewidth}
|
||||||
Fixpunktsatz \\
|
Fixpunktsatz \\
|
||||||
Für alle $F\in\Lambda$ existiert ein $X\in\lambda$ sodass gilt: $F X = X$
|
Für alle $F\in\Lambda$ existiert ein $X\in\lambda$ sodass gilt: $F X = X$
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
@ -2570,7 +2573,7 @@ $\lambda x.xx$ wendet sein Argument auf das Argument selbst an $\Rightarrow$ dad
|
|||||||
|
|
||||||
\subsubsection{Der Fixpunkt-Kombinator}
|
\subsubsection{Der Fixpunkt-Kombinator}
|
||||||
\colorbox{lightgray}{
|
\colorbox{lightgray}{
|
||||||
\begin{minipage}[h]{1.0\linewidth}
|
\begin{minipage}[h]{.9\linewidth}
|
||||||
Im Ergebnis unserer Diskussion des Fixpunktsatzes definieren wir den Fixpunkt-Kombinator wie folgt: $$Y \equiv \lambda f.(\lambda x.f(xx)) (\lambda x.f(xx))$$
|
Im Ergebnis unserer Diskussion des Fixpunktsatzes definieren wir den Fixpunkt-Kombinator wie folgt: $$Y \equiv \lambda f.(\lambda x.f(xx)) (\lambda x.f(xx))$$
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
}
|
}
|
||||||
@ -2678,7 +2681,7 @@ d.h. \space\space\space Yf ist Fixpunkt von f
|
|||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
|
|
||||||
\colorbox{lightgray}{\begin{minipage}[h]{1.0\linewidth}
|
\colorbox{lightgray}{\begin{minipage}[h]{.9\linewidth}
|
||||||
Definition: \\
|
Definition: \\
|
||||||
Die Klasse der rekursiven Funktionen ist die kleinste Klasse numerischer Funktionen, die alle oben genannten Anfangsfunktionen enthält und abgeschlossen ist unter Komposition, primitiver Rekursion und unbeschränkter Minimalisierung
|
Die Klasse der rekursiven Funktionen ist die kleinste Klasse numerischer Funktionen, die alle oben genannten Anfangsfunktionen enthält und abgeschlossen ist unter Komposition, primitiver Rekursion und unbeschränkter Minimalisierung
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
@ -2726,7 +2729,7 @@ d.h. \space\space\space Yf ist Fixpunkt von f
|
|||||||
\begin{itemize*}
|
\begin{itemize*}
|
||||||
\item Aus den Lemmata 1 bis 3 folgt nun der Satz:\\
|
\item Aus den Lemmata 1 bis 3 folgt nun der Satz:\\
|
||||||
\colorbox{lightgray}{
|
\colorbox{lightgray}{
|
||||||
\begin{minipage}[h]{1.0\linewidth}
|
\begin{minipage}[h]{.9\linewidth}
|
||||||
Alle rekursiven Funktionen sind Lambda-definierbar
|
Alle rekursiven Funktionen sind Lambda-definierbar
|
||||||
\end{minipage}}
|
\end{minipage}}
|
||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
@ -2756,7 +2759,7 @@ d.h. \space\space\space Yf ist Fixpunkt von f
|
|||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
\item Eine weitere Kernfrage: Angenommen mehrere unterschiedliche Reduktionsreihenfolgen führen zu einem nicht weiter zu reduzierenden Ergebnis - \color{blue} führen all diese Reihenfolgen zum gleichen Ergebnis? \color{black}
|
\item Eine weitere Kernfrage: Angenommen mehrere unterschiedliche Reduktionsreihenfolgen führen zu einem nicht weiter zu reduzierenden Ergebnis - \color{blue} führen all diese Reihenfolgen zum gleichen Ergebnis? \color{black}
|
||||||
\item Wir definieren zuerst einen zentralen begriff in diesem Zusammenhang:
|
\item Wir definieren zuerst einen zentralen begriff in diesem Zusammenhang:
|
||||||
\colorbox{lightgray}{\begin{minipage}[h]{1.0\linewidth}
|
\colorbox{lightgray}{\begin{minipage}[h]{.9\linewidth}
|
||||||
Ein Transitiosnsystem $(D,\rightarrow*)$ heißt genau dann konfluent, wenn für alle $t,t_1,t_2 \in D$ gilt: wenn $ t \rightarrow* t_1$ und $t \rightarrow* t_2$, dann gibt es ein $t' \in D$ mit $t_1 \rightarrow* t'$ und $t_2 \rightarrow* t'$
|
Ein Transitiosnsystem $(D,\rightarrow*)$ heißt genau dann konfluent, wenn für alle $t,t_1,t_2 \in D$ gilt: wenn $ t \rightarrow* t_1$ und $t \rightarrow* t_2$, dann gibt es ein $t' \in D$ mit $t_1 \rightarrow* t'$ und $t_2 \rightarrow* t'$
|
||||||
\end{minipage}}
|
\end{minipage}}
|
||||||
\item Wenn der Lambda-Kalkül konfluent ist, kann hieraus gefolgert werden, dass unterschiedliche Reduktionsreihenfolgen, die zu einer nicht mehr weiter zu reduzierenden Form führen, somit auf den gleichen Term führen müssen.
|
\item Wenn der Lambda-Kalkül konfluent ist, kann hieraus gefolgert werden, dass unterschiedliche Reduktionsreihenfolgen, die zu einer nicht mehr weiter zu reduzierenden Form führen, somit auf den gleichen Term führen müssen.
|
||||||
@ -2803,7 +2806,7 @@ Bei terminierenden $\beta$-Reduktionen ist irrelevant, welchen Redex man zuerst
|
|||||||
\end{itemize*}
|
\end{itemize*}
|
||||||
\item Hierbei ist es insbesondere von Interesse, wie Parameter gehandhabt werden, deren Werte undefiniert sind (z.B. 1/0)\newline
|
\item Hierbei ist es insbesondere von Interesse, wie Parameter gehandhabt werden, deren Werte undefiniert sind (z.B. 1/0)\newline
|
||||||
\colorbox{lightgray}{
|
\colorbox{lightgray}{
|
||||||
\begin{minipage}[h]{1.0\linewidth}
|
\begin{minipage}[h]{.9\linewidth}
|
||||||
Wir definieren zunächst den zentralen begriff 'strikt': \newline Eine n-stellige Funktion heißt strikt im k-ten Argument $(1<=k<=n)$, wenn gilt: $f(x_1,x_2,...,x_{k-1},\bot,x_{k+1},...,x_n)=\bot$
|
Wir definieren zunächst den zentralen begriff 'strikt': \newline Eine n-stellige Funktion heißt strikt im k-ten Argument $(1<=k<=n)$, wenn gilt: $f(x_1,x_2,...,x_{k-1},\bot,x_{k+1},...,x_n)=\bot$
|
||||||
\end{minipage}}
|
\end{minipage}}
|
||||||
\item Ein undefiniertes Argument führt hier zu einem undefinierten Resultat
|
\item Ein undefiniertes Argument führt hier zu einem undefinierten Resultat
|
||||||
|
Loading…
Reference in New Issue
Block a user