diff --git a/merkzettel.pdf b/merkzettel.pdf index fe06245..4141eb4 100644 Binary files a/merkzettel.pdf and b/merkzettel.pdf differ diff --git a/merkzettel.tex b/merkzettel.tex index eec74e8..9ab7113 100644 --- a/merkzettel.tex +++ b/merkzettel.tex @@ -140,9 +140,33 @@ \item Subjektreduktion: Wenn $\Gamma\vdash t:\alpha$ und $t \rightarrow_\beta^* s$, dann auch $\Gamma \vdash s:\alpha$, aber nicht umgekehrt! \satz{3.38}{45} \end{itemize} \section*{Induktive Datentypen} -\subsection*{Mengenkonstruktionen} -\subsection*{Mehrsortigkeit} +\subsection*{Mengenkonstruktionen} \defin{4.12}{56}\lem{4.13}{57} +\begin{align*} +X_1 \times X_2 &= \left\lbrace \left(x_1, x_2\right)\vert x_i \in X_i\text{ für } i=1,2\right\rbrace &&\text{(\enquote{struct})}\\ +X_1 + X_2 &= \left\lbrace (i,x) \vert i=1,2, x\in X_i\right\rbrace &&\text{(\enquote{union})}\\ +1 &= \left\lbrace * \right\rbrace &&\text{\enquote{()} in Haskell} +\end{align*} +Seien $f_i :X_i \rightarrow Y_i$, $g_i: X_i \rightarrow Z$ und $h_i : Z \rightarrow X_i$ mit $i \in \{1,2\}$. +\begin{align*} +f_1 \times f_2 &: X_1 \times X_2 \rightarrow Y_1 \times Y_2, & (f_1\times f_2) (x_1, x_2) &= (f_1(x_1), f_2(x_2))\\ +f_1 + f_2 &: X_1 + X_2 \rightarrow Y_1 + Y_2, & (f_1+f_2)(i,x) &= (i, f_i(x))\\ +[g_1, g_2] &: X_1 + X_2 \rightarrow Z, & [g_1, g_2])(i,x) &= g_i(x)\\ +\langle h_1, h_2\rangle &: Z\rightarrow X_1\times X_2, & \langle h_1, h_2\rangle(z) &= (h_1(z), h_2(z))\\ +in_i &: X_i \rightarrow X_1 + X_2, & in_i(x) &= (i,x)\\ +\pi_i &: X_1\times X_2 \rightarrow X_i, & \pi_i(x_1,x_2) &= x_i\\ +1&: 1\rightarrow 1 +\end{align*} + +Es gilt +\begin{align*} +[g_1, g_2] \circ in_i &= g_i\\ +f_1 + f_2 &= [in_1 \circ f_1, in_2 \circ f_2]\\ +[r\circ in_1, r\circ in_2] &= r \text{ für } r: X_1+X_2 \rightarrow Z\\ +\pi_i \circ \langle h_1, h_2\rangle &= h_i\\ +f_1 \times f_2 &= \langle f_1 \circ\pi_1, f_2\circ\pi_2\rangle\\ +\langle\pi_i \circ f, \pi_2\circ f\rangle &= f \text{ für } f: Z\rightarrow X_1\times X_2 +\end{align*} \subsection*{Strukturelle Induktion} \begin{itemize} \item über einsortige Datentypen \siehe{S. 63} @@ -156,6 +180,9 @@ \end{itemize} \end{itemize} \subsection*{Kodatentypen} +\begin{itemize} + \item Definition über \enquote{Destruktoren} etwa $hd$ und $tl$ +\end{itemize} \subsection*{Koinduktion} \begin{itemize} \item Bisimulation $R\subseteq A^\omega \times A^\omega$, wenn für alle $(s,t) \in R$ gilt: \defin{4.39}{74}