latexandmore/ThProg/SystemF.tex

	\documentclass{article}	
	\usepackage{amsmath}
	\usepackage{nccmath}
	%\usepackage{bussproofs}
	%dieses Paket koennte man fuer die typherleitung verwenden wenn man wollte
	\DeclareMathSizes{10}{10}{10}{10}
	\setlength{\parindent}{0pt}
	\title{System F und Reduktionsreihenfolge}
	\date{ }
	\begin{document}
	\section{Generelles}
		\subsection{Normale-/Lazy-Reduktion}
			- pre-order durch Baum ("von unten nach oben auswerten")	\\
			- leftmost-outermost\\
			- Argumente zum Schluss auswerten
			\begin{align*}			
				pow(a,pow(c,b))\:\:	& mit\;linkem\;pow\;anfangen\\
									& dann\;a\\
									& dann\;rechtes\;pow\\
									& dann\;c\\
									& dann\;d
			\end{align*}
		\subsection{Applikative Reduktion:}
			- post-order durch Baum ("von oben nach unten")\\
			- leftmost-innermost\\
			- als erstes die Argumente auswerten
			\begin{align*}
				pow(a,pow(c,b))\:\: & mit\;c\;anfangen
				\enspace\;\;\;\;\;\;\;\;\;\enspace\;\;\;\;
											\\
									& dann\;b\\
									& dann\;a\\
									& dann\;rechtes\;pow\\
									& dann\;linkes\;pow
			\end{align*}
		\subsection{How to work with Lambda}
			- Buchstabe hinter $\lambda $ wegnehmen\\
			- Term von der respektiven Stelle hinten entfernen\\
			- alle Vorkommen des Buchstabens mit dem Term ersetzen\\
			- idealerweise bei mehreren $\lambda$ in einem Term \textbf{immer} verschiedene Buchstaben verwenden\\
			- wenn nicht genug Terme zum Aufl\"osen von $\lambda$ vorhanden sind, nicht damit anfangen, also z.B. bei $pred\;\lambda\,f\,a\,.\,fa\;one$ nicht one f\"ur f einsetzen sondern $pred$ aufl\"osen
	\section{SS15Probeklausur Beispielaufgabe}
	\subsection*{1) Reduktion}
	\subsubsection*{a) Normal/Lazy}
		\begin{align*}
			 pow2\;three\;	&=\;	three\;(mult\;two)\;one\\
			 				&=\;	\lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,)(\,mult\;two)\;one\\
			 				&=\;	\lambda a\, .\, (mult\;two)\,((mult\;two)\,((mult\;two)\;a\,)\;one\\
			 				&=\;	(mult\;two)\,((mult\;two)\,((mult\;two)\;one\,)
		\end{align*}
	\subsubsection*{b) Aplikativer Reihenfolge}
		\begin{align*}
			pow2\;three\;	&=\;	pow2\; (\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)\\
							&=\;	(\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)(mult\;two)\;one\\
							&=\;	(\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)(mult\;\lambda g\,b\, .\,g\,(\,g\;b\,))\;one\\
							&=\;	(\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)(mult\;\lambda g\,b\, .\,g\,(\,g\;b\,))\;(\lambda h\,c\, .\,h\;c)
		\end{align*}
	kleine Anmerkung hierzu noch:
	\[
		\underbrace{(\, \lambda f\,a\, .\,f\,(\,f\,(\,f\;a\,) \,)}_{oberste\;Funktion}
		\underbrace{(mult\;\lambda g\,b\, .\,g\,(\,g\;b\,))}_{erstes\;Argument}
		\;
		\underbrace{(\lambda h\,c\, .\,h\;c)}_{zweites\;argument}
	\]
	d.h. wir w\"urden hier beim ersten Argument weitermachen und "mult" aufl\"osen
	(beim zweiten g\"abe es gerade auch gar nichts mehr zu machen)

	\subsection*{2) Typherleitung}	
		\textbf{Typherleitung f\"ur:}
		\[
			\{
			\,mult\;:\;
			\mathrm{N}\rightarrow\mathrm{N}\rightarrow\mathrm{N},\;
			one\; : \; \mathrm{N},\,two\;\mathrm{N}\,
			\vdash \; \lambda n.\,n\,(\, mult \; two\,)\;one\,:\mathrm{N}\rightarrow
			\mathrm{N}
			\}
		\]
		\textbf{mit Sonderhinweis, dass die Chruch-Numerale in System F den folgenden Typ besitzen:}
		\[
			\mathrm{N}\; := \; \forall a.(a\,\rightarrow \, a)\, \rightarrow \, a \, \rightarrow \,a		
		\]
	\textbf{Herleitung:}\\
		
	%Zeile 5
	\underline{
		$(5)\;
			\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash
			\overbrace{
			n\,:\,\forall a\,.\,(\,a\,\rightarrow\,a\,)\rightarrow (\,a\,\rightarrow \,a\,)
			}^{per\;Definition\; =\;\mathrm{N}}
			\hspace{8mm}
			\overbrace{
			mult:\;\mathrm{N}\rightarrow \mathrm{N}\rightarrow \mathrm{N}
			}^{Ax}
			\hspace{5mm}
			\overbrace{
			two:\;\mathrm{N}
			}^{Ax}
		$
	}\\
	%Zeile 4
	\underline{
		$(4)\;
			\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash 
			n\,:\,(\,\mathrm{N}\rightarrow \mathrm{N}\,)
			\rightarrow (\,\mathrm{N}\rightarrow \mathrm{N}\,)
			\hspace{25mm}
			mult\;two\;\mathrm{N}\rightarrow \mathrm{N}
		$
	}\\
	%Zeile 3
	\underline{
	$	(3)\;
		\Gamma \; \cup \{\,n:\mathrm{N}\,\}\,
		\vdash \, n\,(\,mult\;two\,)\,: \mathrm{N}\rightarrow\,\mathrm{N}
		\hspace{6cm}
		\;one\; : \mathrm{N} 
	$
	}\\
	%Zeile 2
	\underline{
	$(2)\;
		\Gamma \; \cup \{\,n:\mathrm{N}\,\}\,
		\vdash \, n\,(\,mult\;two\,)\;one\; : \mathrm{N}
	$\hspace{48mm}}
	\\
	%Zeile 1	
	$	(1)\;
	\{ 
		\underbrace{
			\,mult\;:\;
			\mathrm{N}\rightarrow\mathrm{N}\rightarrow\mathrm{N},\;
			one\; : \; \mathrm{N},\,two\;\mathrm{N}\,
		}_{:=\Gamma}	
	\vdash \; \lambda n.\,n\,(\, mult \; two\,)\;one\,:\mathrm{N}\rightarrow\mathrm{N}
	$		
	\\
	\textbf{Erkl\"arungen:}\\
	(1) $\rightarrow_{i}$\\
	(2)(3) $\rightarrow_e$\\
	(3)(rechts)$[\,one:\mathrm{N}\,]$ mit Ax fertig\\
	(4) $\forall _e$ (wir wissen, dass N : $(a->a)->a->a$ ist, und dass \{n : N ist\}; damit n hinten also mit dem Kontex aufgeht muss es von der Form $(a->a)->a->a$ sein)\\
	(4)(links) $\forall_{e}$ (rechts) $\rightarrow_e$\\\\
	\textbf{Eine \"Ubersicht der Regeln findet sich in den \"Ubungsfolien oder dem SS14 Spickzettel!}
	
\end{document}