diff --git a/Public/thprog/Koinduktion_reduktion.tex b/Public/thprog/Koinduktion_reduktion.tex new file mode 100644 index 0000000..e565e40 --- /dev/null +++ b/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*} + ¤tSample(flat\:x) = x & + &discardSample(flat\:x) = flat\:x \\ + ¤tSample(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*} + ¤tSample(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} \ No newline at end of file diff --git a/Public/thprog/Polynomordnung.tex b/Public/thprog/Polynomordnung.tex new file mode 100644 index 0000000..de82172 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/Public/thprog/Strukturelle_Induktion.tex b/Public/thprog/Strukturelle_Induktion.tex new file mode 100644 index 0000000..0ba1a4b --- /dev/null +++ b/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} \ No newline at end of file diff --git a/Public/thprog/SystemF.tex b/Public/thprog/SystemF.tex new file mode 100644 index 0000000..85c5a24 --- /dev/null +++ b/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} \ No newline at end of file