Falsche Aufgabenstellungen in den falschen Aufgabenbereichen.

Fehlende Aufgabenstellungen hinzugefügt.
Fehlende Definitionen hinzugefügt.
Falsche Definitionen korrigiert.

Braindump.tex

@@ -62,24 +62,56 @@ Wir erinnern an einige im $\lambda$-Kalkül definierte Funktionen:
 \end{enumerate}
 
 \section*{Aufgabe 3}
-
+Wir betrachten den Datentyp der Listen~$List\;a$:
+\begin{align*}
+  &\text{data} \; List\;a \; \text{where} \\
+  &\hspace{10pt}nil :\; ()\; \rightarrow\; List\;a \\
+  &\hspace{10pt}cons :\; a\; \rightarrow\; List\;a\rightarrow\; List\;a.
+\end{align*}
 % XXX: Defintionen von Funktionen über Listen
+Zusätzlich seien die folgenden Funktionen auf Listen definiert:
+\begin{align*}
+	&concat:\; List\;a\rightarrow\;List\;a\rightarrow\;List\;a\; \text{where}\\
+	&\hspace{10pt}concat \;nil\; ys = ys\\
+	&\hspace{10pt}concat\; (cons\; x\; xs) \;ys = cons\;x\; (concat\; xs\; ys)\\[15pt]
+	&flatten:\; List\;(List\;a)\rightarrow\;List\;a\; \text{where}\\
+	&\hspace{10pt}flatten\; nil = nil\\
+	&\hspace{10pt}flatten\; (cons\; xs\; xss) = concat\; xs\; (flatten\; xss)\\[15pt]
+	&map:\; (a \rightarrow b) \rightarrow List\;a\rightarrow\;List\;b\; \text{where}\\
+	&\hspace{10pt}map\; f \;nil\; = nil\\
+	&\hspace{10pt}map\; f \; (cons\; x\; xs) \; = cons\; (f\;x) (map\; f \; xs)
+\end{align*}
 
-Zeigen Sie mittels struktureller Induktion, dass
+\begin{enumerate}
+  \item Zeigen Sie mittels struktureller Induktion, dass
 		\begin{align*}
 			flatten (map \; (map \; f) \; xss) = map \; f \; (flatten \; xss) % XXX: Richtige Frage?
 		\end{align*}
 		für alle $f$, $xss$ gilt.
+	\item Eine Liste natürlicher Zahlen $s:\;List\; Int\;$ ist \emph{steep}, wenn der jeweils nächste
+    $Int$ größer ist als der vorherige, d.h. die Liste der natürlichen Zahlen ist aufsteigend sortiert.\\
+    %\begin{align*}
+      %(head \; s) < head (tail \; s).
+    %\end{align*} % XXX: Defintion okay?
+    Schreiben Sie eine Funktion $steep' s$, die $True$ zurückgibt,
+    wenn $s$ \emph{steep} ist. Hierfür ist folgendes Gerüst zu verwenden:
+    \begin{align*}
+      steep' &= snd. \; fold \; c \; g \; \text{where} \\
+        c &= &:: (Nat, Bool) \\
+        g &= &:: Nat \rightarrow (Nat, \; Bool) \rightarrow (Nat, \; Bool) \\
+    \end{align*}
+\end{enumerate}
+
+\newpage
 
 \section*{Aufgabe 4}
 
 Wir betrachten den Kodatentyp~$IntStream$:
 \begin{align*}
-  \text{codata} \; IntStream \; \text{where} \\
-  head (Cons \; x \; xs) &= x \\
-  tail (Cons \; x \; xs) &= xs
+  &\text{codata} \; IntStream \; \text{where} \\
+  &\hspace{10pt}head :\; IntStream\; \rightarrow\; Int \\
+  &\hspace{10pt}tail :\; IntStream \; \rightarrow \; IntStream.
 \end{align*}
-mit $x \in Int$ und $x \in IntStream$.
 
 Gegeben sind weiterhin folgende auf $IntStream$ definierte Funktionen:
 \begin{align*}
@@ -87,25 +119,24 @@ Gegeben sind weiterhin folgende auf $IntStream$ definierte Funktionen:
   tail (alt \; a \; b) &= alt \; b \; a \\
   head (const \; i) &= i \\
   tail (const \; i) &= const \; i \\
-  head (s \boxplus t) &= (head \; s) \boxplus (head \; t) \\
+  head (s \boxplus t) &= (head \; s) + (head \; t) \\
   tail (s \boxplus t) &= (tail \; s) \boxplus (tail \; t) \\
-  head (psum \; s) &= s \\ % XXX: Schwer lesbar in den Aufzeichnungen
+  head (psum \; s) &= head s \\ % XXX: Schwer lesbar in den Aufzeichnungen
   tail (psum \; s) &= (const (head \; s)) \boxplus (psum (tail \; s))
 \end{align*}
 \begin{enumerate}
-  \item Ein $IntStream \; s$ ist \emph{steep}, wenn der jeweils nächste
-    $Int$ größer ist als der vorherige, d.h.
+  \item Definieren Sie den Begriff $Bisimulation$ über dem Typ $IntStream$.
+  \item Zeigen Sie mittels Koinduktion:
 	\begin{align*}
-      (head \; s) < head (tail \; s).
-    \end{align*} % XXX: Defintion okay?
-    Schreiben Sie eine Funktion $steep' s$, die $True$ zurückgibt,
-    wenn $s$ \emph{steep} ist. Hierfür ist folgendes Gerüst zu verwenden:
+			psum\; (alt\; 1\; (-1)) &= alt\; 1\; 0
+	\end{align*}
+	\textit{Hinweis: Sie dürfen ohne Beweis verwenden, dass gilt
 	\begin{align*}
-      steep' &= snd. \; fold \; c \; g \; \text{where} \\
-        c &= &:: (Nat, Bool) \\
-        g &= &:: (Nat \rightarrow (Nat, \; Bool) \rightarrow (Nat, \; Bool) \\
+		(const\; a) \boxplus (const\; b) &= const (a+b)\\
+		r \boxplus (s \boxplus t) &= (r \boxplus s) \boxplus t\\
+		(r \boxplus s) \boxplus t &= r \boxplus (s \boxplus t)\\
 	\end{align*} 
-  \item Irgendetwas mit Koinduktion zeigen % XXX: TODO
+	}
 \end{enumerate}
 
 \section*{Aufgabe 5}
@@ -122,3 +153,4 @@ an und erläutern Sie, warum dieser $L$ definiert. Andernfalls zeigen
 Sie mittels des Pumping-Lemma, dass $L$ nicht regulär ist.
 
 \end{document}
+

meta.tex

@@ -11,7 +11,10 @@
 % Math and special characters
 \usepackage{amsfonts}
 \usepackage{amssymb}
-\usepackage{mathtools}
+\usepackage{amsthm}
+\usepackage{amsmath}
+\usepackage{listings}
+%\usepackage{mathtools}
 
 % Links
 \usepackage{hyperref}