From d66f4faa7e99025e56b883b8a4c44830f0dd9c6e Mon Sep 17 00:00:00 2001 From: reijix Date: Fri, 9 Jun 2023 17:05:14 +0200 Subject: [PATCH] Adding slides for sheet 07 --- texfiles/slides07.tex => slides07.tex | 145 ++++++++++++++++++++++---- slides06.tex => texfiles/slides06.tex | 0 2 files changed, 123 insertions(+), 22 deletions(-) rename texfiles/slides07.tex => slides07.tex (52%) rename slides06.tex => texfiles/slides06.tex (100%) diff --git a/texfiles/slides07.tex b/slides07.tex similarity index 52% rename from texfiles/slides07.tex rename to slides07.tex index 0626421..c505953 100755 --- a/texfiles/slides07.tex +++ b/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. - \\\;\\ - \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. + \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. + \\\;\\ + 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} \ No newline at end of file diff --git a/slides06.tex b/texfiles/slides06.tex similarity index 100% rename from slides06.tex rename to texfiles/slides06.tex