uebung 08 final

.gitignore

@@ -284,6 +284,4 @@ TSWLatexianTemp*
 
 main.pdf
 main-poster.pdf
-*.pdf
-slides
 .DS_Store

texfiles/slides08.tex

@@ -227,7 +227,7 @@ Die neue Grammatik für Typen lautet:
 
 Natürlich müssen wir damit auch neue Konstrukte einführen, die zu diesen Typkonstruktoren gehören. Die Termsprache wird also erweitert auf die Grammatik
 \[
-t,s ::= x \;\vert\; ts \;\vert\; \lambda x.t \;\vert\; {t, s} \;\vert\; fst\;t \;\vert\; snd\;t    
+t,s ::= x \;\vert\; ts \;\vert\; \lambda x.t \;\vert\; \{t, s\} \;\vert\; fst\;t \;\vert\; snd\;t    
 \]
 \;\\
 Geben Sie die zusätzlich benötigten Typisierungsregeln an und erweitern Sie ebenso die Auswertungsrelation um Grundreduktion für Paare.
@@ -243,7 +243,7 @@ Geben Sie die zusätzlich benötigten Typisierungsregeln an und erweitern Sie eb
 Wir behaupten nun, dass diese Erweiterung uns auch mehr Ausdrucksstärke in der Logik auf der anderen Seite des Curry-Howard-Isomorphismus einbringt.
 Genauer gesagt, dass wir das folgende Fragment der intuitionistischen propositionalen Logik erhalten:
 \[
-\phi, \psi ::= a \;\vert\; \phi \rightarrow \psi \;\vert\; \phi \rightarrow \psi
+\phi, \psi ::= a \;\vert\; \phi \rightarrow \psi \;\vert\; \phi \land \psi
 \]
 wobei $a$ propositionale Variablen sind. Als Deduktionssystem verwenden wir den Sequentenkalkül minimaler Logik mit folgenden zusätzlichen Regeln:
 \[
@@ -254,15 +254,84 @@ wobei $a$ propositionale Variablen sind. Als Deduktionssystem verwenden wir den
 Sei $\overline{\phi}$ der Typ, der entsteht, wenn man in $\phi$ alle $\land$ durch $\times$ ersetzt. Beweisen Sie:
 Der Sequent $\vdash \phi$ ist genau dann herleitbar, wenn der Typ $\overline{\phi}$ inhabited ist.
 \end{frame}
-\begin{frame}[t, fragile]{Aufgabe 1.2}{Der Curry-Howard-Isomorphismus}
+
+\begin{frame}[t, fragile]{Aufgabe 1.2}{Überblick Sequenten- und $\lambda$-Kalkül}
+\begin{minipage}{.44\textwidth}
+\centering\textbf{Sequentenkalkül}
+\\mit $\Gamma$ als Formelmenge $\{\phi_1, \ldots, \phi_n\}$
+\[
+\begin{array}{c c}
+    \multicolumn{2}{c}{\infer* [left=(AX), right=$\phi \in \Gamma$]{\;} {\Gamma \vdash \phi}}
+    \\\;\\
+    \infer* [left=($\rightarrow_I$)] {\Gamma, \phi \vdash \psi} {\Gamma \vdash \phi \rightarrow \psi} & \infer* [left=($\land_I$)] {\Gamma \vdash \phi \\ \Gamma \vdash \psi} {\Gamma \vdash \phi \land \psi}
+    \\\;\\
+    \multicolumn{2}{c}{\infer* [left=($\rightarrow_E$)] {\Gamma \vdash \phi \rightarrow \psi \\ \Gamma \vdash \phi} {\Gamma \vdash \psi}}
+    \\\;\\
+    \infer* [left=($\land_{E1}$)] {\Gamma \vdash \phi \land \psi} {\Gamma \vdash \phi} & \infer* [left=($\land_{E2}$)] {\Gamma \vdash \phi \land \psi} {\Gamma \vdash \psi}
+\end{array}    
+\]
+\end{minipage}
+\begin{minipage}{.54\textwidth}
+    \centering\textbf{Einfach getypter $\lambda$-Kalkül}
+    \\mit $\Gamma$ als Kontext $\{x_1 : \alpha_1, \ldots, x_n : \alpha_n\}$
+    \[
+    \begin{array}{c c}
+        \multicolumn{2}{c}{\infer* [left=(Ax), right=$x : \alpha \in \Gamma$]{\;} {\Gamma \vdash x : \alpha}}
+        \\\;\\
+        \infer* [left=($\rightarrow_i$)] {\Gamma[x \mapsto \alpha] \vdash t : \beta} {\Gamma \vdash \lambda x.t : \alpha \rightarrow \beta} & \infer* [left=($prod$)] {\Gamma \vdash t : \tau \\ \Gamma \vdash s : \sigma} {\Gamma \vdash \{t,s\} : \tau \times \sigma}
+        \\\;\\
+        \multicolumn{2}{c}{\infer* [left=($\rightarrow_e$)] {\Gamma \vdash t : \alpha \rightarrow \beta \\ \Gamma \vdash s : \alpha} {\Gamma \vdash ts : \beta}}
+        \\\;\\
+        \infer* [left=($proj_1$)] {\Gamma \vdash p : \tau \times \sigma} {\Gamma \vdash fst\;p : \tau} & \infer* [left=($proj_2$)] {\Gamma \vdash p : \tau \times \sigma} {\Gamma \vdash snd\;p : \sigma}
+    \end{array}    
+    \]
+    \end{minipage}
+\end{frame}
+
+
+\begin{frame}[t, fragile]{Aufgabe 1.3}{Der Curry-Howard-Isomorphismus}
 Benutzen Sie die eben hergestellte Korrespondenz, um zu zeigen, dass folgende Formel eine Tautologie ist:
 \[
 (p \land q) \rightarrow r \rightarrow ((r \land p) \land q)    
 \]
+\vfill
+\begin{block}{Erweiterte Termgrammatik}
+    \[
+        t,s ::= x \;\vert\; ts \;\vert\; \lambda x.t \;\vert\; \{t, s\} \;\vert\; fst\;t \;\vert\; snd\;t    
+    \]
+\end{block}
 \end{frame}
 
 \section{Aufgabe 2 - Listen und Bäume}
 
+\begin{frame}[t,fragile]{Aufgabe 2}{Listen und Bäume}
+Wir betrachten die folgenden algebraischen Definitionen parametrischer Datentypen von Listen und Binärbäumen über einem Typparameter $a$:
+
+\begin{minipage}{.41\textwidth}
+    \begin{lstlisting}[language=haskell]
+data List a where
+    Nil  $\ $: () $\rightarrow$ List a
+    Cons : a $\rightarrow$ List a $\rightarrow$ List a
+    \end{lstlisting}
+\end{minipage}
+\begin{minipage}{.58\textwidth}
+    \begin{lstlisting}[language=haskell, morekeywords=Tree]
+data Tree a where
+    Leaf  $\ \ $: a $\rightarrow$ Tree a
+    Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a
+    \end{lstlisting}
+\end{minipage}
+\\\;\\\;\\
+\begin{block}{Einige Annahmen}
+Wir nehmen Typ \textbf{Nat} von Konstanten $0,1,2,\ldots$ und die üblichen Grundoperationen für \textbf{Nat} als gegeben an.
+Weiter nehmen wir den Typ \textbf{Bool} mit den Konstanten $True$ und $False$ sowie den Grundoperationen dazu als gegeben an.
+Mit \texttt{()} bezeichnen wir den Typ $unit$; er enthält nur einen einzigen Wert, den wir ebenfalls mit \texttt{()} bezeichnen.
+\\\;\\
+Weiterhin schreiben wir in Beweisen der Gleichheit zweier gegebener Terme $s$ und $t$ die Aussage $s \leftrightarrow_{\beta\delta}^* t$ abgekürzt als $s = t$.
+\end{block}
+
+\end{frame}
+
 \begin{frame}[t,fragile]{Aufgabe 2.1}{Listen und Bäume}
     Wir betrachten die folgenden algebraischen Definitionen parametrischer Datentypen von Listen und Binärbäumen über einem Typparameter $a$:
     
@@ -276,11 +345,11 @@ data List a where
     \begin{minipage}{.58\textwidth}
         \begin{lstlisting}[language=haskell, morekeywords=Tree]
     data Tree a where
-    Leaf  $\ \ $: () $\rightarrow$ Tree a
+        Leaf  $\ \ $: a $\rightarrow$ Tree a
         Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a
         \end{lstlisting}
     \end{minipage}
-\;\\
+    \vfill
     Beschreiben Sie in eigenen Worten die durch die folgenden Terme gegebenen Listen und Binärbäume mit natürlichen Zahlen bzw. zeichnen Sie diese.
     \begin{multicols}{2}
         \begin{itemize}
@@ -309,7 +378,7 @@ Beschreiben Sie in eigenen Worten die durch die folgenden Terme gegebenen Listen
     \begin{minipage}{.58\textwidth}
         \begin{lstlisting}[language=haskell, morekeywords=Tree]
     data Tree a where
-        Leaf  $\ \ $: () $\rightarrow$ Tree a
+        Leaf  $\ \ $: a $\rightarrow$ Tree a
         Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a
         \end{lstlisting}
     \end{minipage}
@@ -328,6 +397,7 @@ size (Leaf x) $\ \ \ \ \ $= 1
 size (Inner x l r) = 1 + size l + size r
         \end{lstlisting}
     \end{minipage}
+    \vfill
     \begin{enumerate}
         \item[(a)] Welchen Typ hat \texttt{length}? Welchen hat \texttt{size}?
         \item[(b)] Werten Sie den Term \texttt{length (Cons 4 (Cons 89 (Cons 21 Nil)))} aus. 
@@ -347,7 +417,7 @@ size (Inner x l r) = 1 + size l + size r
     \begin{minipage}{.58\textwidth}
         \begin{lstlisting}[language=haskell, morekeywords=Tree]
     data Tree a where
-        Leaf  $\ \ $: () $\rightarrow$ Tree a
+        Leaf  $\ \ $: a $\rightarrow$ Tree a
         Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a
         \end{lstlisting}
     \end{minipage}
@@ -366,6 +436,7 @@ size (Leaf x) $\ \ \ \ \ $= 1
 size (Inner x l r) = 1 + size l + size r
         \end{lstlisting}
     \end{minipage}
+    \vfill
     Schreiben Sie eine Funktion $\mathtt{element} : \mathbf{Nat} \rightarrow \mathbf{List}\;\mathbf{Nat} \rightarrow \mathbf{Bool}$, so dass \texttt{element a xs = True} wenn \texttt{a} in \texttt{xs} vorkommt, und andernfalls \texttt{element a xs = False}.
 \end{frame}
 
@@ -374,13 +445,13 @@ size (Inner x l r) = 1 + size l + size r
     Der Typ und die Definitionen dieser Fold-Funktionen ergeben sich dabei allein aus den Typen der Konstruktoren. 
     Beispielsweise ist die Fold-Funktion für den Datentyp $\mathbf{Nat}\;a$ aus der vorangegangenen Übung wie folgt definiert:
     \begin{lstlisting}[language=haskell]
-        foldL : c $\rightarrow$ (a $\rightarrow$ c $\rightarrow$ c) $\rightarrow$ List a $\rightarrow$ C
+        foldL : c $\rightarrow$ (a $\rightarrow$ c $\rightarrow$ c) $\rightarrow$ List a $\rightarrow$ c
         foldL n f Nil = n
         foldL n f (Cons x xs) = f x (foldL n f xs)
     \end{lstlisting}
     Hierbei entspricht der Typparameter $c$ einem Ergebnistyp und die beiden Argumente $n$ und $f$ den Konstruktoren $Nil$ und $Cons$, wobei die Typen der Argumente jeweils Operationen
     auf dem Ergebnistyp $c$ beschreiben, mit dem eine Liste $\mathbf{List}\;a$ in einen einzelnen Wert vom Typ $c$ „zusammengefaltet“ werden kann.
-    \\\;\\
+    \vfill
     Werten Sie den Term \texttt{foldL n f (Cons 2 (Cons 3 (Cons 6 Nil)))} so weit es geht aus.
 \end{frame}
 
@@ -389,13 +460,13 @@ size (Inner x l r) = 1 + size l + size r
     Der Typ und die Definitionen dieser Fold-Funktionen ergeben sich dabei allein aus den Typen der Konstruktoren. 
     Beispielsweise ist die Fold-Funktion für den Datentyp $\mathbf{Nat}\;a$ aus der vorangegangenen Übung wie folgt definiert:
     \begin{lstlisting}[language=haskell]
-        foldL : c $\rightarrow$ (a $\rightarrow$ c $\rightarrow$ c) $\rightarrow$ List a $\rightarrow$ C
+        foldL : c $\rightarrow$ (a $\rightarrow$ c $\rightarrow$ c) $\rightarrow$ List a $\rightarrow$ c
         foldL n f Nil = n
         foldL n f (Cons x xs) = f x (foldL n f xs)
     \end{lstlisting}
     Hierbei entspricht der Typparameter $c$ einem Ergebnistyp und die beiden Argumente $n$ und $f$ den Konstruktoren $Nil$ und $Cons$, wobei die Typen der Argumente jeweils Operationen
     auf dem Ergebnistyp $c$ beschreiben, mit dem eine Liste $\mathbf{List}\;a$ in einen einzelnen Wert vom Typ $c$ „zusammengefaltet“ werden kann.
-    \\\;\\
+    \vfill
     Finden Sie den Typ und die Definition der entsprechenden Fold-Funktion \texttt{foldT} des parametrischen Datentyps $\mathbf{Tree}\;a$.
 \end{frame}
 
@@ -404,13 +475,13 @@ size (Inner x l r) = 1 + size l + size r
     Der Typ und die Definitionen dieser Fold-Funktionen ergeben sich dabei allein aus den Typen der Konstruktoren. 
     Beispielsweise ist die Fold-Funktion für den Datentyp $\mathbf{Nat}\;a$ aus der vorangegangenen Übung wie folgt definiert:
     \begin{lstlisting}[language=haskell]
-        foldL : c $\rightarrow$ (a $\rightarrow$ c $\rightarrow$ c) $\rightarrow$ List a $\rightarrow$ C
+        foldL : c $\rightarrow$ (a $\rightarrow$ c $\rightarrow$ c) $\rightarrow$ List a $\rightarrow$ c
         foldL n f Nil = n
         foldL n f (Cons x xs) = f x (foldL n f xs)
     \end{lstlisting}
     Hierbei entspricht der Typparameter $c$ einem Ergebnistyp und die beiden Argumente $n$ und $f$ den Konstruktoren $Nil$ und $Cons$, wobei die Typen der Argumente jeweils Operationen
     auf dem Ergebnistyp $c$ beschreiben, mit dem eine Liste $\mathbf{List}\;a$ in einen einzelnen Wert vom Typ $c$ „zusammengefaltet“ werden kann.
-    \\\;\\
+    \vfill
     Primitiv rekursive Funktionen auf $\mathbf{List}\;a$ können durch geeignete Instantiierung des Typparameters $c$ und der Argumente $n$ und $f$ alternativ
     mittels \texttt{foldL} ausgedrückt werden. Drücken Sie die Funktionen \texttt{length} und \texttt{size} jeweils als Folds über Listen und Bäumen aus.
 \end{frame}