%!TEX root = Programmierparadigmen.tex \chapter{$\lambda$-Kalkül} Der $\lambda$-Kalkül (gesprochen: Lambda-Kalkül) ist eine formale Sprache. In diesem Kalkül gibt es drei Arten von Termen $T$: \begin{itemize} \item Variablen: $x$ \item Applikationen: $(T S)$ \item Lambda-Abstraktion: $\lambda x. T$ \end{itemize} In der Lambda-Abstraktion nennt man den Teil vor dem Punkt die \textit{Parameter} der $\lambda$-Funktion. Wenn etwas dannach kommt, auf die die Funktion angewendet wird so heißt dieser Teil das \textit{Argument}: \[(\lambda \underbrace{x}_{\mathclap{\text{Parameter}}}. x^2) \overbrace{5}^{\mathclap{\text{Argument}}} = 5^2\] \begin{beispiel}[$\lambda$-Funktionen] \begin{bspenum} \item $\lambda x. x$ heißt Identität. \item $(\lambda x. x^2)(\lambda y. y + 3) = \lambda y. (y+3)^2$ \item \label{bsp:lambda-3} $\begin{aligned}[t] &(\lambda x.\Big (\lambda y.yx \Big ))~ab\\ \Rightarrow&(\lambda y.ya)b\\ \Rightarrow&ba \end{aligned}$ \end{bspenum} In \cref{bsp:lambda-3} sieht man, dass $\lambda$-Funktionen die Argumente von Links nach rechts einziehen. \end{beispiel} Die Funktionsapplikation sei linksassoziativ. Es gilt also: \[a~b~c~d = ((a~b)~c)~d\] \begin{definition}[Gebundene Variable]\xindex{Variable!gebundene}% Eine Variable heißt gebunden, wenn sie der Parameter einer $\lambda$-Funktion ist. \end{definition} \begin{definition}[Freie Variable]\xindex{Variable!freie}% Eine Variable heißt \textit{frei}, wenn sie nicht gebunden ist. \end{definition} \begin{satz} Der untypisierte $\lambda$-Kalkül ist Turing-Äquivalent. \end{satz} \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]\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. Man schreibt dann: $T_1 \overset{\alpha}{=} T_2$. \end{definition} \begin{beispiel}[$\alpha$-Äquivalenz] \begin{align*} \lambda x.x &\overset{\alpha}{=} \lambda y. y\\ \lambda x. x x &\overset{\alpha}{=} \lambda y. y y\\ \lambda x. (\lambda y. z (\lambda x. z y) y) &\overset{\alpha}{=} \lambda a. (\lambda x. z (\lambda c. z x) x) \end{align*} \end{beispiel} \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} \begin{beispiel}[$\beta$-Äquivalenz] \begin{defenum} \item $(\lambda x.\ x)\ y \overset{\beta}{\Rightarrow} x[x \mapsto y] = y$ \item $(\lambda x.\ x\ (\lambda x.\ x)) (y\ z) \overset{\beta}{\Rightarrow} (x\ (\lambda x.\ x))[x \mapsto y\ z] (y\ z) (\lambda x.\ x)$ \end{defenum} \end{beispiel} \begin{definition}[$\eta$-Äquivalenz\footnote{Folie 158}]\xindex{Reduktion!Eta ($\eta$)}\xindex{Äquivalenz!Eta ($\eta$)}% Die Terme $\lambda x. f~x$ und $f$ heißen $\eta$-Äquivalent, wenn $x \notin FV(f)$ gilt. Man schreibt: $\lambda x. f~x \overset{\eta}{=} f$. \end{definition} \begin{beispiel}[$\eta$-Äquivalenz\footnote{Folie 158}]% \begin{align*} \lambda x.\ \lambda y.\ f\ z\ x\ y &\overset{\eta}{=} \lambda x.\ f\ z\ x\\ f\ z &\overset{\eta}{=} \lambda x.\ f\ z\ x\\ \lambda x.\ x &\overset{\eta}{=} \lambda x.\ (\lambda x.\ x)\ x\\ \lambda x.\ f\ x\ x &\overset{\eta}{\neq} f\ x \end{align*} \end{beispiel} \index{Reduktion|)} \section{Auswertungsstrategien} \begin{definition}[Normalenreihenfolge]\xindex{Normalenreihenfolge}% In der Normalenreihenfolge-Auswertungsstrategie wird der linkeste äußerste Redex ausgewertet. \end{definition} \begin{definition}[Call-By-Name]\xindex{Call-By-Name}% In der Call-By-Name Auswertungsreihenfolge wird der linkeste äußerste Redex reduziert, der nicht von einem $\lambda$ umgeben ist. \end{definition} Die Call-By-Name Auswertung wird in Funktionen verwendet. Haskell verwendet die Call-By-Name Auswertungsreihenfolge zusammen mit \enquote{sharing}. Dies nennt man \textit{Lazy Evaluation}. Ein spezialfall der Lazy-Evaluation ist die sog. \textit{Kurzschlussauswertung}.\xindex{Kurzschlussauswertung}\xindex{Short-circuit evaluation} Das bezeichnet die Lazy-Evaluation von booleschen Ausdrücken. \todo[inline]{Was ist sharing?} \begin{definition}[Call-By-Value]\xindex{Call-By-Value}% In der Call-By-Value Auswertung wird der linkeste Redex reduziert, der nicht von einem $\lambda$ umgeben ist und dessen Argument ein Wert ist. \end{definition} Die Call-By-Value Auswertungsreihenfolge wird in C und Java verwendet. Auch in Haskell werden arithmetische Ausdrücke in der Call-By-Name Auswertungsreihenfolge reduziert. \section{Church-Zahlen} Im $\lambda$-Kalkül lässt sich jeder mathematische Ausdruck darstellen, also insbesondere beispielsweise auch $\lambda x. x+3$. Aber \enquote{$3$} und \enquote{$+$} ist hier noch nicht das $\lambda$-Kalkül. Zuerst müssen wir uns also Gedanken machen, wie man natürliche Zahlen $n \in \mdn$ darstellt. Dafür dürfen wir nur Variablen und $\lambda$ verwenden. Eine Möglichkeit das zu machen sind die sog. \textit{Church-Zahlen}. Dabei ist die Idee, dass die Zahl angibt wie häufig eine Funktion $f$ auf eine Variable $z$ angewendet wird. Also: \begin{itemize} \item $0 := \lambda f~z. z$ \item $1 := \lambda f~z. f z$ \item $2 := \lambda f~z. f (f z)$ \item $3 := \lambda f~z. f (f (f z))$ \end{itemize} Auch die gewohnten Operationen lassen sich so darstellen. \begin{beispiel}[Nachfolger-Operation] \begin{align*} \succ :&= \lambda n f z. f (n f z)\\ &= \lambda n. (\lambda f (\lambda z f (n f z))) \end{align*} Dabei ist $n$ die Zahl. Will man diese Funktion anwenden, sieht das wie folgt aus: \begin{align*} \succ 1&= (\lambda n f z. f(n f z)) 1\\ &= (\lambda n f z. f(n f z)) \underbrace{(\lambda f~z. f z)}_{n}\\ &= \lambda f z. f (\lambda f~z. f z) f z\\ &= \lambda f z. f (f z)\\ &= 2 \end{align*} \end{beispiel} \begin{beispiel}[Vorgänger-Operation] \begin{align*} \pair&:= \lambda a. \lambda b. \lambda f. f a b\\ \fst &:= \lambda p. p (\lambda a. \lambda b. a)\\ \snd &:= \lambda p. p (\lambda a. \lambda b. b)\\ \nxt &:= \lambda p. \pair (\snd p)~(\succ (\snd p))\\ \pred&:= \lambda n. \fst (n \nxt (\pair c_0 c_0)) \end{align*} \end{beispiel} \begin{beispiel}[Addition] \begin{align*} \text{plus} &:= \lambda m n f z. m f (n f z) \end{align*} Dabei ist $m$ der erste Summand und $n$ der zweite Summand. \end{beispiel} \begin{beispiel}[Multiplikation] \begin{align*} \text{times} :&= \lambda m n f. m~s~(n~f~z)\\ &\overset{\eta}{=} \lambda m n f z. n (m s) z \end{align*} Dabei ist $m$ der erste Faktor und $n$ der zweite Faktor. \end{beispiel} \begin{beispiel}[Potenz] \begin{align*} \text{exp} :&= \lambda b e. eb\\ &\overset{\eta}{=} \lambda b e f z. e b f z \end{align*} Dabei ist $b$ die Basis und $e$ der Exponent. \end{beispiel} \section{Church-Booleans} \begin{definition}[Church-Booleans]\xindex{Church-Booleans}% \texttt{True} wird zu $c_{\text{true}} := \lambda t. \lambda f. t$.\\ \texttt{False} wird zu $c_{\text{false}} := \lambda t. \lambda f. f$. \end{definition} Hiermit lässt sich beispielsweise die Funktion \texttt{is\_zero} definieren, die \texttt{True} zurückgibt, wenn eine Zahl $0$ repräsentiert und sonst \texttt{False} zurückgibt: \[ \text{\texttt{is\_zero}} = \lambda n.\ n\ (\lambda x.\ c_{\text{False}})\ c_{\text{True}}\] \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} \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} \section{Let-Polymorphismus}\xindex{let-Polymorphismus}\footnote{WS 2013 / 2014, Folie 205ff}% Das Programm $P = \text{let } f = \lambda x.\ 2 \text{ in } f\ (f\ \text{\texttt{true}})$ ist eine polymorphe Hilfsfunktion, da sie beliebige Werte auf 2 Abbildet. Auch solche Ausdrücke sollen typisierbar sein. Die Kodierung \[\text{let} x = t_1 \text{ in } t_2\] ist bedeutungsgleich mit \[(\lambda x.\ t_2) t_1\] Das Problem ist, dass \[P = \lambda f. \ f (f\ \text{\texttt{true}})\ (\lambda x.\ 2)\] so nicht typisierbar ist, da in \[\ABS \frac{f: \tau_f \vdash f\ (f\ \text{\texttt{true}}): \dots}{\vdash \lambda f.\ f\ (f\ \text{\texttt{true}}): \dots}\] müsste \[\tau_f = \text{bool} \rightarrow \text{int}\] und zugleich \[\tau_f = \text{int} \rightarrow \text{int}\] in den Typkontext eingetragen werden. Dies ist jedoch nicht möglich. Stattdessen wird \[\text{let} x = t_1 \text{ in } t_2\] als neues Konstrukt im $\lambda$-Kalkül erlaubt. \begin{definition}[Typschema]\xindex{Typschema}% Ein Typ der Gestalt $\forall \alpha_1.\ \forall \alpha_2.\ \dots\ \forall \alpha_n. \tau$ heißt \textbf{Typschema}. Es bindet freie Variablen $\alpha_1, \dots, \alpha_n$ in $\tau$. \end{definition} \begin{beispiel}[Typschema] Das Typschema $\forall \alpha.\ \alpha \rightarrow \alpha$ steht für unendlich viele Typen und insbesondere für folgende: \begin{bspenum} \item int $\rightarrow$ int, bool $\rightarrow$ bool, \dots \item (int $\rightarrow$ int) $\rightarrow$ (int $\rightarrow$ int), \dots \item \dots \end{bspenum} \end{beispiel} \begin{definition}[Typschemainstanziierung]\xindex{Typschemainstanziierung}% Sei $\tau_2$ ein Nicht-Schema-Typ. Dann heißt der Typ \[\tau[\alpha \mapsto \tau_2]\] eine \textbf{Instanziierung} vom Typschema $\forall \alpha.\ \tau$ und man schreibt: \[(\forall \alpha.\ \tau) \succeq \tau [\alpha \mapsto \tau_2]\] \end{definition} \begin{beispiel}[Typschemainstanziierung] Folgendes sind Beispiele für Typschemainstanziierungen: \begin{bspenum} \item $\forall \alpha.\ \alpha \rightarrow \alpha \succeq \text{int} \rightarrow \text{int}$ \item $\forall \alpha.\ \alpha \rightarrow \alpha \succeq (\text{int} \rightarrow \text{int}) \rightarrow (\text{int} \rightarrow \text{int})$ \item $\text{int} \succeq \text{int}$ \end{bspenum} Folgendes sind keine Typschemainstanziierungen: \begin{bspenum} \item $\alpha \rightarrow \alpha \nsucceq \text{int} \rightarrow \text{int}$ \item $\alpha \nsucceq \text{bool}$ \item $\forall \alpha.\ \alpha \rightarrow \alpha \nsucceq \text{bool}$ \end{bspenum} \end{beispiel} Zu Typschemata gibt es angepasste Regeln: \[\VAR \frac{\Gamma(x)= \tau' \;\;\; \tau' \succeq \tau}{\gamma \vdash x: \tau}\] und \[\ABS \frac{\Gamma, x: \tau_1 \vdash t: \tau_2 \;\;\; \tau_1 \text{ kein Typschema}}{\Gamma \vdash \lambda x. t: \tau_1 \rightarrow \tau_2}\] \todo[inline]{Folie 208ff} \section{Literatur} \begin{itemize} \item \url{http://c2.com/cgi/wiki?FreeVariable} \item \url{http://www.lambda-bound.com/book/lambdacalc/node9.html} \end{itemize}