diff --git a/merkzettel.pdf b/merkzettel.pdf index ffe471c..0cd21c5 100644 Binary files a/merkzettel.pdf and b/merkzettel.pdf differ diff --git a/merkzettel.tex b/merkzettel.tex index 3d7a0f4..a02df7b 100644 --- a/merkzettel.tex +++ b/merkzettel.tex @@ -27,6 +27,8 @@ \newcommand{\defin}[2]{\marginpar{\footnotesize \textit{Def.~#1 (#2)}}} \newcommand{\kor}[2]{\marginpar{\footnotesize \textit{Kor.~#1 (#2)}}} \newcommand{\lem}[2]{\marginpar{\footnotesize \textit{Lem.~#1 (#2)}}} +\newcommand{\bem}[2]{\marginpar{\footnotesize \textit{Bem.~#1 (#2)}}} +\newcommand{\alg}[2]{\marginpar{\footnotesize \textit{Alg.~#1 (#2)}}} %Abkürzungen für Symbole, Reduktionen, etc. \newcommand{\app}{\ensuremath{\rightarrow_a}} @@ -78,7 +80,8 @@ \begin{itemize} \item \textbf{TODO} \end{itemize} - \item Typisierungsprobleme \begin{itemize} + \item Typisierungsprobleme \siehe{S. 40} + \begin{itemize} \item Typcheck: \enquote{Gilt $\Gamma \vdash t:\alpha$?} \item Typinferenz: \enquote{Was ist das beste $\alpha$ / Existiert $\alpha$ mit $\Gamma \vdash t:\alpha$?} \item Type inhabitation: \enquote{Existiert $t$ mit $\Gamma t:\alpha$?} @@ -89,7 +92,7 @@ \item Typsubstitution $\sigma$ ist Lösung von $\Gamma \vdash t:\alpha$, wenn $\Gamma\sigma \vdash t:\alpha\sigma$ herleitbar \item Substitutionen: $\sigma_1$ allgemeiner als $\sigma_2 \Leftrightarrow \exists \tau. \sigma_1\tau = \sigma_2$ \siehe{GLoIn, S. 38} \item Prinzipaltyp von $\Gamma, t$ ist $\sigma(a)$ für allgemeinste Lösung $\sigma$ von $\Gamma\vdash t:a$ ($a$ frisch) - \item Algorithmus W (Hindley/Milner) + \item Algorithmus W (Hindley/Milner) \alg{3.31}{42} \begin{itemize} \item Menge $PT$ von Typgleichungen \begin{align*} @@ -104,6 +107,7 @@ $\Rightarrow$ Prinzipaltyp von $u$: $\text{mgu}(\upvarepsilon)(a)$ \end{itemize} \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*{Unifikationsalgorithmus (Martelli/Montanari)} \begin{align*}