From a2612bbd133c60eec93ac4e74714aef4569ab5fa Mon Sep 17 00:00:00 2001 From: Sheppy Date: Wed, 7 Oct 2015 16:30:14 +0200 Subject: [PATCH] Filenames changed --- Public/thprog/Koinduktio_reduktion.tex | 111 ------------------ Public/thprog/Strukturelle Induktion.tex | 51 -------- .../SystemF_und_Reduktionsreihenfolge.tex | 59 ---------- Public/thprog/ThProg_Polynomordnung.tex | 71 ----------- 4 files changed, 292 deletions(-) delete mode 100644 Public/thprog/Koinduktio_reduktion.tex delete mode 100644 Public/thprog/Strukturelle Induktion.tex delete mode 100644 Public/thprog/SystemF_und_Reduktionsreihenfolge.tex delete mode 100644 Public/thprog/ThProg_Polynomordnung.tex diff --git a/Public/thprog/Koinduktio_reduktion.tex b/Public/thprog/Koinduktio_reduktion.tex deleted file mode 100644 index e565e40..0000000 --- a/Public/thprog/Koinduktio_reduktion.tex +++ /dev/null @@ -1,111 +0,0 @@ - \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/Strukturelle Induktion.tex b/Public/thprog/Strukturelle Induktion.tex deleted file mode 100644 index 0ba1a4b..0000000 --- a/Public/thprog/Strukturelle Induktion.tex +++ /dev/null @@ -1,51 +0,0 @@ - \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_und_Reduktionsreihenfolge.tex b/Public/thprog/SystemF_und_Reduktionsreihenfolge.tex deleted file mode 100644 index 85c5a24..0000000 --- a/Public/thprog/SystemF_und_Reduktionsreihenfolge.tex +++ /dev/null @@ -1,59 +0,0 @@ - \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 diff --git a/Public/thprog/ThProg_Polynomordnung.tex b/Public/thprog/ThProg_Polynomordnung.tex deleted file mode 100644 index de82172..0000000 --- a/Public/thprog/ThProg_Polynomordnung.tex +++ /dev/null @@ -1,71 +0,0 @@ - \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