|
@@ -46,12 +46,12 @@ Die Funktionsapplikation sei linksassoziativ. Es gilt also:
|
|
|
Der untypisierte $\lambda$-Kalkül ist Turing-Äquivalent.
|
|
|
\end{satz}
|
|
|
|
|
|
-\section{Reduktionen}\index{Reduktionen|(}
|
|
|
+\section{Reduktionen}\index{Reduktion|(}
|
|
|
\begin{definition}[Redex]\xindex{Redex}%
|
|
|
Eine $\lambda$-Term der Form $(\lambda x. t_1) t_2$ heißt Redex.
|
|
|
\end{definition}
|
|
|
|
|
|
-\begin{definition}[$\alpha$-Äquivalenz]
|
|
|
+\begin{definition}[$\alpha$-Äquivalenz]\xindex{Reduktion!Alpha ($\alpha$)}\xindex{Äquivalenz!Alpha ($\alpha$)}%
|
|
|
Zwei Terme $T_1, T_2$ heißen $\alpha$-Äquivalent, wenn $T_1$ durch
|
|
|
konsistente Umbenennung in $T_2$ überführt werden kann.
|
|
|
|
|
@@ -67,7 +67,7 @@ Die Funktionsapplikation sei linksassoziativ. Es gilt also:
|
|
|
\end{align*}
|
|
|
\end{beispiel}
|
|
|
|
|
|
-\begin{definition}[$\beta$-Äquivalenz]
|
|
|
+\begin{definition}[$\beta$-Äquivalenz]\xindex{Reduktion!Beta ($\beta$)}\xindex{Äquivalenz!Beta ($\beta$)}%
|
|
|
Eine $\beta$-Reduktion ist die Funktionsanwendung auf einen Redex:
|
|
|
\[(\lambda x. t_1) t_2 \Rightarrow t_1 [x \mapsto t_2]\]
|
|
|
\end{definition}
|
|
@@ -79,7 +79,7 @@ Die Funktionsapplikation sei linksassoziativ. Es gilt also:
|
|
|
\end{defenum}
|
|
|
\end{beispiel}
|
|
|
|
|
|
-\begin{definition}[$\eta$-Äquivalenz]
|
|
|
+\begin{definition}[$\eta$-Äquivalenz]\xindex{Reduktion!Eta ($\eta$)}\xindex{Äquivalenz!Eta ($\eta$)}%
|
|
|
Zwei Terme $\lambda x. f~x$ und $f$ heißen $\eta$-Äquivalent, wenn
|
|
|
$x$ nicht freie Variable von $f$ ist.
|
|
|
\end{definition}
|
|
@@ -87,7 +87,7 @@ Die Funktionsapplikation sei linksassoziativ. Es gilt also:
|
|
|
\begin{beispiel}[$\eta$-Äquivalenz]
|
|
|
TODO
|
|
|
\end{beispiel}
|
|
|
-\index{Reduktionen|)}
|
|
|
+\index{Reduktion|)}
|
|
|
|
|
|
\section{Auswertungsstrategien}
|
|
|
\begin{definition}[Normalenreihenfolge]\xindex{Normalenreihenfolge}%
|
|
@@ -193,4 +193,101 @@ Auch die gewohnten Operationen lassen sich so darstellen.
|
|
|
\section{Weiteres}
|
|
|
\begin{satz}[Satz von Curch-Rosser]
|
|
|
Wenn zwei unterschiedliche Terme $a$ und $b$ äquivalent sind, d.h. mit Reduktionsschritten beliebiger Richtung ineinander transformiert werden können, dann gibt es einen weiteren Term $c$, zu dem sowohl $a$ als auch $b$ reduziert werden können.
|
|
|
-\end{satz}
|
|
|
+\end{satz}
|
|
|
+
|
|
|
+\section{Fixpunktkombinator}
|
|
|
+\begin{definition}[Fixpunkt]\xindex{Fixpunkt}%
|
|
|
+ Sei $f: X \rightarrow Y$ eine Funktion mit $\emptyset \neq A = X \cap Y$ und
|
|
|
+ $a \in A$.
|
|
|
+
|
|
|
+ $a$ heißt \textbf{Fixpunkt} der Funktion $f$, wenn $f(a) = a$ gilt.
|
|
|
+\end{definition}
|
|
|
+
|
|
|
+\begin{beispiel}[Fixpunkt]
|
|
|
+ \begin{bspenum}
|
|
|
+ \item $f_1: \mdr \rightarrow \mdr; f(x) = x^2 \Rightarrow x_1 = 0$ ist
|
|
|
+ Fixpunkt von $f$, da $f(0) = 0$. $x_2 = 1$ ist der einzige weitere
|
|
|
+ Fixpunkt dieser Funktion.
|
|
|
+ \item $f_2: \mdn \rightarrow \mdn$ hat ganz $\mdn$ als Fixpunkte, also
|
|
|
+ insbesondere unendlich viele Fixpunkte.
|
|
|
+ \item $f_3: \mdr \rightarrow \mdr; f(x) = x+1$ hat keinen einzigen Fixpunkt.
|
|
|
+ \item $f_4: \mdr[X] \rightarrow \mdr[X]; f(p) = p^2$ hat $p_1(x) = 0$ und
|
|
|
+ $p_2(x)=1$ als Fixpunkte.
|
|
|
+ \end{bspenum}
|
|
|
+\end{beispiel}
|
|
|
+
|
|
|
+\begin{definition}[Kombinator]\xindex{Kombinator}%
|
|
|
+ Ein Kombinator ist eine Abbildung ohne freie Variablen.
|
|
|
+\end{definition}
|
|
|
+
|
|
|
+\begin{beispiel}[Kombinatoren\footnotemark]%
|
|
|
+ \begin{bspenum}
|
|
|
+ \item $\lambda a.\ a$
|
|
|
+ \item $\lambda a.\ \lambda b.\ a$
|
|
|
+ \item $\lambda f.\ \lambda a.\ \lambda b. f\ b\ a$
|
|
|
+ \end{bspenum}
|
|
|
+\end{beispiel}
|
|
|
+\footnotetext{Quelle: \url{http://www.haskell.org/haskellwiki/Combinator}}
|
|
|
+
|
|
|
+\begin{definition}[Fixpunkt-Kombinator]\xindex{Fixpunkt-Kombinator}%
|
|
|
+ Sei $f$ ein Kombinator, der $f\ g = g\ (f\ g)$ erfüllt. Dann heißt $f$
|
|
|
+ \textbf{Fixpunktkombinator}.
|
|
|
+\end{definition}
|
|
|
+
|
|
|
+Insbesondere ist also $f \ g$ ein Fixpunkt von $g$.
|
|
|
+
|
|
|
+\begin{definition}[Y-Kombinator]\xindex{Y-Kombinator}%
|
|
|
+ Der Fixpunktkombinator
|
|
|
+ \[Y := \lambda f.\ (\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x))\]
|
|
|
+ heißt $Y$-Kombinator.
|
|
|
+\end{definition}
|
|
|
+
|
|
|
+\begin{behauptung}
|
|
|
+ Der $Y$-Kombinator ist ein Fixpunktkombinator.
|
|
|
+\end{behauptung}
|
|
|
+
|
|
|
+\begin{beweis}\footnote{Quelle: Vorlesung WS 2013/2014, Folie 175}\leavevmode
|
|
|
+
|
|
|
+ \textbf{Teil 1:} Offensichtlich ist $Y$ ein Kombinator.
|
|
|
+
|
|
|
+ \textbf{Teil 2:} z.~Z.: $Y f \Rightarrow^* f \ (Y \ f)$
|
|
|
+
|
|
|
+ \begin{align*}
|
|
|
+ Y\ f &=\hphantom{^\beta f\ } (\lambda f.\ (\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x)))\ f\\
|
|
|
+ &\Rightarrow^\beta\hphantom{f \ (\lambda f.\ } (\lambda x. f\ (x\ x))\ (\lambda x.\ f\ (x\ x))\\
|
|
|
+ &\Rightarrow^\beta f \ (\hphantom{\lambda f.\ }(\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x)))\\
|
|
|
+ &\Rightarrow^\beta f \ (\lambda f.\ (\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x))\ f)\\
|
|
|
+ &=\hphantom{^\beta} f \ (Y \ f)
|
|
|
+ \end{align*}
|
|
|
+ $\qed$
|
|
|
+\end{beweis}
|
|
|
+
|
|
|
+\begin{definition}[Turingkombinator]\xindex{Turingkombinator}%
|
|
|
+ Der Fixpunktkombinator
|
|
|
+ \[\Theta := (\lambda x. \lambda y. y\ (x\ x\ y)) (\lambda x.\ \lambda y.\ y\ (x\ x\ y))\]
|
|
|
+ heißt \textbf{Turingkombinator}.
|
|
|
+\end{definition}
|
|
|
+
|
|
|
+\begin{behauptung}
|
|
|
+ Der Turing-Kombinator $\Theta$ ist ein Fixpunktkombinator.
|
|
|
+\end{behauptung}
|
|
|
+
|
|
|
+\begin{beweis}\footnote{Quelle: Übungsblatt 6, WS 2013/2014}
|
|
|
+
|
|
|
+ \textbf{Teil 1:} Offensichtlich ist $\Theta$ ein Kombinator.
|
|
|
+
|
|
|
+ \textbf{Teil 2:} z.~Z.: $\Theta f \Rightarrow^* f \ (\Theta \ f)$
|
|
|
+
|
|
|
+ Sei $\Theta_0 := (\lambda x.\ \lambda y.\ y\ (x\ x\ y))$. Dann gilt:
|
|
|
+ \begin{align*}
|
|
|
+ \Theta\ f &= ((\lambda x.\ \lambda y.\ y\ (x\ x\ y))\ \Theta_0)\ f\\
|
|
|
+ &\Rightarrow^\beta (\lambda y. y\ (\Theta_0 \ \Theta_0 \ y))\ f\\
|
|
|
+ &\Rightarrow^\beta f \ (\Theta_0 \Theta_0 f)\\
|
|
|
+ &= f \ (\Theta \ f)
|
|
|
+ \end{align*}
|
|
|
+ $\qed$
|
|
|
+\end{beweis}
|
|
|
+
|
|
|
+
|
|
|
+
|
|
|
+Für den Turing-Operator gilt
|