mirror of
https://gitlab.cs.fau.de/ik15ydit/latexandmore.git
synced 2024-11-22 11:49:32 +01:00
Filenames changed
This commit is contained in:
Sheppy
parent
2f0ac44482
commit
a2612bbd13
@ -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}
|
||||
@ -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}
|
||||
@ -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}
|
||||
@ -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}
|
||||
Loading…
Reference in New Issue
Block a user