Marco/ThProg-Merkzettel
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Anmerkungen am Rand, Subjektreduktion

Browse Source
This commit is contained in:
Marco Ammon 2018-10-03 16:43:55 +02:00
parent 4a22e8f6bc
commit 2c42a5f573
2 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
merkzettel.pdf
View File

Binary file not shown.

8
merkzettel.tex
View File

@ -27,6 +27,8 @@
\newcommand{\defin}[2]{\marginpar{\footnotesize \textit{Def.~#1 (#2)}}} \newcommand{\defin}[2]{\marginpar{\footnotesize \textit{Def.~#1 (#2)}}}
\newcommand{\kor}[2]{\marginpar{\footnotesize \textit{Kor.~#1 (#2)}}} \newcommand{\kor}[2]{\marginpar{\footnotesize \textit{Kor.~#1 (#2)}}}
\newcommand{\lem}[2]{\marginpar{\footnotesize \textit{Lem.~#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. %Abkürzungen für Symbole, Reduktionen, etc.
\newcommand{\app}{\ensuremath{\rightarrow_a}} \newcommand{\app}{\ensuremath{\rightarrow_a}}
@ -78,7 +80,8 @@
\begin{itemize} \begin{itemize}
\item \textbf{TODO} \item \textbf{TODO}
\end{itemize} \end{itemize}
\item Typisierungsprobleme \begin{itemize} \item Typisierungsprobleme \siehe{S. 40}
\begin{itemize}
\item Typcheck: \enquote{Gilt $\Gamma \vdash t:\alpha$?} \item Typcheck: \enquote{Gilt $\Gamma \vdash t:\alpha$?}
\item Typinferenz: \enquote{Was ist das beste $\alpha$ / Existiert $\alpha$ mit $\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$?} \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 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 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 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} \begin{itemize}
\item Menge $PT$ von Typgleichungen \item Menge $PT$ von Typgleichungen
\begin{align*} \begin{align*}
@ -104,6 +107,7 @@
$\Rightarrow$ Prinzipaltyp von $u$: $\text{mgu}(\upvarepsilon)(a)$ $\Rightarrow$ Prinzipaltyp von $u$: $\text{mgu}(\upvarepsilon)(a)$
\end{itemize} \end{itemize}
\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} \end{itemize}
\section*{Unifikationsalgorithmus (Martelli/Montanari)} \section*{Unifikationsalgorithmus (Martelli/Montanari)}
\begin{align*} \begin{align*}