mirror of
https://gitlab.cs.fau.de/ik15ydit/latexandmore.git
synced 2024-11-22 11:49:32 +01:00
79 lines
2.8 KiB
TeX
79 lines
2.8 KiB
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) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,)
|
|
\hspace{1cm}&\hspace{8mm}
|
|
\underbrace{l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Uparrow \,\underbrace{(v\;\;\Downarrow\;v\,)}_{z'}}_{Regel\;(1)} \\\\
|
|
l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,)
|
|
\hspace{1cm}&==\hspace{10mm}
|
|
l_1\sigma (1) = x\;\Uparrow \, ( \, u \; \Downarrow \; u\,) \\
|
|
\end{align*}
|
|
\textbf{Analog mit (2)(2) und allen anderen kritischen Paaren (wobei (1)(2) und (2)(1) hier triviale kritische Paare w\"aren!)}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\begin{tiny}
|
|
\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
|
|
\end{tiny}
|
|
\end{document}
|