Working on ueb09
This commit is contained in:
parent
dc416791a3
commit
dd2bb7d142
1 changed files with 334 additions and 0 deletions
334
slides09.tex
Normal file
334
slides09.tex
Normal file
|
|
@ -0,0 +1,334 @@
|
||||||
|
% ..............................................................................
|
||||||
|
% 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 09 - Strukturelle Induktion}{Übung 09 - Strukturelle Induktion}}
|
||||||
|
\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}{26}{-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 - Beweise mittels struktureller Induktion}
|
||||||
|
\begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion}
|
||||||
|
Wir betrachten die folgenden Funktionen auf Listen:
|
||||||
|
|
||||||
|
\begin{minipage}{.45\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat}]
|
||||||
|
length : List a $\rightarrow$ Nat
|
||||||
|
length Nil = 0
|
||||||
|
length (Cons x xs) = 1 + length xs
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\begin{minipage}{.5\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat}]
|
||||||
|
reverse : List a $\rightarrow$ List a
|
||||||
|
reverse Nil = Nil
|
||||||
|
reverse (Cons x xs) = snoc (reverse xs) x
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\begin{minipage}{.5\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat}]
|
||||||
|
snoc : List a $\rightarrow$ List a
|
||||||
|
snoc Nil y = Cons y Nil
|
||||||
|
snoc (Cons x xs) y = Cons x (snoc xs y)
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
|
||||||
|
Wir zeigen einige Eigenschaften dieser Funktionen. Beweisen Sie diese jeweils durch Induktion über der Struktur der Argumentliste.
|
||||||
|
Rechtfertigen Sie hierbei Ihre Schritte und geben Sie jeweils ihre Induktionshypothese an.
|
||||||
|
|
||||||
|
\textit{Hinweis:} Wir erinnern daran, dass $s = t$ als $s \leftrightarrow_{\beta\delta} t$ zu lesen ist.
|
||||||
|
Außerdem können Sie jederzeit zuvor bewiesene Eigenschaften verwenden.
|
||||||
|
\end{frame}
|
||||||
|
|
||||||
|
\begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion}
|
||||||
|
Wir betrachten die folgenden Funktionen auf Listen:
|
||||||
|
|
||||||
|
\begin{minipage}{.45\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat}]
|
||||||
|
length : List a $\rightarrow$ Nat
|
||||||
|
length Nil = 0
|
||||||
|
length (Cons x xs) = 1 + length xs
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\begin{minipage}{.5\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat}]
|
||||||
|
reverse : List a $\rightarrow$ List a
|
||||||
|
reverse Nil = Nil
|
||||||
|
reverse (Cons x xs) = snoc (reverse xs) x
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\begin{minipage}{.5\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat}]
|
||||||
|
snoc : List a $\rightarrow$ List a
|
||||||
|
snoc Nil y = Cons y Nil
|
||||||
|
snoc (Cons x xs) y = Cons x (snoc xs y)
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\vfill
|
||||||
|
Beweisen Sie mittels Induktion:
|
||||||
|
\begin{enumerate}
|
||||||
|
\item \texttt{$\forall$x xs. length (snoc xs x) = 1 + length xs}
|
||||||
|
\pause
|
||||||
|
\item \texttt{$\forall$xs. length (reverse xs) = length xs}
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
\end{frame}
|
||||||
|
|
||||||
|
\section{Aufgabe 2 - Eine binäre Funktion: Listenkonkatenation}
|
||||||
|
\begin{frame}[t, fragile]{Aufgabe 2}{Eine binäre Funktion: Listenkonkatenation}
|
||||||
|
Wir betrachten die folgende Definition einer Funktion zur Listenkonkatenation:
|
||||||
|
\begin{lstlisting}[keywords={List, Nat}]
|
||||||
|
($\oplus$) : List a $\rightarrow$ List a $\rightarrow$ List a
|
||||||
|
Nil $\oplus$ ys = ys
|
||||||
|
(Cons x xs) $\oplus$ ys = Cons x (xs $\oplus$ ys)
|
||||||
|
\end{lstlisting}
|
||||||
|
Wir möchten die folgende Eigenschaft mittels struktureller Induktion beweisen:
|
||||||
|
$$\forall \texttt{xs ys. length (xs $\oplus$ ys) = length xs + length ys}$$
|
||||||
|
\begin{enumerate}
|
||||||
|
\item Über welche Liste(n) sollten wir induzieren, über das erste Argument von (\_ $\oplus$ \_), über das zweite, oder über beide? Warum?
|
||||||
|
\pause
|
||||||
|
\item Beweisen Sie die oben angegebene Eigenschaft; begründen Sie Ihre Schritte und geben Sie explizit an, an welcher Stelle die Induktionshypothese verwendet wird.
|
||||||
|
\end{enumerate}
|
||||||
|
\end{frame}
|
||||||
|
|
||||||
|
\section{Aufgabe 3 - Induktion über Bäume}
|
||||||
|
\begin{frame}[t, fragile]{Aufgabe 3.1}{Induktion über Bäume}
|
||||||
|
Wir erinnern uns an den induktiven Datentyp der binären Bäume von Blatt 8 und die Funktion \texttt{size}, die die Knoten eines Baums zählt:
|
||||||
|
|
||||||
|
\begin{minipage}{.5\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat, Tree, data, where}]
|
||||||
|
data Tree a where
|
||||||
|
Leaf : a $\rightarrow$ Tree a
|
||||||
|
Inner : a $\rightarrow$ Tree a $\rightarrow$ Tree a $\rightarrow$ Tree a
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\begin{minipage}{.49\textwidth}
|
||||||
|
\begin{lstlisting}[keywords={List, Nat, Tree}]
|
||||||
|
size : Tree a $\rightarrow$ Nat
|
||||||
|
size (Leaf x) = 1
|
||||||
|
size (Inner x l r) = 1 + size l + size r
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\vfill
|
||||||
|
Definieren Sie induktiv eine Funktion \lstinline[keywords={List, Tree}]{inorder : Tree a $\rightarrow$ List a}, die die Elemente eines Baumes
|
||||||
|
gemäß ener In-Order-Traversierung von links nach rechts ausgibt. Zeigen Sie dann per struktureller Induktion über Bäume, dass
|
||||||
|
$$\forall\texttt{t. length (inorder t) = size t}$$
|
||||||
|
\end{frame}
|
||||||
|
\begin{frame}[t, fragile]{Aufgabe 3.2}{Induktion über Bäume}
|
||||||
|
Wir betrachten im folgenden einen parametrischen induktiven Datentyp für Bäume, deren Blätter Elemente vom Typ $a$ enthalten, und deren innere Knoten jeweils
|
||||||
|
bis zu drei Kinder haben, selbst aber keine Werte enthalten:
|
||||||
|
\begin{lstlisting}[keywords={VarTree}]
|
||||||
|
data VarTree a where
|
||||||
|
VLeaf : a $\rightarrow$ VarTree a
|
||||||
|
Node1 : VarTree a $\rightarrow$ VarTree a
|
||||||
|
Node2 : VarTree $\rightarrow$ VarTree a $\rightarrow$ VarTree a
|
||||||
|
Node3 : VarTree $\rightarrow$ VarTree a $\rightarrow$ VarTree a $\rightarrow$ VarTree a
|
||||||
|
\end{lstlisting}
|
||||||
|
Hierbe ist also \texttt{Node1} ein Knoten mit einem Nachfolger \texttt{m}, \texttt{Node2 l r} ein Knoten mit einem linken Nachfolger \texttt{l} und rechtem Nachfolger \texttt{r},
|
||||||
|
und \texttt{Node3 l m r} ein Knoten mit linkem Nachfolger \texttt{l}, mittlerem Nachfolger \texttt{m} und rechtem Nachfolger \texttt{r}.
|
||||||
|
\vfill
|
||||||
|
Definieren Sie induktiv eine Funktion \lstinline[keywords=VarTree]{mirror : VarTree a $\rightarrow$ VarTree a}, die einen solchen Baum spiegelt und zeigen Sie
|
||||||
|
per struktureller Induktion, dass \texttt{mirror} eine \textbf{Involution} darstellt, das heißt:
|
||||||
|
\[
|
||||||
|
\forall \texttt{t. mirror (mirror t) = t}
|
||||||
|
\]
|
||||||
|
\end{frame}
|
||||||
|
|
||||||
|
\end{document}
|
||||||
Loading…
Reference in a new issue