Einfach getypter Lambda-Kalkül, Typinferenz, Unif.

merkzettel.tex

@@ -16,6 +16,7 @@
 \usepackage{pdfpages}
 \usepackage{pgfplots}
 \usepackage{hyperref}
+\usepackage{upgreek}
 \usepackage{tikz}
 \usetikzlibrary{positioning}
 \usetikzlibrary{arrows.meta}
@@ -30,6 +31,7 @@
 %Abkürzungen für Symbole, Reduktionen, etc.
 \newcommand{\app}{\ensuremath{\rightarrow_a}}
 \newcommand{\norm}{\ensuremath{\rightarrow_n}}
+\newcommand{\pteq}{\ensuremath{\overset{\cdot}{=}}}
 
 \theoremstyle{definition}
 \newtheorem{definition}{Definition}[section]
@@ -68,6 +70,50 @@
 		\item terminiert immer, falls Normalform existiert (nach Standardisierungssatz) \satz{3.17}{35}
 	\end{itemize}
 \end{itemize}
-\subsection*{Getypt}
+\subsection*{Einfach getypt $(\lambda \rightarrow)$}
-
+\siehe{S. 39}\begin{itemize}
+	\item Church: Annotation der Variablen mit Typen, nur herleitbare Terme hinschreibbar
+	\item Curry: Alle Terme hinschreibbar, dann Aussondern der nicht typisierbaren
+	\item Typregeln: \siehe{S. 39}
+	\begin{itemize}
+		\item \textbf{TODO}
+	\end{itemize}
+	\item Typisierungsprobleme \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$?}
+	\end{itemize}
+	\item Inversionslemma \lem{3.29}{41} \textbf{TODO}
+	\item Typinferenz \siehe{S. 41}
+	\begin{itemize}
+		\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)
+		\begin{itemize}
+			\item Menge $PT$ von Typgleichungen
+			\begin{align*}
+			PT(\Gamma;x;\alpha) &= \lbrace a\pteq b \vert x:\beta \in \Gamma\rbrace\\
+			PT(\Gamma; \lambda x.t; \alpha) &= PT((\Gamma;x:a);t;b) \cup \lbrace a\rightarrow b \pteq \alpha \rbrace\ \text{mit $a,b$ frisch}\\
+			PT(\Gamma;ts;\alpha) &= PT(\Gamma; t; a\rightarrow \alpha ) \cup PT(\Gamma;s;a)\ \text{mit $a$ frisch}
+			\end{align*}
+			\item Typinferenz des Terms $u$ mit leerem Kontext:
+			\begin{equation*}
+				\upvarepsilon \coloneqq PT(\emptyset;u;a)
+			\end{equation*}
+			$\Rightarrow$ Prinzipaltyp von $u$: $\text{mgu}(\upvarepsilon)(a)$
+		\end{itemize}
+	\end{itemize}
+\end{itemize}
+\section*{Unifikationsalgorithmus (Martelli/Montanari)}
+\begin{align*}
+&S \cup \lbrace x \pteq x\rbrace &&\rightarrow S &&\text{(delete)}\\
+&S \cup \lbrace f(E_1, \ldots, E_n) \pteq f(D_1, \ldots, D_n)\rbrace &&\rightarrow S \cup \lbrace E_1 \pteq D_1, \ldots, E_n \pteq D_n\rbrace &&\text{(decomp)}\\
+&S \cup \lbrace f(E_1, \ldots, E_n) \pteq g(D_1, \ldots, D_k)\rbrace &&\rightarrow \bot \text{ (für $f \not = g$)} &&\text{(conflict)}\\
+&S \cup \lbrace E \pteq x \rbrace &&\rightarrow S \cup \lbrace x \pteq E \rbrace \text{ (für $E$ keine Variable)} &&\text{(orient)}\\
+&S \cup \lbrace x \pteq E \rbrace &&\rightarrow \begin{cases*}
+\bot (\text{für }x \in FV(E), x\not = E) \\
+S\lbrack E/x\rbrack \cup \lbrace x \pteq E\rbrace (\text{für }x\notin FV(E), x\in FV(S))
+\end{cases*} && \text{ (occurs)/(elim)}
+\end{align*}
 \end{document}