diff --git a/merkzettel.pdf b/merkzettel.pdf index 4a415f2..3a9d78d 100644 Binary files a/merkzettel.pdf and b/merkzettel.pdf differ diff --git a/merkzettel.tex b/merkzettel.tex index a976ccf..d0442c1 100644 --- a/merkzettel.tex +++ b/merkzettel.tex @@ -72,6 +72,7 @@ Wir definieren $A \subseteq \mathbb{N}$ und für jede $n$-stellige Operation $f$ \begin{equation*} \lambda x.yx \ered y \end{equation*} + \item \textbf{TODO} $\alpha$-Äquivalenz \end{itemize} \subsubsection*{Auswertungsstrategien} \begin{itemize} @@ -363,4 +364,69 @@ f_1 \times f_2 &= \langle f_1 \circ\pi_1, f_2\circ\pi_2\rangle\\ S\lbrack E/x\rbrack \cup \lbrace x \pteq E\rbrace (\text{für }x\notin FV(E), x\in FV(S)) \end{cases*} && \text{ (occurs)/(elim)} \end{align*} +\section*{Notation} +\begin{itemize} + \item Applikation ist links-assoziativ: $((x(yz))u)v = x(yz)uv$ + \item Abstraktion reicht so weit wie möglich: $\lambda x.(x(\lambda y.(yx))) = \lambda x.x(\lambda y.yx)$ + \item Aufeinanderfolgende Abstraktionen werden zusammengefasst: $\lambda x.\lambda y.\lambda z.yx = \lambda xyz.yz$ +\end{itemize} +\section*{Definitionen aus der Übung} +\begin{align*} +flip\ &= \lambda f\ x\ y.f\ y\ x\\ +const\ &= \lambda x\ y.x\\ +twice\ &= \lambda f\ x.f\ (f\ x) +\end{align*} +\subsection*{Church-Kodierung} +\begin{align*} +true\ &= \lambda x\ y.x\\ +false\ &= \lambda x\ y.y\\ +if\_then\_else\ &= \lambda b\ x\ y.b\ x\ y +\end{align*} +\begin{align*} +pair\ a\ b\ &= \lambda select.select\ a\ b\\ +fst\ p\ &= p\ (\lambda x\ y.x)\\ +snd\ p\ &= p\ (\lambda x\ y.y)\\ +swap\ p\ &= p\ (\lambda x\ y\ select.select\ y\ x) +\end{align*} +\begin{align*} +zero\ &= \lambda f\ a.a\\ +succ\ n\ &= \lambda f\ a. f\ (n\ f\ a)\\ +add\ n\ m\ &= \lambda f\ a. n\ f\ (m\ f\ a) = n\ succ\ m\\ +mult\ n\ m\ &= \lambda f\ a.n\ (m\ f)\ a = n\ (add\ m)\ 0\\ +isZero\ n &= n\ (\lambda x.false)\ true\\ +odd\ n\ & if\ (n == 0)\ then\ true\ else\ (not\ (odd\ n-\lceil 1\rceil )) +\end{align*} +\begin{align*} +length\ Nil\ &= 0\\ +length\ (Cons\ x\ xs)\ &= 1 + length(xs) +\end{align*} +\begin{align*} +snoc\ Nil\ x\ &= Cons\ x\ Nil\\ +snoc\ (Cons\ x\ xs)\ y\ &= Cons\ x\ (snoc\ xs\ y) +\end{align*} +\begin{align*} +reverse\ Nil\ &= Nil\\ +reverse\ (Cons\ x\ xs)\ &= snoc\ reverse(xs)\ x +\end{align*} +\begin{align*} +drop\ y\ Nil\ = Nil\\ +drop\ y\ (Cons\ x\ xs) &= \begin{cases*} +drop\ y\ xs\ \text{, falls } y=x\\ +Cons\ x\ (drop\ y\ xs)\ \text{, sonst} +\end{cases*} +\end{align*} +\begin{align*} +elem\ y\ Nil\ &= False\\ +elem\ y\ (Cons\ x\ xs) &= \begin{cases*} +True\ \text{, falls x=y}\\ +elem\ y\ xs\ \text{, sonst} +\end{cases*} +\end{align*} +\begin{align*} +minimum\ Nil\ &= 0\\ +minimum\ (Cons\ x\ xs)\ &= \begin{cases*} +x\ \text{, falls $minimum\ xs$ = 0}\\ +min\ x\ (minimum\ xs)\ \text{, sonst} +\end{cases*} +\end{align*} \end{document} \ No newline at end of file