latexandmore/Vorlesungen/ThProg/Konfluenz.tex

	\documentclass{article}
	\usepackage{amsmath}
	\usepackage{nccmath}
	\DeclareMathSizes{10}{10}{10}{10}
	\newcommand{\xhspace}[0]{\noindent\hspace*{5mm}}
	\setlength{\parindent}{0pt}
	\title{Konfluenz}
	\date{ }
	\begin{document}
	\section*{Wichtige Lemmas}
		\subsection*{Newman's Lemma:}
			Ein stark normalisierendes und lokal Konfluentes Termersetzungssystem (TES) ist konfluent.
		\subsection*{Critical Pair Lemma:}
			Ein TES ist lokal konfluent, wenn alle kritischen Paare zusammenf\"uhrbar sind.
			
		\section*{Allgemeines Vorgehen:}
		Alle Regeln m\"ussen gegen alle anderen gematched werden um lokale Konfluenz zu 
		zeigen, f\"ur das Gegenteil reicht also logischerweise \textbf{ein} nicht- 
		zusammenf\"urbares Paar.\\\\
		
		\textbf{F\"ur Regelpaar (x)(y):}\\
		$\rightarrow$ $l_1$ = linke Seite von x\\
		$\rightarrow$ $l_2$ = linke Seite von y (falls gleiche Variablennamen selbige umbennen)\\
		$\rightarrow$ $l_1$ so substituieren, dass Regel y angewendet werden kann (aka MGU finden)\\
		$\rightarrow$ $l_1$ sollte der MGU = $l_2$ sein $\rightarrow$ triviales Paar\\
		$\rightarrow$ beide Regeln 1x anwenden und sehen ob man die entstehenden Terme wieder zusammen bringen kann 
		\textit{(durch Anwendung beliebiger Regeln des TES)}\\\\
		
		Triviale Paare muessen nicht gezeigt werden. Ein Paar kann bereits nach Anwendung beider Regeln wieder gleich sein
		(z.B. $\neg\neg\neg x$ ). So ein Paar ist automatisch zusammenf\"uhrbar, aber dennoch der Definition nach
		\textbf{\underline{kein}} triviales Paar.
		\section*{Beispiel Lokale Konfluenz zeigen:}
			Formeln:
			\begin{align}
				x \Uparrow ( y \Uparrow z) & \rightarrow_{0}
					\; x \Uparrow (y \Downarrow y)
				\\				
				x \Downarrow ( x \Downarrow y ) & \rightarrow_0
					\; x \Downarrow y
			\end{align}
			
		\textbf{(1)(1)}
			\begin{align*}
				l_1 &= x \Uparrow ( y \Uparrow z)  \\
				l_2 &= u \Uparrow ( v \Uparrow w)  \\
			\end{align*}
		\textbf{damit:}
			\[
				mgu = [\;y \mapsto u\,,\;z \mapsto (\,u;\Uparrow\;w\,)\;]
			\]
		\textbf{und die mit dem MGU substituierte Seite $l_1$:}
			\begin{align*}
				l_1\sigma = x \Uparrow (\,u\;&\Uparrow\,(\,v\Uparrow\;w\,))\\ \\
				l_1\sigma (1.1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,)
				\hspace{1cm}&\hspace{8mm}
				l_1\sigma (1.2) = x\;\Uparrow \, ( \, u \; \Uparrow \,(v\;\;\Downarrow\;v\,) \\\\
				
			\end{align*}
		Newman's Lemma bedeutet in der Umkehrung, dass ein System bei dem mindestens ein Paar nicht zusammenf\"uhrbar ist, nicht konfluent ist.\\
		D.h. wir sind hier bereits fertig.
		
		
		
		
		
		
		
		
		
	
		
		
		
	\begin{tiny}
	\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
	\end{tiny}
\end{document}