diff --git a/slides08.tex b/slides08.tex new file mode 100644 index 0000000..1478463 --- /dev/null +++ b/slides08.tex @@ -0,0 +1,419 @@ +% .............................................................................. +% Demo of the fau-beamer template. +% +% Copyright 2022 by Tim Roith +% +% This program can be redistributed and/or modified under the terms +% of the GNU Public License, version 2. +% +% ------------------------------------------------------------------------------ +\documentclass[final]{beamer} + +% ======================================================================================== +% Theme: inner, outer, font and colors +% ---------------------------------------------------------------------------------------- +\usepackage[institute=Tech, + %SecondLogo = template-art/FAUWortmarkeBlau.pdf, + %ThirdLogo = template-art/FAUWortmarkeBlau.pdf, + %WordMark=None, + aspectratio=169, + fontsize=11, + fontbaselineskip=13, + scale=1. + ]{styles/beamerthemefau} +% ---------------------------------------------------------------------------------------- +% Input and output encoding +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +% ---------------------------------------------------------------------------------------- +% Language settings +\usepackage[german]{babel} + +% ======================================================================================== +% Fonts +% - Helvet is loaded by styles/beamerfonts +% - We use serif for math environements +% - isomath is used for upGreek letters +% ---------------------------------------------------------------------------------------- +\usepackage{isomath} +%\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} + +% ======================================================================================== +% Setup for Titlepage +% ---------------------------------------------------------------------------------------- +\title[fau-beamer]{Theorie der Programmierung} +\subtitle{\texorpdfstring{Übung 08 - Curry-Howard und induktive Datentypen}{Übung 08 - Curry-Howard und induktive Datentypen}} +\author[L. Vatthauer]{ +Leon Vatthauer} +% + +% Instead of \institute you can also use the \thanks command +% ------------------------------------------------ +%\author[T. Roith]{ +%Tim Roith\thanks{Friedrich-Alexander Universität Erlangen-Nürnberg, Department Mathematik}\and% +%Second Author\thanks{Second Insitute}\and% +%Third Author\thanks{Third Insitute}% +%} + +\usepackage[useregional]{datetime2} + +\date{\DTMdisplaydate{2023}{6}{19}{-1}} + + +% ================================================ +% Bibliography +% ------------------------------------------------ +\usepackage{csquotes} +\usepackage[style=alphabetic, %alternatively: numeric, numeric-comp, and other from biblatex + defernumbers=true, + useprefix=true,% + giveninits=true,% + hyperref=true,% + autocite=inline,% + maxcitenames=5,% + maxbibnames=20,% + uniquename=init,% + sortcites=true,% sort citations when multiple entries are passed to one cite command + doi=true,% + isbn=false,% + url=false,% + eprint=false,% + backend=biber% + ]{biblatex} +\addbibresource{bibliography.bib} +\setbeamertemplate{bibliography item}[text] +\babeltags{en=english} + +% ================================================ +% Hyperref and setup +% ------------------------------------------------ +\usepackage{hyperref} +\hypersetup{ + colorlinks = true, + final=true, + plainpages=false, + pdfstartview=FitV, + pdftoolbar=true, + pdfmenubar=true, + pdfencoding=auto, + psdextra, + bookmarksopen=true, + bookmarksnumbered=true, + breaklinks=true, + linktocpage=true, + urlcolor=BaseColor, + citecolor=BaseColor, + linkcolor=BaseColor, + unicode = true +} + +% ================================================ +% Additional packages +% ------------------------------------------------ +\usepackage{listings} +\usepackage{lstautogobble} % Fix relative indenting +\usepackage{color} % Code coloring +\usepackage{zi4} % Nice font + +\definecolor{bluekeywords}{rgb}{0.13, 0.13, 1} +\definecolor{greencomments}{rgb}{0, 0.5, 0} +\definecolor{redstrings}{rgb}{0.9, 0, 0} +\definecolor{graynumbers}{rgb}{0.5, 0.5, 0.5} +\lstset{ + %autogobble, + columns=fullflexible, + showspaces=false, + showtabs=false, + breaklines=true, + showstringspaces=false, + breakatwhitespace=true, + escapeinside={(*@}{@*)}, + commentstyle=\color{greencomments}, + %keywordstyle=\color{bluekeywords}, + stringstyle=\color{redstrings}, + numberstyle=\color{graynumbers}, + basicstyle=\ttfamily\normalsize, + mathescape=true, + %frame=l, + framesep=12pt, + %xleftmargin=.1\textwidth,%12pt, + tabsize=4, + captionpos=b +} +\usepackage{mathpartir} +\usepackage{enumerate} +\usepackage{multicol} +%\usepackage[centercolon=true]{mathtools} +% end of listings setup + +% ================================================ +% Various custom commands +% ------------------------------------------------ +%\setbeameroption{show notes on second screen} +\begingroup\expandafter\expandafter\expandafter\endgroup +\expandafter\ifx\csname pdfsuppresswarningpagegroup\endcsname\relax +\else + \pdfsuppresswarningpagegroup=1\relax +\fi +% Change color for cite locally +\newcommand{\colorcite}[3]{{\hypersetup{citecolor=#1}{\cite[#2]{#3}}}} +% ------------------------------------------------ +% ================================================ +% The main document +% ------------------------------------------------ +\begin{document} +% Title page +\begin{frame}[t, titleimage]{-} +\titlepage% +\end{frame} + +\newcommand{\isaeq}{=_\alpha^?} +\newcommand{\isbr}{\rightarrow_\beta^?} + +\newcommand{\betared}{\rightarrow_\beta} +\newcommand{\alphaeq}{=_\alpha} +\newcommand{\deltared}{\rightarrow_\delta} +\newcommand{\etared}{\rightarrow_\eta} +\newcommand{\betadeltared}{\rightarrow_{\beta\delta}^*} + +\newcommand{\ceil}[1]{\lceil {#1} \rceil} + +\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} +} + +\AtBeginSection{} + +% Introduction +\section{Aufgabe 1 - Der Curry-Howard-Isomorphismus} +\begin{frame}[t, fragile]{Aufgabe 1}{Der Curry-Howard-Isomorphismus} +Wie bereits in der Hausaufgabe zum letzten Blatt angedeutet, gibt es eine Korrespondenz zwischen \textit{minimaler Logik} +und Inhabitation im einfach getypten $\lambda$-Kalkül. +\\\;\\ +Minimale Logik besitzt eine sehr eingeschränkte Syntax; allerdings haben wir in den letzten Wochen auch gelernt, dass sich +im ungetypten $\lambda$-Kalkül mittels Church-Kodierung auch Terme für z.B. Paare von Werten finden lassen: +Nehmen wir an, $\Gamma \vdash t : \tau$ sowie $\Gamma\vdash s : \sigma$. Per Definition aus Übung 5, Blatt 4, ist dann $pair\;t\;s = \lambda select. select\;t\;s$ +Der Prinzipaltyp dieses Terms lässt sich einfach bestimmen: er lautet $(\tau \rightarrow \sigma \rightarrow \alpha)\rightarrow\alpha$. Sie werden jedoch feststellen, dass es keine +Möglichkeit gibt (warum?), einen allgemeinen Typkonstruktor für Paare zu simulieren. Wir werden später ein Typsystem kennenlernen, das es uns erlaubt, über Typvariablen zu +quantifizieren und damit das gewünschte zu erreichen. +\end{frame} + + +\begin{frame}[t, fragile]{Aufgabe 1.1}{Der Curry-Howard-Isomorphismus} +Für den Moment wollen wir uns jedoch damit zufriedengeben, den einfach getypten $\lambda$-Kalkül um einen solchen Typkonstruktor zu erweitern. +Die neue Grammatik für Typen lautet: +\[ +\tau,\sigma ::= a \;\vert\; \mathbf{b} \;\vert\; \tau\rightarrow\sigma \;\vert\; \tau \times \sigma \qquad\qquad a \in \mathbf{V}, \mathbf{b} \in \mathbf{B} +\] + +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 +\] +\;\\ +Geben Sie die zusätzlich benötigten Typisierungsregeln an und erweitern Sie ebenso die Auswertungsrelation um Grundreduktion für Paare. + +\end{frame} + +\begin{frame}[t, fragile]{Aufgabe 1.1}{Recall: einfach getypter $\lambda$-Kalkül} +\typing +\end{frame} + +\begin{frame}[t, fragile]{Aufgabe 1.2}{Der Curry-Howard-Isomorphismus} + +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 +\] +wobei $a$ propositionale Variablen sind. Als Deduktionssystem verwenden wir den Sequentenkalkül minimaler Logik mit folgenden zusätzlichen Regeln: +\[ +\begin{array}{c c c} + \infer* [left=$\land_{E1}$] {\Gamma\vdash \phi \land \psi} {\Gamma\vdash \phi} & \infer* [left=$\land_{E2}$] {\Gamma\vdash \phi \land \psi} {\Gamma\vdash \psi} & \infer* [left=$\land_{I}$] {\Gamma\vdash \phi \\ \Gamma\vdash \psi} {\Gamma\vdash \phi \land \psi} +\end{array} +\] +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} +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) +\] +\end{frame} + +\section{Aufgabe 2 - Listen und Bäume} + +\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$: + +\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 $\ \ $: () $\rightarrow$ Tree a + Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a + \end{lstlisting} +\end{minipage} +\;\\ +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} + \item Nil + \item Cons 5 Nil + \item Leaf 13 + \item Inner 5 (Leaf 3) (Leaf 9) + \item Cons 5 (Cons 5 Nil) + \item Cons 1 (Cons 2 (Cons 3 4 Nil)) + \item Inner 8 (Inner 4 (Leaf 1) (Leaf 20)) (Leaf 8) + \item Inner 6 (Leaf 99) (Inner 1 (Leaf 4) (Leaf 6)) + \end{itemize} +\end{multicols} +\end{frame} + +\begin{frame}[t,fragile]{Aufgabe 2.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 $\ \ $: () $\rightarrow$ Tree a + Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a + \end{lstlisting} + \end{minipage} + \;\\ + Es können nun Funktionen induktiv über der Struktur von $\mathbf{List}\;a$ und $\mathbf{Tree}\;a$ definiert werden, beispielsweise: + + \begin{minipage}{.41\textwidth} + \begin{lstlisting}[] +length Nil $\ \ \ \ \ \ \ \ $= 0 +length (Cons x xs) = 1 + length xs + \end{lstlisting} + \end{minipage} + \begin{minipage}{.58\textwidth} + \begin{lstlisting}[] +size (Leaf x) $\ \ \ \ \ $= 1 +size (Inner x l r) = 1 + size l + size r + \end{lstlisting} + \end{minipage} + \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. + \end{enumerate} + \end{frame} + +\begin{frame}[t,fragile]{Aufgabe 2.3}{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 $\ \ $: () $\rightarrow$ Tree a + Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a + \end{lstlisting} + \end{minipage} + \;\\ + Es können nun Funktionen induktiv über der Struktur von $\mathbf{List}\;a$ und $\mathbf{Tree}\;a$ definiert werden, beispielsweise: + + \begin{minipage}{.41\textwidth} + \begin{lstlisting}[] +length Nil $\ \ \ \ \ \ \ \ $= 0 +length (Cons x xs) = 1 + length xs + \end{lstlisting} + \end{minipage} + \begin{minipage}{.58\textwidth} + \begin{lstlisting}[] +size (Leaf x) $\ \ \ \ \ $= 1 +size (Inner x l r) = 1 + size l + size r + \end{lstlisting} + \end{minipage} + 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} + +\begin{frame}[t, fragile]{Aufgabe 3.1}{Fold-Funktionen} + Jeder induktive Datentyp besitzt eine Fold-Funktion, die sich aus der initialen Algebrastruktur des Typs ergibt. + 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 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. + \\\;\\ + Werten Sie den Term \texttt{foldL n f (Cons 2 (Cons 3 (Cons 6 Nil)))} so weit es geht aus. +\end{frame} + +\begin{frame}[t, fragile]{Aufgabe 3.2}{Fold-Funktionen} + Jeder induktive Datentyp besitzt eine Fold-Funktion, die sich aus der initialen Algebrastruktur des Typs ergibt. + 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 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. + \\\;\\ + Finden Sie den Typ und die Definition der entsprechenden Fold-Funktion \texttt{foldT} des parametrischen Datentyps $\mathbf{Tree}\;a$. +\end{frame} + +\begin{frame}[t, fragile]{Aufgabe 3.3}{Fold-Funktionen} + Jeder induktive Datentyp besitzt eine Fold-Funktion, die sich aus der initialen Algebrastruktur des Typs ergibt. + 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 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. + \\\;\\ + 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} +% input exmple sections +%\input{sections/01_Intro_Landscape} +\end{document} \ No newline at end of file diff --git a/texfiles/slides06.tex b/texfiles/slides06.tex index fbfa7f7..fc9582a 100755 --- a/texfiles/slides06.tex +++ b/texfiles/slides06.tex @@ -66,8 +66,9 @@ Leon Vatthauer} %Second Author\thanks{Second Insitute}\and% %Third Author\thanks{Third Insitute}% %} +\usepackage[useregional]{datetime2} -\date{\today} +\date{\DTMdisplaydate{2023}{6}{5}{-1}} % ================================================ @@ -339,7 +340,7 @@ Leon Vatthauer} Schreiben Sie eine rekursive Funktion $odd$, sodass: \[ odd\,\ceil{n} = \begin{cases} - true & \text{falls } n \text{ gerade}\\ + true & \text{falls } n \text{ ungerade}\\ false & \text{sonst} \end{cases} \] @@ -406,7 +407,7 @@ Diese unterscheiden sich hauptsächlich in den Zeitpunkten, zu denen $\beta$-Red Wir schreiben wie aus der Vorlesung bekannt $I = (\lambda x.\,x)$ und $\Omega = (\lambda x.\,x\,x)$. - Reduzieren Sie den Term $\lambda f.\,f\,I\,(\Omega\,\Omega)(\lambda x\,y.\,x\,x)$ mittels + Reduzieren Sie den Term $(\lambda f.\,f\,I\,(\Omega\,\Omega))(\lambda x\,y.\,x\,x)$ mittels \begin{enumerate} \item[(a)] applikativer Reduktion, \item[(b)] normaler Reduktion. diff --git a/slides07.tex b/texfiles/slides07.tex similarity index 98% rename from slides07.tex rename to texfiles/slides07.tex index c505953..37b8b85 100755 --- a/slides07.tex +++ b/texfiles/slides07.tex @@ -50,7 +50,7 @@ % Setup for Titlepage % ---------------------------------------------------------------------------------------- \title[fau-beamer]{Theorie der Programmierung} -\subtitle{\texorpdfstring{Übung 07 - Der einfach getypte $\lambda$-Kalkül}{Übung 05 - Der einfach getypte Lambda-Kalkül}} +\subtitle{\texorpdfstring{Übung 07 - Der einfach getypte $\lambda$-Kalkül}{Übung 07 - Der einfach getypte Lambda-Kalkül}} \author[L. Vatthauer]{ Leon Vatthauer} % @@ -63,7 +63,9 @@ Leon Vatthauer} %Third Author\thanks{Third Insitute}% %} -\date{\today} +\usepackage[useregional]{datetime2} + +\date{\DTMdisplaydate{2023}{6}{12}{-1}} % ================================================ diff --git a/texfiles/ueb07.hs b/texfiles/ueb07.hs new file mode 100644 index 0000000..dbd6520 --- /dev/null +++ b/texfiles/ueb07.hs @@ -0,0 +1,6 @@ + +add :: Int -> Int -> Int +add n m = n + m + +len :: String -> Int +len str = Prelude.length str