\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{bussproofs}
\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}{=}}}
\newcommand{\bred}{\ensuremath{\rightarrow_\beta}}
\newcommand{\ered}{\ensuremath{\rightarrow_\eta}}

\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}
\begin{itemize}
	\item $\beta$-Reduktion
	\begin{equation*}
	(\lambda x.t)s \bred t[s/x]
	\end{equation*}
	\item $\eta$-Reduktion
	\begin{equation*}
	\lambda x.yx \ered y
	\end{equation*}
\end{itemize}
\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{prooftree}
		\AxiomC{}
		\LeftLabel{$(Ax)$}
		\RightLabel{$x:\alpha \in \Gamma$}
		\UnaryInfC{$\Gamma \vdash x:\alpha$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma \vdash t:\alpha\rightarrow \beta$}
		\AxiomC{$\Gamma \vdash s:\alpha$}
		\LeftLabel{$(\rightarrow_e)$}
		\BinaryInfC{$\Gamma \vdash ts:\beta$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma, x:\alpha \vdash t:\beta$}
		\LeftLabel{$(\rightarrow_i)$}
		\UnaryInfC{$\Gamma \vdash \lambda x.t:\alpha\rightarrow\beta$}
	\end{prooftree}
	\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}
	\begin{enumerate}
		\item $\Gamma \vdash x:\alpha \Rightarrow x:\alpha\in\Gamma$
		\item $\Gamma \vdash ts:\beta \Rightarrow \exists\alpha$ mit $\Gamma \vdash t:\alpha\rightarrow\beta$ und $\Gamma\vdash s:\alpha$
		\item $\Gamma \vdash\lambda x.t:\gamma \Rightarrow \gamma = \alpha\rightarrow \beta$ mit $\Gamma, x:\alpha \vdash t:\beta$
	\end{enumerate}
	\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} \defin{4.12}{56}\lem{4.13}{57}
\begin{align*}
X_1 \times X_2 &= \left\lbrace \left(x_1, x_2\right)\vert x_i \in X_i\text{ für } i=1,2\right\rbrace &&\text{(\enquote{struct})}\\
X_1 + X_2 &= \left\lbrace (i,x) \vert i=1,2, x\in X_i\right\rbrace &&\text{(\enquote{union})}\\
1 &= \left\lbrace * \right\rbrace &&\text{\enquote{()} in Haskell}
\end{align*}

Seien $f_i :X_i \rightarrow Y_i$, $g_i: X_i \rightarrow Z$ und $h_i : Z \rightarrow X_i$ mit $i \in \{1,2\}$.
\begin{align*}
f_1 \times f_2 &: X_1 \times X_2 \rightarrow Y_1 \times Y_2, & (f_1\times f_2) (x_1, x_2) &= (f_1(x_1), f_2(x_2))\\
f_1 + f_2 &: X_1 + X_2 \rightarrow Y_1 + Y_2, & (f_1+f_2)(i,x) &= (i, f_i(x))\\
[g_1, g_2] &: X_1 + X_2 \rightarrow Z, & [g_1, g_2])(i,x) &= g_i(x)\\
\langle h_1, h_2\rangle &: Z\rightarrow X_1\times X_2, & \langle h_1, h_2\rangle(z) &= (h_1(z), h_2(z))\\
in_i &: X_i \rightarrow X_1 + X_2, & in_i(x) &= (i,x)\\
\pi_i &: X_1\times X_2 \rightarrow X_i, & \pi_i(x_1,x_2) &= x_i\\
1&: 1\rightarrow 1
\end{align*}

Es gilt
\begin{align*}
[g_1, g_2] \circ in_i &= g_i\\
f_1 + f_2 &= [in_1 \circ f_1, in_2 \circ f_2]\\
[r\circ in_1, r\circ in_2] &= r \text{ für } r: X_1+X_2 \rightarrow Z\\
\pi_i \circ \langle h_1, h_2\rangle &= h_i\\
f_1 \times f_2 &= \langle f_1 \circ\pi_1, f_2\circ\pi_2\rangle\\
\langle\pi_i \circ f, \pi_2\circ f\rangle &= f \text{ für } f: Z\rightarrow X_1\times X_2
\end{align*}
\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}
\begin{itemize}
	\item Definition über \enquote{Destruktoren} etwa $hd$ und $tl$
\end{itemize}
\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: \defin{5.1}{84}
	\begin{prooftree}
		\AxiomC{}
		\LeftLabel{$(Ax)$}
		\RightLabel{$(x:\alpha \in \Gamma)$}
		\UnaryInfC{$\Gamma \vdash x:\alpha$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma \vdash t:\alpha\rightarrow \beta$}
		\AxiomC{$\Gamma \vdash s:\alpha$}
		\LeftLabel{$(\rightarrow_e)$}
		\BinaryInfC{$\Gamma \vdash ts:\beta$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma, x:\alpha \vdash t:\beta$}
		\LeftLabel{$(\rightarrow_i)$}
		\UnaryInfC{$\Gamma \vdash \lambda x.t:\alpha\rightarrow\beta$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma \vdash s:\alpha$}
		\AxiomC{$a\notin FV(\Gamma)$}
		\LeftLabel{$(\forall_i)$}
		\BinaryInfC{$\Gamma \vdash s:\forall a.\alpha$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma \vdash s:\forall a.\alpha$}
		\LeftLabel{$(\forall_e)$}
		\UnaryInfC{$\Gamma \vdash s:(\alpha[\beta/a])$}
	\end{prooftree}
\end{itemize}
\subsection*{Church-Kodierung}\siehe{S. 84}
\begin{itemize}
	\item Natürliche Zahlen
	\begin{align*}
	\mathbb{N}\ &\coloneqq \forall a.(a\rightarrow a) \rightarrow a \rightarrow a\\
	zero\ &: \mathbb{N}\\
	zero\ &= \lambda fx.x\\
	suc\ &: \mathbb{N}\rightarrow\mathbb{N}\\
	suc\ &= \lambda nfx.f(nfx)\\
	fold\ &: \forall a.(a\rightarrow a) \rightarrow a \rightarrow \mathbb{N}\rightarrow a\\
	fold\ &= \lambda fxn.nfx\\
	add &: \mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}\\
	add &= \lambda n.fold\ suc\ n
	\end{align*}
	\item Paare
	\begin{align*}
	(a\times b)\ &\coloneqq \forall r.(a\rightarrow b\rightarrow r)\rightarrow r\\
	pair\ &: \forall ab.a\rightarrow b\rightarrow (a\times b)\\
	pair\ &= \lambda xyf.fxy\\
	fst\ &: \forall ab.(a\times b) \rightarrow a\\
	fst\ &= \lambda p.p (\lambda xy.x)\\
	snd\ &: \forall ab.(a\times b) \rightarrow b\\
	snd\ &= \lambda p.p(\lambda xy.y) 
	\end{align*}
	\item Summen
	\begin{align*}
	(a+b)\ &\coloneqq \forall r.(a\rightarrow r) \rightarrow (b \rightarrow r)\rightarrow r\\
	inl\ &: \forall ab.a\rightarrow(a+b)\\
	inl\ &= \lambda xfg.fx\\
	inr\ &: \forall ab.b\rightarrow(a+b)\\
	inr\ &= \lambda yfg.gy\\
	case\ &: \forall abs.(a\rightarrow s)\rightarrow (b\rightarrow s) \rightarrow (a+b) \rightarrow s\\
	case\ &= \lambda fgs.sfg
	\end{align*}
	\item Listen
	\begin{align*}
	List\ a\ &\coloneqq \forall r.r\rightarrow (a\rightarrow r\rightarrow r)\rightarrow r\\
	Nil\ &: \forall a.Lista\ a\\
	Nil\ &= \lambda uf.u\\
	Cons\ &: \forall a.a\rightarrow List\ a\rightarrow List\ a\\
	Cons\ &= \lambda xluf.fx(luf)\\
	len\ &: \forall a.List\ a\rightarrow \mathbb{N}\\
	len\ &= \lambda l.l\ zero\ (\lambda xr.suc\ r)
	\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 \siehe{S. 88}
	\begin{prooftree}
		\AxiomC{}
		\LeftLabel{$(\forall_e)$}
		\RightLabel{$(x:\forall a_1,\ldots, \forall a_k .\alpha) \in \Gamma$}
		\UnaryInfC{$\Gamma \vdash x:\alpha[\beta_1/a_1,\ldots, \beta_k/a_k]$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma, x:\alpha \vdash t:\beta$}
		\LeftLabel{$(\rightarrow_i)$}
		\UnaryInfC{$\Gamma \vdash \lambda x.t:\alpha\rightarrow\beta$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma \vdash t:\alpha\rightarrow \beta$}
		\AxiomC{$\Gamma \vdash s:\alpha$}
		\LeftLabel{$(\rightarrow_e)$}
		\BinaryInfC{$\Gamma \vdash ts:\beta$}
	\end{prooftree}
	\begin{prooftree}
		\AxiomC{$\Gamma \vdash t:\alpha$}
		\AxiomC{$\Gamma, x:Cl(\Gamma, \alpha)\vdash s:\beta$}
		\LeftLabel{(let)}
		\BinaryInfC{$\Gamma \vdash$ let $x = t$ in $s:\beta$}
	\end{prooftree}
	\item Inversionslemma \siehe{S. 89}
	\begin{enumerate}
		\item Wenn $\Gamma \vdash x:\alpha$, dann existieren Typen $\beta_i$ und ein Typschema $S = \forall a_1 \ldots \forall a_k.\gamma$, so dass $(x:S)\in \Gamma$ und $\alpha = \gamma[\beta_1/a_1,\ldots,\beta_k/a_k]$
		\item Wenn $\Gamma \vdash ($ let $x = s$ in $t) : \alpha$, dann existiert ein Typ $\beta$ nut $\Gamma \vdash s:\beta$ und $\Gamma, x:Cl(\Gamma, \beta) \vdash t:\alpha$
	\end{enumerate}
	\item erweiterter Algorithmus W  mit Menge $PT$ von Typgleichungen
	\begin{align*}
	PT(\Gamma;x;\alpha) &= \lbrace a\pteq \gamma [a_1'/a_1,\ldots,a_k'/a_k] \vert (x: \forall a_1,\ldots,\forall a_k .\gamma) \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}\\
	PT(\Gamma;(\text{let } x=s\text{ in }t);\alpha) &= PT(\Gamma\sigma, x:Cl(\Gamma\sigma, \sigma(b));t;\alpha\sigma)
	\end{align*}
	wobei $\sigma = mgu(PT(\Gamma;s;b))$ mit $b$ frisch
\end{itemize}
\section*{Minimierung von deterministischen endlichen Automaten}
\begin{enumerate}
	\item Entferne aus $Q$ alle nicht erreichbaren Zustände
	\item Initialisiere $R$ auf $\lbrace (q_1, q_2)\ \vert\ q_1 \in F \Leftrightarrow q_2 \in F\rbrace$
	\item Suche ein Paar $(q_1,q_2) \in R$ und einen Buchstaben $a \in \Sigma$ mit
	\begin{equation*}
	(\delta(a,q_1),\delta(a,q_2)) \notin R
	\end{equation*}
	Wenn kein solches Paar gefunden wird, gehe zu Schritt 4. Andernfalls entferne $(q_1,q_2)$ aus $R$ und fahre bei 3. fort.
	\item Identifiziere alle Zustandspaare in $R$.
\end{enumerate}
\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}