\documentclass[11pt,a4paper]{scrartcl}
\usepackage[a4paper,left=3cm,right=3cm,top=2.5cm,bottom=2.5cm]{geometry}
\usepackage[ngerman]{babel}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathrsfs}
\usepackage{scrextend}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{enumitem}
\usepackage{tikz-qtree}
\usepackage{mathtools}
\usepackage{latexsym}
\usepackage{algorithmicx}
\usepackage{csquotes}
\usepackage{pdfpages}
\usepackage{pgfplots}
\usepackage{hyperref}
\usepackage{upgreek}
\usepackage{tikz}
\usetikzlibrary{positioning}
\usetikzlibrary{arrows.meta}

%Anmerkungen am Rand
\newcommand{\siehe}[1]{\marginpar{\footnotesize \textit{#1}}}
\newcommand{\satz}[2]{\marginpar{\footnotesize \textit{Satz~#1 (#2)}}}
\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}}
\newcommand{\norm}{\ensuremath{\rightarrow_n}}
\newcommand{\pteq}{\ensuremath{\overset{\cdot}{=}}}

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

\title{Merkzettel für \enquote{Theorie der Programmierung}}
\author{Marco Ammon}
\date{\today}

\begin{document}
\maketitle
\section*{Termersetzungssysteme}
\subsection*{Terminierung}
\subsubsection*{Polynomordnungen}
\subsection*{Konfluenz}
\subsection*{Critical Pairs}

\section*{$\lambda$-Kalkül}
\subsection*{Ungetypt}
\subsubsection*{Rekursion}
\subsubsection*{Auswertungsstrategien}
\begin{itemize}
	\item applikativ (\textit{leftmost-innermost}) \app \defin{3.13}{33}
	\begin{itemize}
		\item $\lambda x.t \app \lambda x.t'$, wenn $t \app t'$
		\item $ts \app t's$, wenn $t \app t'$
		\item $ts \app ts'$, wenn $s\app s'$ und $t$ normal ist
		\item $(\lambda x.t)s \app t\lbrack s/x\rbrack$, wenn $t$ und $s$ normal sind
		\item effizient
	\end{itemize}	
	\item normal (\textit{leftmost-outermost}) \norm \defin{3.14}{34}
	\begin{itemize}
		\item $(\lambda x.t) s \norm t\lbrack s/x\rbrack$
		\item $\lambda x.t \norm \lambda x.t'$, wenn $t\norm t'$
		\item $ts \norm t's$m wenn $t\norm t'$ und $t$ keine $\lambda$-Abstraktion ist
		\item $ts \norm ts'$, wenn $s\norm s'$ und $t$ normal und keine $\lambda$-Abstraktion ist
		\item terminiert immer, falls Normalform existiert (nach Standardisierungssatz) \satz{3.17}{35}
	\end{itemize}
\end{itemize}
\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 \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$?}
	\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) \alg{3.31}{42}
		\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}
	\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*{Mengenkonstruktionen}
\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}
\subsection*{Curry}
\begin{itemize}
	\item Typen:\defin{5.1}{84}
	\begin{align*}
	\alpha, \beta \coloneqq a\ \vert\ \alpha \rightarrow \beta\ \vert\ \forall a.\alpha && (a\in V)
	\end{align*}
	\item Typisierung: \textbf{TODO: $\lambda \rightarrow$}, \textbf{TODO} \defin{5.1}{84}
	\begin{align*}
	Inhalt...
	\end{align*}
\end{itemize}
\subsection*{Church-Kodierung}\siehe{S. 84}
\begin{itemize}
	\item Natürliche Zahlen
	\begin{align*}
	\textbf{Todo}
	\end{align*}
	\item Paare
	\begin{align*}
	Inhalt...
	\end{align*}
	\item Summen
	\begin{align*}
	Inhalt...
	\end{align*}
	\item Listen
	\begin{align*}
	Inhalt...
	\end{align*}
\end{itemize}
\subsection*{ML-Polymorphie}
\begin{itemize}
	\item Einschränkung von System F durch $\forall$ nur auf oberster Ebene sowie Mehrfachinstanziierung polymorpher Funktionen nur in $let$-Konstrukt \siehe{S. 88}
	\item Typen
	\begin{equation*}
	\alpha, \beta \coloneqq a\ \vert\ \alpha \rightarrow \beta
	\end{equation*}
	\item Typschemata
	\begin{align*}
	S \coloneqq \forall a_1, \ldots, a_k.\alpha &&(k\geq 0)
	\end{align*}
	\item Terme
	\begin{equation*}
	t,s \coloneqq x\ \vert\ t\ s\ \vert\ \lambda x.t\ \vert\ let\ x = t\ in\ s
	\end{equation*}
	\item Kontexte
	\begin{align*}
		\Gamma &= ( x_1:S_1,\ldots, x_n :S_n )\\
		Cl(\Gamma, \alpha) &= \forall a_1,\ldots,a_k.\alpha &&\text{für $FV(\alpha)\backslash FV(\Gamma) = \lbrace a_1,\ldots,a_k \rbrace$}
	\end{align*}
	\item Typisierungsregeln \textbf{TODO}
	\item Inversionslemma \textbf{TODO}
	\item erweiterter Algorithmus W \textbf{TODO}
\end{itemize}
\section*{Reguläre Ausdrücke}
\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}