Working on slides08
This commit is contained in:
parent
83a6caf07e
commit
afecdc3d44
4 changed files with 433 additions and 5 deletions
419
slides08.tex
Normal file
419
slides08.tex
Normal file
|
|
@ -0,0 +1,419 @@
|
|||
% ..............................................................................
|
||||
% 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{\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}
|
||||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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}}
|
||||
|
||||
|
||||
% ================================================
|
||||
6
texfiles/ueb07.hs
Normal file
6
texfiles/ueb07.hs
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
|
||||
add :: Int -> Int -> Int
|
||||
add n m = n + m
|
||||
|
||||
len :: String -> Int
|
||||
len str = Prelude.length str
|
||||
Loading…
Reference in a new issue