Unverified Commit fae42b03 authored by Philip K.'s avatar Philip K. 🌝

strukturell: applied new input from realisation

parent 40d988b5
......@@ -10,7 +10,7 @@ data String where
Cons: char -> String -> String
\end{verbatim}
Als bekannt darf
Auf diesen Typen sind die Operationen "`$\oplus : \mathtt{String} \rightarrow \mathtt{String} \rightarrow \mathtt{String}$"' und "`$+ : \mathtt{Nat} \rightarrow \mathtt{Nat} \rightarrow \mathtt{Nat}$"' definiert:
\begin{multicols}{2}
\begin{math}
\mathtt{Empty} \oplus t = t\\
......@@ -19,31 +19,39 @@ Als bekannt darf
(\mathtt{S}\; n) + m = \mathtt{S}\; (n + m)
\end{math}
\end{multicols}
angenommen werden.
Die Funktion \texttt{unary}, welche ein \texttt{Nat} in die unäre
Mitetls der \emph{fold}-Funktion für natürliche Zahlen
\begin{verbatim}
foldN : a -> (a -> a) -> Nat -> a
foldN x f Z = x
foldn x f (S n) = f (foldN x f n)
\end{verbatim}
ist die Funktion \texttt{unary}, welche ein \texttt{Nat} in die unäre
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:
Per Definition, besitzt diese Funktion die Eigenschaft:
\begin{verbatim}
unary (S n) = Cons '|' (unary n)
\end{verbatim}
Sie können diese Aussage verwenden.
\begin{enumerate}
\item Beweisen\points{6} Sie mittels Induktion, dass
\item Beweisen\points{6} Sie mittels struktureller Induktion folgende
weitere Eigenschaft:
\[ \forall n, m \in \mathtt{Nat} \,.\, (\mathtt{unary}\;n) \oplus
(\mathtt{unary}\;m) = \mathtt{unary}\;(n + m) \]
\item Geben\points{3} Sie Typ und Definition einer \emph{fold} Funktion, für
\texttt{NatTree} an, definiert als
\item Betrachten\points{3} Sie diese Variante eines Binärbaums, bei dem alle
Knoten durch Natürliche Zahlen gelabelt' sind:
\begin{verbatim}
data NatTree where
leaf: Nat -> NatTree
branch: NatTree -> NatTree -> NatTree
\end{verbatim}
Geben Sie Typ und Definition einer \emph{fold} Funktion, für
\texttt{NatTree} an.
\end{enumerate}
%%% Local Variables:
......
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