Typregeln, Church-Kodierung, erweiterter Alg. W

2018-10-05 13:57:17 +02:00
parent 2f8cdc41dc
commit 66a7da8f45
2 changed files with 143 additions and 18 deletions
--- a/merkzettel.pdf
+++ b/merkzettel.pdf
--- a/merkzettel.tex
+++ b/merkzettel.tex
@@ -11,7 +11,7 @@
 \usepackage{tikz-qtree}
 \usepackage{mathtools}
 \usepackage{latexsym}
-\usepackage{algorithmicx}
+\usepackage{bussproofs}
 \usepackage{csquotes}
 \usepackage{pdfpages}
 \usepackage{pgfplots}
@@ -34,6 +34,8 @@
 \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]
@@ -52,7 +54,16 @@

 \section*{$\lambda$-Kalkül}
 \subsection*{Ungetypt}
-\subsubsection*{Rekursion}
+\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}
@@ -77,16 +88,35 @@
 	\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}
+	\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} \textbf{TODO}
+	\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
@@ -143,28 +173,79 @@
 	\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*}
+	\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*}
-	\textbf{Todo}
+	\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*}
-	Inhalt...
+	(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*}
-	Inhalt...
+	(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*}
-	Inhalt...
+	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}
@@ -187,11 +268,55 @@
 		\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}
+	\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*{Reguläre Ausdrücke}
+\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)}\\