Files fixed

Public/thprog/Koinduktion_reduktion.tex

@@ -0,0 +1,111 @@
+	\documentclass{article}
+	\usepackage{amsmath}
+	\usepackage{nccmath}
+	\DeclareMathSizes{10}{10}{10}{10}
+	\setlength{\parindent}{0pt}
+	\title{Ko-Rekursion/-Induktion}
+	\date{ }
+	\begin{document}
+	\maketitle
+	\section{Korekursion}
+	\textbf{Gegeben:}
+		\begin{fleqn}
+				\begin{align*}
+					co&data Signal\:where  \\
+					& \enspace currentSample : Signal \rightarrow Int \\
+					& \enspace discardSample : Signal \rightarrow Signal
+				\end{align*}
+		\end{fleqn}
+	\textbf{sowie:}
+	\begin{fleqn}
+	\begin{align*}
+		&currentSample(flat\:x) = x			&
+		&discardSample(flat\:x) = flat\:x	\\
+		&currentSample(square\:x\:y)		&
+		&discardSample(square\:x\:y)		
+	\end{align*}	
+	\end{fleqn}
+	\textbf{Es soll gelten:}\\
+	sampler t s\enspace = s , wenn $t>0$ und 0 sonst\\
+	sowie insbesondere:
+	\begin{fleqn}
+	\begin{align*}
+		&sampler:\:Signal\rightarrow Signal\rightarrow Signal \\
+		&sampler(square\:0\:1)(square\:x\:0) = flat\:0 \\
+		&sampler(square\:1\:0)(flat\:x) = square\:x\:0  \\
+	\end{align*}	
+	\end{fleqn}
+	\textbf{Schritt 1:}\\
+	$\rightarrow$ sampler Funktion in codata-Funktionen einsetzen
+	\begin{fleqn}
+	\begin{align*}
+		&currentSample(sampler\:t\:s)\\
+		&discardSample(sampler\:t\:s)	
+	\end{align*}	
+	\end{fleqn}
+	\textbf{Schritt 2:}\\
+	$\rightarrow$ Bedingung von oben bei erster Funktion anwenden also:
+	\begin{fleqn}
+		\begin{align*}
+			currentSample(sampler\:t\:s) = \:&if\:(currentSample\:\:t>0)\\
+											&then\:(currentSample\:\:s)\\
+											&else\:(flat\:\:0)
+		\end{align*}
+	\end{fleqn}
+	\textbf{sowie zweite Formel zum Aufteilen verwenden:}
+		\begin{fleqn}
+		\begin{align*}
+			discardSample(sampler\:t\:s) = sampler(discardSample\:\:t)(discardSample\:\:s)
+		\end{align*}
+	\end{fleqn}
+	\newpage
+	\section{Ko-Induktion:}
+	\textbf{Induktionsanfang:}\\
+	$\rightarrow$ anhand erster Formel 'R' aufstellen
+	\[ 
+		R = \{ 
+			\underbrace{
+				sampler(square\:0\:1)(square\:x\:0)}_{linke\:Seite},\underbrace{flat\:0}_{rechte\:Seite} \:|\: \underbrace{x\in Int}_{von\:oben}\}
+		\]
+	$\rightarrow$ "R ist Bisimulation" hinschreiben, linke Seite aufloesen\\
+	\[ sampler(square\:0\:1)(square\:x\:0) = 0 \]
+	$\rightarrow$ wenn hier am Endde kein Term rauskommt, dann koennen wir einfach die \textbf{rechte Seite bei der normalen Funktion} einsetzen und selbige aufloesen:
+	\[ currentSample(flat\;0) = 0 \]
+	$\rightarrow$ sehr gut, die rechten Seiten sind gleich wir sind hier also fertig\\ \\
+	\textbf{zweite Bedingung:}
+		\[discardSample(sampler(square\:1\:0)(square\:0\:x)) = sampler(square\:1\:0)(square\:0\:x)\]
+	\textit{das ist doof denn:}
+		\[discardSample(flat 0) = 0\]
+	\textbf{Schritt 3:}\\
+	\[R' = R \;\cup\;\{\underbrace{sampler(square\:1\:0)(square\:0\:x)}_{aufgeloeste\;2.\;Bedingung},flat\;0\:|\:x\in Int\}\]	
+	wir muessen jetzt zeigen:
+	\[
+		currentSample(\underbrace{sampler(square\:1\:0)(square\:0\:x)}_{hier\;=\;0}) = \underbrace{currentSample(flat\;0)}_{hier\;=\;0}
+	\]
+	passt also, jetzt wie oben auch zweite Funktion:
+	\[
+		discardSample(sampler(square\:1\:0)(square\:0\:x)) = \underbrace{sampler(square\:1\:0)(square\:0\:x)}_{wieder\;linke\;Seite\;in\;R'}\]\[
+		discardSample(flat\;0) = \underbrace{flat\;0}_{wieder\;rechte\;Seite}
+	\]
+	und fertig!\\\\
+	\begin{tiny}
+	\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
+	\end{tiny}
+	\newpage
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+\end{document}

Public/thprog/Polynomordnung.tex

@@ -0,0 +1,71 @@
+	\documentclass{article}
+	\usepackage{amsmath}
+	\usepackage{nccmath}
+	\usepackage{ulem}
+	\DeclareMathSizes{10}{10}{10}{10}
+	\setlength{\parindent}{0pt}
+	\title{Ko-Rekursion/-Induktion}
+	\date{Oktober 2015}
+	\begin{document}
+	\maketitle
+	\section{In Funktionsschreibweise bringen}
+	Infixnotation:
+	\[x \uparrow ( y \uparrow z) \rightarrow_{0}\; x \uparrow (y \downarrow y)\]\\
+	Funktionsschreibweise:
+	\[ P_{\uparrow}(x,P_{\uparrow}(y,z)) \rightarrow_{0} \; P_{\uparrow}(x,P_{\downarrow}(y,y))\]
+	\section{Kontext ggf. kuerzen}
+	\[ P_{\uparrow}(x,P_{\uparrow}(y,z)) \rightarrow_{0} \; P_{\uparrow}(x,P_{\downarrow}(y,y))\]
+	\[\xout{P(x},P_{\uparrow}(y,z)) \rightarrow_{0} \; \xout{P(x},P_{\downarrow}(y,y)))\]
+	\[P_{\uparrow}(y,z) \rightarrow_{0} \;P_{\downarrow}(y,y)\]
+	\section{Polynom finden}
+	\[P_{\uparrow}(y,z) \rightarrow_{0} \;P_{\downarrow}(y,y)\]
+	Ein "+" zwischen die Parameter setzen und Multiplikator vor beide sodass gilt:
+	\[P_{\uparrow}(y,z) > \;P_{\downarrow}(y,y)\;\;\textbf{\underline{bzw:}}\;\;ay+bx>cy+dy\]
+	\textbf{Hinweise:}\\
+	- linke Seite ist syntaktisch echt gr\"osser als die Rechte ist aussreichendes Kriterium also z.B.:
+	\[ P_{\downarrow}( P_{\downarrow}(x,y) ) > P_{\downarrow}(x,y) \]
+	- niemals Minuswerte \\
+	- niemals '0' als Multiplikator\\\\
+	\textbf{hier:}
+		\[ay+bx>cy+dy\]
+	\textbf{Wir nehmen an dass wir 'y' hoch genug setzen damit bx irrelevant wird:}\\
+		\[ay>cy+dy = a>c+d \]
+	\\ \textbf{das ist nun trivial, wir raten:}
+	\begin{fleqn}
+		\begin{align*}
+			&c = 1 \\
+			&d = 1 \\
+			&a = c+d+1 = 3
+		\end{align*}
+	\end{fleqn} \\
+	\textbf{und damit die Polynome:}\\
+	\[P\downarrow = x_1+x_2 \;\;\; und \;\;\; P\uparrow = 3x_1+x_2 \] \\
+	\section{Dom\"anen und Grenzf\"alle}
+	Unsere Polynome gelten potentiell f\"ur kleine Werte nicht, hier, nur f\"ur die 0 nicht, daher geben wir als Dom\"ane an:
+	\[ A = N\setminus\{0\} \]
+und Funktionsdom\"ane:\\
+	\[\mathcal{A} = \{P(*),P(*)\}\]
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	
+	\end{document}

Public/thprog/Strukturelle_Induktion.tex

@@ -0,0 +1,51 @@
+	\documentclass{article}
+	\usepackage{amsmath}
+	\usepackage{nccmath}
+	\DeclareMathSizes{10}{10}{10}{10}
+	\setlength{\parindent}{0pt}
+	\title{Struckturelle Induktion}
+	\date{ }
+	\begin{document}
+	\maketitle
+	%----------------------------------%
+	\textbf{Referenzaufgabe:} \\
+		\\
+		\textbf{data List} a = $Nil$ $|$ $Cons$ a \textbf{List} a
+		\begin{align*}
+			snoc\;Nil\;a 			&= Cons\;a\;Nil\\
+			snoc(Cons\;x\;xs)\;a	&= Cons\;x\;(snoc\;xs\;a)
+		\end{align*}
+		\begin{align*}
+			Nil + ys 			&= ys\\
+			(Cons\;x\;xs) + ys 	&= Cons\;x\;(xs + ys)
+		\end{align*}
+		\underline{Beweisen sie dass:}\\
+		$\forall e,\;xs,\;ys\\xs+(Cons\;e\;ys) = (snoc\;xs\;e)+ys$ \\\\
+	%----------------------------------%
+	\textbf{Induktionsanfang (IA):}\\\\
+		$xs = Nil$\;\;$\Rightarrow$ Einsetzen und beide Seiten maximal vereinfachen
+	\begin{align*}
+		Nil+(Cons\;e\;ys) 	&= (snoc\;Nil\;e)+ys\\
+			 Cons\;e\;ys	&= (snoc\;Nil\;e)+ys\\
+			 Cons\;e\;ys	&= (Cons e Nil) + ys\\
+			 Cons\;e\;ys	&= Cons\;e (Nil + ys)\\
+			 Cons\;e\;ys	&= Cons\;e\;ys
+	\end{align*}
+	\textbf{Induktionshypothese/-voraussetzeung (IH/IV):}\\\\
+	- $xs$ durch allgemeines as ersetzen
+	\[as+(Cons\;e\;ys) = (snoc\;as\;e)+ys\]
+\newpage
+	\textbf{Induktionsschritt (IS):}\\\\
+	$as\;=\;Cons\;a\;as$\\$\Rightarrow$ Einsetzen und wieder beide Seiten maximal vereinfachen,auf einer Seite die Induktionshypothese reinfrikeln (idR. nur auf einer Seite,z.B. auf der linken)
+	\begin{align*}
+		Cons\;a\;as\;+(Cons\;e\;ys)\;&=\;snoc\;((Cons\;a\;as)\;e)+ys \\
+		Cons\;a\;(\underbrace{as\;+(Cons\;e\;ys)}_{IH\;links})\;&=\;snoc\;((Cons\;a\;as)\;e)+ys\\
+		Cons\;a\;(\underbrace{(snoc\;as\;e)\;+\;ys)}_{IH\;rechts})\;&=\;snoc\;((Cons\;a\;as)\;e)+ys\\
+		Cons\;a\;((snoc\;as\;e)\;+\;ys))\;&=\;Cons\;a\;((\;snoc\;as\;e)\;+\;ys))
+	\end{align*}\\
+\textbf{Q.E.D. und fertig!}\\
+\\\\
+	\begin{tiny}
+	\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
+	\end{tiny}
+\end{document}

Public/thprog/SystemF.tex

@@ -0,0 +1,59 @@
+	\documentclass{article}
+	\usepackage{amsmath}
+	\usepackage{nccmath}
+	\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*}
+				
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+		
+	\begin{tiny}
+	\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
+	\end{tiny}
+\end{document}