https://wiki-de.moshellshocker.dns64.de/index.php?action=history&feed=atom&title=Konfluenz_%28Informatik%29 2026-06-09T08:10:22Z Versionsgeschichte dieser Seite in Wikipedia (Deutsch) – Lokale Kopie MediaWiki 1.43.8 https://wiki-de.moshellshocker.dns64.de/index.php?title=Konfluenz_(Informatik)&diff=336757&oldid=prev 2025-04-18T05:18:06Z

<p></p> <p><b>Neue Seite</b></p><div>{{Belege fehlen}}<br /> [[Datei:Konvergenz.png|thumb|right|Konfluenz in einem [[Termersetzungssystem]]]]<br /> <br /> &#039;&#039;&#039;Konfluenz&#039;&#039;&#039; ist ein Begriff aus der [[Theoretische Informatik|theoretischen Informatik]] und bezeichnet die Eigenschaft eines [[Transitionssystem]]s, jedem Element &#039;&#039;höchstens&#039;&#039; eine [[Normalform]] zuzuordnen. Das heißt, wenn ein Element oder ein Term auf verschiedene Art und Weise ersetzt werden kann, wird es nach weiteren Ersetzungen immer zum gleichen Term überführt. Konfluenz ist also analog zu mehreren Strömen, die zu einem Strom zusammenfließen. Im [[Lambda-Kalkül]] wird dieses durch das [[Church-Rosser-Theorem]] gezeigt.<br /> <br /> Formal bedeutet dies:<br /> <br /> Ein Transitionssystem &lt;math&gt;(D,\rightarrow^*)&lt;/math&gt; heißt genau dann &#039;&#039;konfluent&#039;&#039;, wenn für alle &lt;math&gt;t,t_1,t_2 \in D&lt;/math&gt; gilt: wenn &lt;math&gt;t \rightarrow^* t_1&lt;/math&gt; und &lt;math&gt;t \rightarrow^* t_2&lt;/math&gt;, dann gibt es ein &lt;math&gt;t&#039; \in D&lt;/math&gt; mit &lt;math&gt;t_1 \rightarrow^* t&#039;&lt;/math&gt; und &lt;math&gt;t_2 \rightarrow^* t&#039;&lt;/math&gt;.<br /> <br /> Konfluente [[Termersetzungssystem]]e sind sehr nützlich, wenn man beweisen möchte, dass Terme, beispielsweise in einem Gleichungssystem, äquivalent sind. Eine Gleichung ist beweisbar korrekt genau dann, wenn die Terme auf beiden Seiten des Gleichheitssymbols zum gleichen Term umgeformt werden können.<br /> <br /> Konfluenz ist [[Entscheidbar|unentscheidbar]] auf der Menge aller Termersetzungssysteme. Für [[Terminiertheit|terminierende]] Termersetzungssysteme ist die Konfluenz aber entscheidbar. Denn nach dem [[Diamond Lemma]] ist die Konfluenz für ein terminierendes Termersetzungssystem äquivalent zur [[Lokale Konfluenz|lokalen Konfluenz]]. Und die lokale Konfluenz ist nach dem [[Kritisches-Paar-Lemma]] entscheidbar, da ein Termersetzungssystem lokal konfluent ist, genau dann wenn alle seine kritischen Paare [[Zusammenführbarkeit|zusammenführbar]] sind.<br /> <br /> == Weblinks ==<br /> * Dieter Hofbauer: [http://www.theory.informatik.uni-kassel.de/~hofbauer/formal_methods/skript/rewriting4.pdf Konfluenz von Wort und Termersetzung] (PDF; 156&amp;nbsp;kB)<br /> <br /> {{Normdaten|TYP=s|GND=4516767-9}}<br /> <br /> [[Kategorie:Automatentheorie]]</div>

imported>Müllt-Renner