From dd2bb7d142244bc3129ee6637aaa3a73c119e412 Mon Sep 17 00:00:00 2001 From: reijix Date: Sat, 24 Jun 2023 15:04:41 +0200 Subject: [PATCH] Working on ueb09 --- slides09.tex | 334 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 334 insertions(+) create mode 100644 slides09.tex diff --git a/slides09.tex b/slides09.tex new file mode 100644 index 0000000..be17d94 --- /dev/null +++ b/slides09.tex @@ -0,0 +1,334 @@ +% .............................................................................. +% 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 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} \ No newline at end of file