mirror of
https://gitlab.cs.fau.de/ik15ydit/latexandmore.git
synced 2024-11-22 11:49:32 +01:00
ThProg Umlaute und kleine Aenderungen
SystemF hinzugefuegt
This commit is contained in:
parent
5cd2c564a2
commit
de8e51af04
@ -4,7 +4,6 @@
|
||||
\DeclareMathSizes{10}{10}{10}{10}
|
||||
\setlength{\parindent}{0pt}
|
||||
\title{Ko-Rekursion/-Induktion}
|
||||
\author{Yannik Schmidt (Sheppy)\\September 2015}
|
||||
\date{ }
|
||||
\begin{document}
|
||||
\maketitle
|
||||
@ -63,7 +62,11 @@
|
||||
\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}\}\]
|
||||
\[
|
||||
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:
|
||||
|
@ -21,14 +21,14 @@
|
||||
\[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{Ansatz:}\\
|
||||
- zweite Formel linke Seite ist syntaktisch echt groesser als die Rechte\\
|
||||
- erste Formel P$\uparrow$ ist auf beiden Seiten gleich also beliebig \\
|
||||
\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:}\\
|
||||
\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}
|
||||
@ -40,10 +40,10 @@
|
||||
\end{fleqn} \\
|
||||
\textbf{und damit die Polynome:}\\
|
||||
\[P\downarrow = x_1+x_2 \;\;\; und \;\;\; P\uparrow = 3x_1+x_2 \] \\
|
||||
\section{Domaenen und Grenzfaelle}
|
||||
Unsere Polynome gelten fuer kleine Werte nicht, um genauzusein, nur fuer die 0 nicht, daher geben wir als Domaene an:
|
||||
\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 Funktionsdomaene:\\
|
||||
und Funktionsdom\"ane:\\
|
||||
\[\mathcal{A} = \{P(*),P(*)\}\]
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user