Adding slides for sheet 07

slides07.tex

@@ -36,14 +36,13 @@
 % - isomath is used for upGreek letters
 % ----------------------------------------------------------------------------------------
 \usepackage{isomath}
-\usefonttheme[onlymath]{serif}
+%\usefonttheme[onlymath]{serif}
 \usepackage{exscale}
 \usepackage{anyfontsize}
 \setbeamercolor{alerted text}{fg=BaseColor}
 % ----------------------------------------------------------------------------------------
 % custom commands for symbols
 \usepackage{styles/symbols}
-
 \usepackage{tikz-cd}
 \usetikzlibrary{cd, babel}
 
@@ -51,7 +50,7 @@
 % Setup for Titlepage
 % ----------------------------------------------------------------------------------------
 \title[fau-beamer]{Theorie der Programmierung}
-\subtitle{\texorpdfstring{Übung 07 - Rekursion und der einfach getypte $\lambda$-Kalkül}{Übung 05 - Rekursion und der einfach getypte Lambda-Kalkül}}
+\subtitle{\texorpdfstring{Übung 07 - Der einfach getypte $\lambda$-Kalkül}{Übung 05 - Der einfach getypte Lambda-Kalkül}}
 \author[L. Vatthauer]{
 Leon Vatthauer}
 %
@@ -147,6 +146,8 @@ Leon Vatthauer}
     tabsize=4,
     captionpos=b
 }
+\usepackage{mathpartir}
+\usepackage{enumerate}
 % end of listings setup
 
 % ================================================
@@ -217,33 +218,133 @@ Leon Vatthauer}
 	\end{block}
 }
 
+\newcommand{\typing}{
+	\begin{block}{Typisierung}
+		Wir lesen $\Gamma \vdash t : \alpha$ als „im Kontext $\Gamma$ hat der Term $t$ den Typ $\alpha$“ und definieren diese Relation wie folgt:
+		\[
+		\begin{array}{c c}
+			\infer* [left=\text{(Ax)}, right=\text{($x : \alpha \in \Gamma$)}]{\;} {\Gamma \vdash x : \alpha} & \infer* [left=\text{($\rightarrow_i$)}] {\Gamma[x\mapsto \alpha] \vdash t : \beta} {\Gamma \vdash \lambda x.t : \alpha \rightarrow \beta}\\
+			\\
+			\multicolumn{2}{c}{
+				\infer* [left=\text{($\rightarrow_e$)}] {\Gamma \vdash t : \alpha \rightarrow \beta \\ \Gamma \vdash s : \alpha} {\Gamma \vdash t\;s : \beta}
+			}
+		\end{array}
+		\]
+	\end{block}
+}
+\newcommand{\inversionlemma}{
+	\begin{block}{Inversionslemma}
+		\begin{enumerate}
+			\item Wenn $\Gamma \vdash x : \alpha$, dann $x : \alpha \in \Gamma$
+			\item Wenn $\Gamma \vdash t\;s : \beta$, dann existiert $\alpha$ mit $\Gamma \vdash t : \alpha \rightarrow \beta$ und $\Gamma \vdash s : \alpha$
+			\item Wenn $\Gamma \vdash \lambda x.t : \gamma$, dann hat $\gamma$ die Form $\gamma = \alpha \rightarrow \beta$ und $\Gamma[x \mapsto \alpha] \vdash t : \beta$
+		\end{enumerate}
+	\end{block}
+}
+
+\newcommand{\algorithmw}{
+	\begin{block}{Algorithmus W nach Hindley/Milner}
+		Wir definieren rekursiv eine Menge $PT(\Gamma;t;\alpha)$ von Typgleichungen, so dass der mgu $\sigma = \mathbf{mgu}(PT(\Gamma;t;\alpha))$ die allgemeinste Lösung von $\Gamma \vdash t : \alpha$ liefert (wenn eine Lösung existiert).
+		\begin{enumerate}
+			\item $PT(\Gamma;\;x;\;\alpha) = \{\alpha \unif \beta \;\vert\; x : \beta \in \Gamma\}$
+			\item $PT(\Gamma;\;\lambda x.t;\; \alpha) = PT ((\Gamma[x \mapsto a]);\;t;\;b) \cup \{a \rightarrow b \unif \alpha\}$, mit $a, b$ frisch
+			\item $PT(\Gamma;\;t\;s;\;\alpha) = PT(\Gamma;\;t;\;a \rightarrow \alpha) \cup PT(\Gamma;\;s;\;a)$, mit $a$ frisch
+		\end{enumerate}
+	\end{block}
+}
+
+\newcommand{\unif}{\overset{.}{=}}
+
 \AtBeginSection{}
 
 % Introduction
-\section{Aufgabe 1 - Rekursive Definitionen II}
-\begin{frame}[t, fragile]{Aufgabe 1}{Rekursive Definitionen II}
+\section{Der einfach getypte Lambda-Kalkül}
+\begin{frame}[t, fragile]{Der einfach getypte $\lambda$-Kalkül $(\lambda\rightarrow)$}{Definitionen}
+	\begin{block}{Typen}
+		Sei $\mathbf{V}$ eine Menge von \textit{Typvariablen} $a,b, $ etc. und $\mathbf{B}$ eine Menge von Basistypen, etwa $\mathbf{Bool, Int}$. Die Grammatik für Typen $\alpha, \beta, \ldots$ ist dann
+		$$\alpha, \beta ::= a\;\vert\;\mathbf{b}\;\vert\;\alpha\rightarrow\beta \qquad (\mathbf{b}\in \mathbf{B}, a \in \mathbf{V})$$
+	\end{block}
+	\begin{block}{Notation}
+		Im Gegensatz zur Applikation von $\lambda$-Termen, welche links-assoziativ ist (also $add\;5\;3 = (add\;5)\;3$),
+		ist der Funktionspfeil rechts-assoziativ, also $\alpha \rightarrow \beta \rightarrow \gamma = \alpha \rightarrow (\beta \rightarrow \gamma)$
+	\end{block}
+	\begin{block}{Kontext}
+		Ein \textit{(Typ-)Kontext} ist eine Menge
+		$$\Gamma = \{x_1 : \alpha_1;\ldots ; x_n : \alpha_n\}$$
+	\end{block}
+\end{frame}
+\begin{frame}[t, fragile]{Der einfach getypte $\lambda$-Kalkül $(\lambda\rightarrow)$}{Definitionen}
+	\typing
+	\inversionlemma
+\end{frame}
 
-	Wir erinnern uns an die rekursiv definierte Fakultätsfunktion vom letzten Blatt:
-	\begin{lstlisting}[language=haskell]
-		fact n = if n $\leq$ $\ceil{\texttt{1}}$ then $\ceil{\texttt{1}}$ else n * (fact (n - $\ceil{\texttt{1}}$))
-	\end{lstlisting}
-	Wir wollen zeigen, dass \texttt{fact} tatsächlich eine korrekte Implementierung der Fakultätsfunktion ist, genauer, dass $fact \ceil{n} \betadeltared \ceil{n!}$ für jede natürliche Zahl $n$.
-	\\\;\\
+\section{Aufgabe 1 - Typprüfung einfach getypter Terme}
+
+\begin{frame}[t, fragile]{Aufgabe 1}{Typprüfung einfach getypter Terme}
+	Zeigen Sie, dass die folgenden Aussagen zutreffen, indem Sie jeweils eine korrekte Typherleitung angeben.
 	\begin{enumerate}
-		\item Bevor wir mit dem Beweis beginnen können, benötigen wir zunächst entsprechende Aussagen über die in obiger Definition von \texttt{fact} verwendeten Funktionen und Operationen.
-		Zum Beispiel benötigen wir, dass $\ceil{n} * \ceil{m} \betadeltared \ceil{n * m}$ für alle $n, m \in \mathbb{N}$. Ergänzen Sie die Aussagen für die restlichen Operationen. 
-		Wir werden diese im Folgenden ohne gesonderten Beweis verwenden.
+		\item $ x : \texttt{int}, add : \texttt{int} \rightarrow \texttt{int} \rightarrow \texttt{int} \vdash \lambda y.add\;x\;(add\;x\;y) : \texttt{int} \rightarrow \texttt{int}$
+		\item $\vdash \lambda xy.x : \alpha \rightarrow \beta \rightarrow \alpha$, für alle Typen $\alpha, \beta$
+	\end{enumerate}
+
+	\vfill
+	\typing
+\end{frame}
+
+\section{Prinzipaltyp}
+
+\begin{frame}[t, fragile]{Algorithmus W nach Hindley/Milner}
+	\begin{block}{Prinzipaltyp}
+		Es sei $t$ ein $\lambda$-Term und $\Gamma$ ein Kontext; wir sagen, dass $\alpha$ der \textit{Prinzipaltyp} (engl. \textit{principal type}) von $t$ ist, 
+		wenn 
+		\begin{enumerate}
+			\item $\Gamma \vdash t : \alpha$
+			\item $\alpha$ allgemeiner ist als jeder Typ $\beta$ mit $\Gamma \vdash t : \beta$
+		\end{enumerate}
+		d.h. wenn jedes solche $\beta$ sich durch Substitution von Typvariablen aus $\alpha$ erzeugen lässt. Beispielsweise ist $a \rightarrow b \rightarrow a$ (für Typvariablen $a$ und $b$) der Prinzipaltyp von $\lambda xy.x$.
+	\end{block}
+
+	\algorithmw
+
+\end{frame}
+
+\section{Aufgabe 2 - Inferenz von Prinzipaltypen}
+
+\begin{frame}[t, fragile]{Aufgabe 2}{Inferenz von Prinzipaltypen}
+	Leiten Sie den Prinzipaltyp der folgenden $\lambda$-Terme in dem jeweils gegebenen Kontext her
+	\begin{enumerate}
+		\item $\Gamma = \emptyset, t = \lambda x y z.x\;(y\;z)$
+		\item $\Gamma = \{add : \texttt{int} \rightarrow \texttt{int} \rightarrow \texttt{int}, length : \texttt{string} \rightarrow \texttt{int}\}, t = \lambda x. add\;(length\; x)$
+	\end{enumerate}
+
+	\vfill
+	\algorithmw
+\end{frame}
+
+\section{Aufgabe 3 - Type Inhabitation und untypisierbare Terme}
+\begin{frame}[t, fragile]{Aufgabe 3.1}{Type Inhabitation und untypisierbare Terme}
+	Das zur Typinferenz symmetrische Problem ist das Problem der \foreignlanguage{english}{\textit{type inhabitation}}, 
+	d.h. das Problem, einen $\lambda$-Term eines gegebenen Typs zu finden, falls ein solcher Term existiert.
+	\\Im Folgenden bezeichnen $p$, $q$ und $r$ Typvariablen.
 	\\\;\\
-		\pause
-		\item Beweisen Sie nun per Induktion, dass $fact \ceil{n} \betadeltared \ceil{n!}$ für alle $n \in \mathbb{N}$. Kennzeichnen Sie dabei, an welchen Stellen die Eigenschaften aus Teilaufgabe 1 einfließen. 
+	Finden Sie für jeden der folgenden Typen $\alpha$ einen $\lambda$-Term $s$, sodass $\vdash s : \alpha$.
+	\begin{enumerate}[(a)]
+		\item $p \rightarrow p$
+		\item $p \rightarrow (q \rightarrow p)$
+		\item $(p \rightarrow (q \rightarrow r)) \rightarrow (p \rightarrow q) \rightarrow p \rightarrow r$
+		\item $((p \rightarrow q) \rightarrow r) \rightarrow q \rightarrow r$
 	\end{enumerate}
 \end{frame}
-
-\section{Der einfach getypte Lambda-Kalkül}
-\begin{frame}[t]{Der einfach getypte $\lambda$-Kalkül}
-	
+\begin{frame}[t, fragile]{Aufgabe 3.2}{Type Inhabitation und untypisierbare Terme}
+	Im Gegenzug dazu gibt es auch Terme, denen man keinen Typ zuordnen kann. 
+	Verwenden Sie das Inversionslemma aus der Vorlesung, um zu zeigen, dass:
+	\begin{enumerate}[(a)]
+		\item $\not\vdash \lambda x.x\;x : \alpha$, für jeden Typ $\alpha$.
+		\item $y : \texttt{char} \not\vdash \lambda x.y\;x : \alpha$, für jeden Typ $\alpha$.
+	\end{enumerate}
+	\vfill
+	\inversionlemma
 \end{frame}
-
 % input exmple sections
 %\input{sections/01_Intro_Landscape}
 \end{document}