Commit 6122bf92 authored by Philip K.'s avatar Philip K. 🌝

Merge branch 'master' into 'master'

Improve Strukturelle Induktion

See merge request !2
parents e47d02a9 58d74750
\section{Strukturelle Induktion und Folds \hfill 9 Punkte}
In dieser Aufgabe wird der Grunddatentyp \texttt{char} verwendet. Es wird die gewöhnliche Schreibweise '\_' für char-Literale benutzt.
Definiert Seien
\begin{verbatim}
data Nat = Z | S Nat
Z + s = s
(S n) + s = S (n + s)
data String = Empty | Cons ???
data String where
Empty: String
Cons: char -> String -> String
\end{verbatim}
Als bekannt darf
\[ \mathtt{Empty} \oplus t = t \]
\[ (\mathtt{Cons}\; x\; s) \oplus t = \mathtt{Cons}\; x\; (s \oplus
t) \]
\begin{multicols}{2}
\begin{math}
\mathtt{Empty} \oplus t = t\\
(\mathtt{Cons}\; x\; s) \oplus t = \mathtt{Cons}\; x\; (s \oplus t)\\
Z + s = s\\
(S\ n) + m = S\ (n + m)
\end{math}
\end{multicols}
angenommen werden.
Die Funktion \texttt{unary}, welche ein \texttt{Nat} in die unäre
Repräsentation dieser Zahl in Form eines Strings darstellt, definiert als:
Repräsentation dieser Zahl in Form eines Strings umwandelt, ist definiert als:
\begin{verbatim}
unary = foldN Empty (Cons '|')
\end{verbatim}
wobei \texttt{foldN} die \emph{fold}-Funktion über die Natürlichen Zahlen (\texttt{Nat}) darstellt.\\
Es kann gezeigt werden, dass gilt:
\begin{verbatim}
unary Z = Empty
unary (S n) = Cons '|' (unary n)
\end{verbatim}
Sie können diese Aussage verwenden.
\begin{enumerate}
\item Beweisen\points{6} Sie mittels Induktion, dass
\[ \forall n, m \in \mathtt{Nat} \,.\, (\mathtt{unary}\;n) \oplus
(\mathtt{unary}\;m) = \mathtt{unary}\;(n + m) \]
\item Schreiben\points{3} Sie eine \emph{fold} Funktion, für
\texttt{NatTree}, definiert als
\item Geben\points{3} Sie Typ und Definition einer \emph{fold} Funktion, für
\texttt{NatTree} an, definiert als
\begin{verbatim}
data NatTree where
leaf: Nat -> NatTree
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment