Unverified Commit ace9f2bc authored by Philip K.'s avatar Philip K. 🌝
Browse files

strukturell: wrote up initial draft

parent 58d5344e
\section{Strukturelle Induktion und Folds \hfill 9 Punkte}
Definiert Seien
data Nat = Z | S Nat
Z + s = s
(S n) + s = S (n + s)
data String = Empty | Cons ???
Als bekannt darf
\[ \mathtt{Empty} \oplus t = t \]
\[ (\mathtt{Cons}\; x\; s) \oplus t = \mathtt{Cons}\; x\; (s \oplus
t) \]
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:
unary Z = Empty
unary (S n) = Cons 'Z' (unary n)
\item \points{6}
\item \points{3}
\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
data NatTree where
leaf: Nat -> NatTree
branch: NatTree -> NatTree -> NatTree
%%% 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