diff --git a/12/tut12.md b/12/tut12.md new file mode 100644 index 0000000000000000000000000000000000000000..9c3047b4c3eec07481033629da4fbfb1ab7c9fd1 --- /dev/null +++ b/12/tut12.md @@ -0,0 +1,77 @@ +--- +theme: metropolis +aspectratio: 169 +header-includes: | + \usepackage{qrcode} + \include{hyperref} + \include{amsmath} +--- + +# Überleitung + +```Haskell +add3 a b c = a + b + c +``` +\ +**Auswertung**: +```Haskell +add3 1 2 3 +(\a -> \b -> \c -> a + b + c) 1 2 3 +(\b -> \c -> 1 + b + c) 2 3 +(\c -> 1 + 2 + c) 3 +1 + 2 + 3 +``` + +# Lambda-Kalkül + +weniger Formal korrekte, aber vielleicht leichter verständliche Zusammenfassung + +# Variablen + +* Variablennamen bestehen nur aus einem Buchstaben + +**Beispiel**: + +* $(\lambda xyz.xyz)$ hat drei Argumente + +# Bindung + +\begin{center} +\huge{($\lambda$ $V.E$)} +\end{center} + +* Eine Variable ist gebunden, wenn sie in V und in E vorkommt +* E kann wieder ein weiterer Lambda-Ausdruck sein, dann sind Variablen mit dem gleichen Namen auch darin gebunden +* In einem Ausdruck mit mehreren Teilausdrücken ist eine Variable gebunden, wenn sie in einem Teilausdruck gebunden ist. + +**Beispiele**: + +* $(\lambda x.x)$ - x ist gebunden +* $(\lambda x.y)$ - y ist nicht gebunden +* $(\lambda x.(\lambda y.x))$ - x ist gebunden + + +# $\beta$-Reduktion (Funktionsanwendung) + +\begin{center} +\huge{($\lambda$ $x.E$) y} +\end{center} + +* Der Ausdruck in Klammern hat ein Argument, $x$ +* Bei der Auswertung mit einem übergebenen Argument ($y$), wird der Wert von $y$ für $x$ eingesetzt + +**Beispiel**: + +* $(\lambda x.x)y \equiv_{\beta} y$ + +# $\alpha$-Konversion (Umbenennung) + +\begin{center} +\huge{($\lambda$ $V.E$) x} +\end{center} + +Wenn $x$ in $E$ gebunden wäre, muss $x$ in V und E umbenannt werden, bevor $x$ eingesetzt werden kann. + +**Beispiel**: + +* $(\lambda xy.x) y \equiv_{\alpha} (\lambda xt.x) y$ diff --git a/12/tut12.pdf b/12/tut12.pdf new file mode 100644 index 0000000000000000000000000000000000000000..9c68c0164aa66026256948f32caa555c5088d924 Binary files /dev/null and b/12/tut12.pdf differ