diff --git a/slides/ThProgUE10.pdf b/slides/ThProgUE10.pdf new file mode 100644 index 0000000..df705ad Binary files /dev/null and b/slides/ThProgUE10.pdf differ diff --git a/texfiles/slides10.tex b/texfiles/slides10.tex new file mode 100644 index 0000000..4631c71 --- /dev/null +++ b/texfiles/slides10.tex @@ -0,0 +1,316 @@ +% .............................................................................. +% 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{Übung 10 - System F} +\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}{7}{3}{-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}, + keywords=List, + %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{} + +\section{System F} +\begin{frame}[t, fragile]{System F} + System F ist eine Erweiterung des einfach getypten $\lambda$-Kalküls um Polymorphie. Wir erweitern die Typgrammatik: + \[ + \alpha, \beta ::= a\;\vert\; \alpha \rightarrow \beta \;\vert\; \forall a. \alpha \qquad (a \in \mathbf{V}) + \] + + Die Typisierungsregeln sind: + \[ + \begin{array}{c 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} + &\infer* [left=($\forall_i$), right=$a \not\in FV(\Gamma)$] {\Gamma \vdash s : \alpha} {\Gamma \vdash s : \forall a. \alpha} + \\\\ + \multicolumn{2}{c}{ + \infer* [left=\text{($\rightarrow_e$)}] {\Gamma \vdash t : \alpha \rightarrow \beta \\ \Gamma \vdash s : \alpha} {\Gamma \vdash t\;s : \beta} + } + &\infer* [left=($\forall_e$)] {\Gamma \vdash s : \forall a.\alpha} {\Gamma \vdash s : (\alpha [\beta / a])} + \end{array} + \] +\end{frame} + +% Introduction +\section{Aufgabe 1 - Produkte in System F (a la Curry)} +\begin{frame}[t, fragile]{Aufgabe 1}{Produkte in System F (à la Curry)} + Wir kodieren das kartesische Produkt der Typen $a$ und $b$ in System F unter Verwendung des Typs $(a \times b) := \forall r. (a \rightarrow b \rightarrow r) \rightarrow r$ + \vfill + \begin{enumerate} + \item + Für diese Kodierung ist die ``Konstruktions-Funktion'' $pair$, welche aus zwei Elementen der Typen $a$ bzw. $b$ ein Paar des Typs $(a \times b)$ konstruiert, wie folgt definiert: + \[ + pair = \lambda x\;y . (\lambda f.\;f\;x\;y) + \] + Zeigen Sie, dass $\vdash pair : \forall a\;b.\; a \rightarrow b \rightarrow (a \times b)$ in System F gilt. + \pause + \\\;\\ + \item + Geben Sie zu jeder der folgenden Funktionssignaturen eine Implementierung der jeweiligen Funktion (d.h. einen $\lambda$-Term) an und zeigen Sie, dass Ihre Implementierung den benötigten Typ hat: + \begin{enumerate} + \item[(a)] $fst : \forall a\;b.\;(a \times b) \rightarrow a$ + \item[(b)] $snd : \forall a\;b.\;(a \times b) \rightarrow b$ + \end{enumerate} + \end{enumerate} +\end{frame} + +\begin{frame}[t, fragile]{Aufgabe 1}{Produkte in System F (à la Curry)} + Wir kodieren das kartesische Produkt der Typen $a$ und $b$ in System F unter Verwendung des Typs $(a \times b) := \forall r. (a \rightarrow b \rightarrow r) \rightarrow r$ + \vfill + \begin{enumerate} + \item[3.] + Schreiben Sie unter Verwendung der obigen Funktionen eine weitere Funktion + \[ + swap : \forall a\;b. (a \times b) \rightarrow (b \times a) + \] + und zeigen Sie, dass sie den korrekten Typ hat. Finden Sie also einen $\lambda$-Term $s$, so dass + $\Gamma\vdash s : \forall a\;b. (a \times b) \rightarrow (b \times a)$, wobei + \begin{align*} + \Gamma := \{ &pair : \forall a\;b. a \rightarrow b \rightarrow (a \times b), + \\&fst : \forall a\;b.\; (a \times b) \rightarrow a, + \\&snd : \forall a\;b.\;(a \times b) \rightarrow b \} + \end{align*} + \end{enumerate} +\end{frame} + +\begin{frame}[t, fragile]{Aufgabe 2}{Listen in System F (à la Curry)} + Listen können in System F unter Verwendung des folgenden Typs kodiert werden: + \begin{lstlisting}[keywords=List] + List a := $\forall r.\; r\rightarrow (a \rightarrow r \rightarrow r) \rightarrow r$ + \end{lstlisting} + In diesem Fall ergeben sich die folgenden ``Konstruktor-Funktionen'': + \begin{lstlisting} + nil = $\lambda$ u f. u + cons = $\lambda$x l.$\lambda$ u f. f x (l u f) + \end{lstlisting} + Für einen gegebenen (und durch \texttt{nil} und \texttt{cons} konstruierten) Term \texttt{t} des Typs \lstinline[keywords=List]|List a| + verhält sich der Term '\lstinline|t u ($\lambda$x l. s)|' also genau so wie eine Funktion \texttt{f} für die für alle x (des Typs a) und alle l (des Typs \lstinline[keywords=List]|List a|) gilt: + \begin{alignat*}{2} + &f\;nil &&\rightarrow_{\beta\delta}^* u\\ + &f\;(cons\;x\;nil) &&\rightarrow_{\beta\delta}^* s[l \mapsto f\;l] + \end{alignat*} + \vfill + \begin{enumerate} + \item Zeigen Sie, dass: + \begin{itemize} + \item[(a)] \lstinline|$\vdash$ nil : $\forall$ a. List a | + \item[(b)] \lstinline|$\vdash$ cons : $\forall$ a.a $\rightarrow$ List a $\rightarrow$ List a| + \end{itemize} + \end{enumerate} +\end{frame} + +\begin{frame}[t, fragile]{Aufgabe 2}{Listen in System F (à la Curry)} + Listen können in System F unter Verwendung des folgenden Typs kodiert werden: + \begin{lstlisting}[keywords=List] + List a := $\forall r.\; r\rightarrow (a \rightarrow r \rightarrow r) \rightarrow r$ + \end{lstlisting} + In diesem Fall ergeben sich die folgenden ``Konstruktor-Funktionen'': + \begin{lstlisting} + nil = $\lambda$ u f. u + cons = $\lambda$x l.$\lambda$ u f. f x (l u f) + \end{lstlisting} + \vfill + \begin{enumerate} + \item[2.] Schreiben Sie eine Funktion \texttt{length}, welche die Länge einer Liste berechnet. Es soll gelten: + \begin{alignat*}{2} + &\texttt{length nil} &&\rightarrow_{\beta\delta}^* \texttt{zero}\\ + &\texttt{length (cons x l)} &&\rightarrow_{\beta\delta}^* \texttt{succ (length l)} + \end{alignat*} + Zeigen Sie, dass \lstinline|$\Gamma_0 \vdash$ length : $\forall$ a. List a $\rightarrow$ $\mathbb{N}$|, wobei $\Gamma_0 := \{\texttt{zero} : \mathbb{N}, succ : \mathbb{N} \rightarrow \mathbb{N}\}$. + \end{enumerate} +\end{frame} +\end{document} \ No newline at end of file