diff --git a/merkzettel.pdf b/merkzettel.pdf index 0cd21c5..bdf2e6e 100644 Binary files a/merkzettel.pdf and b/merkzettel.pdf differ diff --git a/merkzettel.tex b/merkzettel.tex index a02df7b..ef9760e 100644 --- a/merkzettel.tex +++ b/merkzettel.tex @@ -109,6 +109,34 @@ \end{itemize} \item Subjektreduktion: Wenn $\Gamma\vdash t:\alpha$ und $t \rightarrow_\beta^* s$, dann auch $\Gamma \vdash s:\alpha$, aber nicht umgekehrt! \satz{3.38}{45} \end{itemize} +\section*{Induktive Datentypen} +\subsection*{Mehrsortigkeit} +\subsection*{Strukturelle Induktion} +\begin{itemize} +\item über einsortige Datentypen \siehe{S. 63} +\begin{itemize} + \item Induktionsanfang: \enquote{Anfangs}-Konstruktor (etwa $Nil$) + \item Induktionsschritt: alle anderen Konstruktoren (etwa $cons$) +\end{itemize} +\item über mehrsortige Datentypen \siehe{S. 64} +\begin{itemize} + \item Funktionen müssen immer auf allen Datentypen definiert werden +\end{itemize} +\end{itemize} +\subsection*{Kodatentypen} +\subsection*{Koinduktion} +\begin{itemize} + \item Bisimulation $R\subseteq A^\omega \times A^\omega$, wenn für alle $(s,t) \in R$ gilt: \defin{4.39}{74} + \begin{align*} + hd\ s &= hd\ t\\ + (tl\ s)\ &R\ (tl\ t) + \end{align*} + \item Wenn $R$ eine Bisimulation ist, gilt $sRt \Rightarrow s=t$ \satz{4.40}{74} +\end{itemize} +\subsection*{Kodatentypen mit Alternativen} +\section*{System F} +\section*{Polymorphie} +\subsection*{ML-Polymorphie} \section*{Unifikationsalgorithmus (Martelli/Montanari)} \begin{align*} &S \cup \lbrace x \pteq x\rbrace &&\rightarrow S &&\text{(delete)}\\