Added slides10
This commit is contained in:
parent
e5cc70baee
commit
3fa889d223
2 changed files with 316 additions and 0 deletions
BIN
slides/ThProgUE10.pdf
Normal file
BIN
slides/ThProgUE10.pdf
Normal file
Binary file not shown.
316
texfiles/slides10.tex
Normal file
316
texfiles/slides10.tex
Normal file
|
|
@ -0,0 +1,316 @@
|
|||
% ..............................................................................
|
||||
% Demo of the fau-beamer template.
|
||||
%
|
||||
% Copyright 2022 by Tim Roith <tim.roith@fau.de>
|
||||
%
|
||||
% 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}
|
||||
Loading…
Reference in a new issue