Teaching/ThProg-SS23
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

finished ue09

Browse source
This commit is contained in:
Leon 2023-06-26 10:20:01 +02:00
parent dd2bb7d142
commit e5cc70baee
2 changed files with 20 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
slides/ThProgUE9.pdf Normal file
View file

Binary file not shown.

28
slides09.tex → texfiles/slides09.tex
View file

@ -206,8 +206,14 @@ Leon Vatthauer}
% Introduction % Introduction
\section{Aufgabe 1 - Beweise mittels struktureller Induktion} \section{Aufgabe 1 - Beweise mittels struktureller Induktion}
\begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion} \begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion}
Wir betrachten die folgenden Funktionen auf Listen: Wir betrachten erneut den Datentyp der Listen sowie die folgenden Funktionen:
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[keywords={data, where, List, Nat}]
data List a where
Nil : () $\rightarrow$ List a
Cons : a $\rightarrow$ List a $\rightarrow$ List a
\end{lstlisting}
\end{minipage}
\begin{minipage}{.45\textwidth} \begin{minipage}{.45\textwidth}
\begin{lstlisting}[keywords={List, Nat}] \begin{lstlisting}[keywords={List, Nat}]
length : List a $\rightarrow$ Nat length : List a $\rightarrow$ Nat
@ -222,7 +228,7 @@ reverse Nil = Nil
reverse (Cons x xs) = snoc (reverse xs) x reverse (Cons x xs) = snoc (reverse xs) x
\end{lstlisting} \end{lstlisting}
\end{minipage} \end{minipage}
\begin{minipage}{.5\textwidth} \begin{minipage}{.45\textwidth}
\begin{lstlisting}[keywords={List, Nat}] \begin{lstlisting}[keywords={List, Nat}]
snoc : List a $\rightarrow$ List a snoc : List a $\rightarrow$ List a
snoc Nil y = Cons y Nil snoc Nil y = Cons y Nil
@ -238,8 +244,14 @@ snoc (Cons x xs) y = Cons x (snoc xs y)
\end{frame} \end{frame}
\begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion} \begin{frame}[t, fragile]{Aufgabe 1}{Beweise mittels struktureller Induktion}
Wir betrachten die folgenden Funktionen auf Listen: Wir betrachten erneut den Datentyp der Listen sowie die folgenden Funktionen:
\begin{minipage}{.45\textwidth}
\begin{lstlisting}[keywords={data, where, List, Nat}]
data List a where
Nil : () $\rightarrow$ List a
Cons : a $\rightarrow$ List a $\rightarrow$ List a
\end{lstlisting}
\end{minipage}
\begin{minipage}{.45\textwidth} \begin{minipage}{.45\textwidth}
\begin{lstlisting}[keywords={List, Nat}] \begin{lstlisting}[keywords={List, Nat}]
length : List a $\rightarrow$ Nat length : List a $\rightarrow$ Nat
@ -254,7 +266,7 @@ reverse Nil = Nil
reverse (Cons x xs) = snoc (reverse xs) x reverse (Cons x xs) = snoc (reverse xs) x
\end{lstlisting} \end{lstlisting}
\end{minipage} \end{minipage}
\begin{minipage}{.5\textwidth} \begin{minipage}{.45\textwidth}
\begin{lstlisting}[keywords={List, Nat}] \begin{lstlisting}[keywords={List, Nat}]
snoc : List a $\rightarrow$ List a snoc : List a $\rightarrow$ List a
snoc Nil y = Cons y Nil snoc Nil y = Cons y Nil
@ -308,13 +320,13 @@ size (Inner x l r) = 1 + size l + size r
\end{minipage} \end{minipage}
\vfill \vfill
Definieren Sie induktiv eine Funktion \lstinline[keywords={List, Tree}]{inorder : Tree a $\rightarrow$ List a}, die die Elemente eines Baumes 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 gemäß einer 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}$$ $$\forall\texttt{t. length (inorder t) = size t}$$
\end{frame} \end{frame}
\begin{frame}[t, fragile]{Aufgabe 3.2}{Induktion über Bäume} \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 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: bis zu drei Kinder haben, selbst aber keine Werte enthalten:
\begin{lstlisting}[keywords={VarTree}] \begin{lstlisting}[keywords={VarTree, data, where}]
data VarTree a where data VarTree a where
VLeaf : a $\rightarrow$ VarTree a VLeaf : a $\rightarrow$ VarTree a
Node1 : VarTree a $\rightarrow$ VarTree a Node1 : VarTree a $\rightarrow$ VarTree a