Mirror/latexandmore
1
0
Fork 0
mirror of https://gitlab.cs.fau.de/ik15ydit/latexandmore.git synced 2024-11-22 03:49:31 +01:00
Code Issues Projects Releases Wiki Activity

small fixes

Browse Source
This commit is contained in:
Sheppy 2015-10-08 12:07:30 +02:00
parent 51fd2bba20
commit 1ecbe50259
3 changed files with 12 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Vorlesungen/ThProg/Konfluenz.tex
View File

@ -9,7 +9,8 @@
\section*{Wichtige Lemmas} \section*{Wichtige Lemmas}
\subsection*{Newman's Lemma:} \subsection*{Newman's Lemma:}
Ein stark normalisierendes und lokal Konfluentes Termersetzungssystem (TES) ist konfluent. Ein stark normalisierendes und lokal Konfluentes Termersetzungssystem (TES) ist konfluent.
\subsection*{} \subsection*{Critical Pair Lemma:}
Ein TES ist lokal konfluent, wenn alle kritischen Paare zusammenf\"uhrbar sind.
\section{Matching Table:} \section{Matching Table:}
Formeln: Formeln:
\begin{align} \begin{align}

2
Vorlesungen/ThProg/Strukturelle_Induktion.tex
View File

@ -37,7 +37,7 @@
\[as+(Cons\;e\;ys) = (snoc\;as\;e)+ys\] \[as+(Cons\;e\;ys) = (snoc\;as\;e)+ys\]
\newpage \newpage
\textbf{Induktionsschritt (IS):}\\\\ \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) $xs\;=\;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*} \begin{align*}
Cons\;a\;as\;+(Cons\;e\;ys)\;&=\;snoc\;((Cons\;a\;as)\;e)+ys \\ 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{as\;+(Cons\;e\;ys)}_{IH\;links})\;&=\;snoc\;((Cons\;a\;as)\;e)+ys\\

29
Vorlesungen/ThProg/SystemF.tex
View File

@ -86,9 +86,9 @@
$(5)\; $(5)\;
\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash \Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash
\overbrace{ \overbrace{
n\,:\,(\,a\,\rightarrow\,a\,)\rightarrow (\,a\,\rightarrow \,a\,) n\,:\,\forall a\,.',(\,a\,\rightarrow\,a\,)\rightarrow (\,a\,\rightarrow \,a\,)
}^{per\;Definition\; =\;\mathrm{N}} }^{per\;Definition\; =\;\mathrm{N}}
\hspace{1cm} \hspace{8mm}
\overbrace{ \overbrace{
mult:\;\mathrm{N}\rightarrow \mathrm{N}\rightarrow \mathrm{N} mult:\;\mathrm{N}\rightarrow \mathrm{N}\rightarrow \mathrm{N}
}^{Ax} }^{Ax}
@ -104,7 +104,7 @@
\Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash \Gamma \;\cup \{\,n:\mathrm{N}\,\} \vdash
n\,:\,(\,\mathrm{N}\rightarrow \mathrm{N}\,) n\,:\,(\,\mathrm{N}\rightarrow \mathrm{N}\,)
\rightarrow (\,\mathrm{N}\rightarrow \mathrm{N}\,) \rightarrow (\,\mathrm{N}\rightarrow \mathrm{N}\,)
\hspace{2cm} \hspace{25mm}
mult\;two\;\mathrm{N}\rightarrow \mathrm{N} mult\;two\;\mathrm{N}\rightarrow \mathrm{N}
$ $
}\\ }\\
@ -136,22 +136,11 @@
$ $
\\ \\
\textbf{Erkl\"arungen:}\\ \textbf{Erkl\"arungen:}\\
\begin{small} (1) $\rightarrow_{i}$\\
- (1) $\rightarrow_{i}$\\ (2)(3) $\rightarrow_e$\\
- (2)(3) $\rightarrow_e$\\ (3)(rechts)$[\,one:\mathrm{N}\,]$ mit Ax fertig\\
- in (3) ist $[\,one:\mathrm{N}\,]$ mit Ax fertig\\ (4) $\forall _e$ (wir wissen, dass N : $(a->a)->a->a$ ist, und dass \{n : N ist\}; damit n hinten also mit dem Kontex aufgeht muss es von der Form $(a->a)->a->a$ sein)\\
- in (4) $\forall _e$\\ (4)(links) $\forall_{e}$ (rechts) $\rightarrow_e$\\\\
- (4)(links) $\forall_{e}$ (rechts) $\rightarrow_e$\\
\end{small}
\\
\textbf{Eine \"Ubersicht der Regeln findet sich in den \"Ubungsfolien oder dem SS14 Spickzettel!} \textbf{Eine \"Ubersicht der Regeln findet sich in den \"Ubungsfolien oder dem SS14 Spickzettel!}
$ $\\\\
\begin{tiny}
\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
\end{tiny}
\end{document} \end{document}