Confluence (abstraktes Umschreiben) – Wikipedia

Bild 1: Der Name Zusammenfluss ist von der Geographie inspiriert, was bedeutet, dass sich dort zwei Gewässer treffen.

In der Informatik Zusammenfluss ist eine Eigenschaft von Umschreibesystemen, die beschreibt, welche Begriffe in einem solchen System auf mehr als eine Weise umgeschrieben werden können, um das gleiche Ergebnis zu erzielen. Dieser Artikel beschreibt die Eigenschaften in der abstraktesten Einstellung eines abstrakten Umschreibungssystems.

Motivierende Beispiele[edit]

Die üblichen Regeln der Elementararithmetik bilden ein abstraktes Umschreibungssystem. Zum Beispiel kann der Ausdruck (11 + 9) × (2 + 4) entweder links oder rechts in Klammern ausgewertet werden; In beiden Fällen wird jedoch letztendlich das gleiche Ergebnis erzielt. Dies deutet darauf hin, dass das arithmetische Umschreibungssystem konfluent ist.

Ein zweites, abstrakteres Beispiel ergibt sich aus dem folgenden Beweis, dass jedes Gruppenelement der Umkehrung seiner Umkehrung entspricht:
^[1]

Dieser Beweis geht von den gegebenen Gruppenaxiomen A1-A3 aus und legt fünf Sätze R4, R6, R10, R11 und R12 fest, von denen jeder einige frühere verwendet, wobei R12 der Hauptsatz ist. Einige der Beweise erfordern nicht offensichtliche, wenn nicht kreative Schritte, wie das umgekehrte Anwenden des Axioms A2, wodurch “1” in “umgeschrieben wird.ein⁻¹ ⋅ a “im ersten Schritt des Beweises von R6. Eine der historischen Motivationen für die Entwicklung der Theorie des Umschreibens von Begriffen war die Notwendigkeit solcher Schritte zu vermeiden, die für einen unerfahrenen Menschen schwer zu finden sind, geschweige denn für ein Computerprogramm.

Wenn ein Begriff Umschreibesystem ist konfluent und BeendenEs gibt eine einfache Methode, um die Gleichheit zwischen zwei Ausdrücken zu beweisen (auch bekannt als) Begriffe) s und t: Beginnen mit sGleichheiten anwenden^{[note 1]} so lange wie möglich von links nach rechts, um schließlich eine Laufzeit zu erhalten s ‘. Erhalten von t ein Begriff t ‘ auf eine ähnliche Weise. Wenn beide Begriffe s ‘ und t ‘ stimme also buchstäblich zu s und t sind (nicht überraschend) gleich erwiesen. Wichtiger, wenn sie nicht übereinstimmen, s und t kann nicht gleich sein. Das heißt, zwei beliebige Begriffe s und t das kann überhaupt als gleich erwiesen werden, kann so durch diese Methode sein.

Der Erfolg dieser Methode hängt nicht von einer bestimmten Reihenfolge ab, in der die Umschreiberegeln angewendet werden sollen Zusammenfluss stellt sicher, dass jede Folge von Regelanwendungen letztendlich zum gleichen Ergebnis führt (während die Beendigung Eigenschaft stellt sicher, dass jede Sequenz irgendwann überhaupt ein Ende erreicht).^[2] Wenn daher ein konfluentes und terminierendes Termumschreibungssystem für eine Gleichungstheorie bereitgestellt werden kann,^{[note 2]}

Es ist kein Hauch von Kreativität erforderlich, um Beweise für die Gleichheit der Begriffe zu erbringen. Diese Aufgabe wird daher für Computerprogramme zugänglich. Moderne Ansätze behandeln allgemeiner abstrakte Umschreibungssysteme eher, als Begriff Umschreiben von Systemen; Letztere sind ein Sonderfall des ersteren.

Allgemeiner Fall und Theorie[edit]

Bild 2: In diesem Diagramm ist ein reduziert sich auf beide b oder c in null oder mehr Schritten zum Umschreiben (gekennzeichnet durch das Sternchen). Damit die Umschreibungsbeziehung konfluent ist, müssen beide Reduktionen wiederum auf einige gemeinsame reduziert werden d.

Ein Umschreibungssystem kann als gerichteter Graph ausgedrückt werden, in dem Knoten Ausdrücke und Kanten Umschreibungen darstellen. Also zum Beispiel, wenn der Ausdruck ein kann umgeschrieben werden b, dann sagen wir das b ist ein reduzieren von ein (Alternative, ein reduziert zu b, oder ein ist ein Erweiterung von b). Dies wird in Pfeilnotation dargestellt. ein → b zeigt an, dass ein reduziert zu b. Intuitiv bedeutet dies, dass der entsprechende Graph eine gerichtete Kante von hat ein zu b.

Wenn zwischen zwei Diagrammknoten ein Pfad vorhanden ist c und ddann bildet es a Reduktionssequenz. Also zum Beispiel, wenn c → c‘→ c” → … → d‘→ d, dann können wir schreiben c ∗→ d, was auf die Existenz einer Reduktionssequenz aus hinweist c zu d. Formal, ∗→ ist der reflexiv-transitive Verschluss von →. Anhand des Beispiels aus dem vorherigen Absatz haben wir (11 + 9) × (2 + 4) → 20 × (2 + 4) und 20 × (2 + 4) → 20 × 6, also (11 + 9) × ( 2 + 4) ∗→ 20 × 6.

Wenn dies festgestellt ist, kann die Konfluenz wie folgt definiert werden. ein ∈ S. gilt als konfluent, wenn für alle Paare b, c ∈ S. so dass ein ∗→ b und ein ∗→ cgibt es eine d ∈ S. mit b ∗→ d und c ∗→ d. Wenn jeder ein ∈ S. ist konfluent, wir sagen, dass → konfluent ist oder die hat Church-Rosser Eigentum. Diese Eigenschaft wird manchmal auch als bezeichnet Diamant Eigentumnach der Form des rechts gezeigten Diagramms. Einige Autoren behalten sich den Begriff vor Diamanteigenschaft für eine Variante des Diagramms mit einzelnen Reduzierungen überall; das heißt, wann immer ein → b und ein → cmuss es eine geben d so dass b → d und c → d. Die Single-Reduction-Variante ist strikt stärker als die Multi-Reduction-Variante.

Lokaler Zusammenfluss[edit]

Bild 3: Zyklisches, lokal konfluentes, aber nicht global konfluentes Umschreibungssystem^[3]

Bild 4: Unendliches nicht-zyklisches, lokal konfluentes, aber nicht global konfluentes Umschreibungssystem^[3]

Ein Element ein ∈ S. soll lokal (oder schwach) konfluent sein, wenn für alle b, c ∈ S. mit ein → b und ein → c es gibt d ∈ S. mit b ∗→ d und c ∗→ d. Wenn jeder ein ∈ S. ist lokal konfluent, dann heißt → lokal (oder schwach) konfluent oder hat die schwaches Church-Rosser-Eigentum. Dies unterscheidet sich vom Zusammenfluss darin b und c muss reduziert werden von ein in einem Schritt. In Analogie dazu wird Konfluenz manchmal als bezeichnet globaler Zusammenfluss.

Die Beziehung ∗→, eingeführt als Notation für Reduktionssequenzen, kann als eigenständiges Umschreibungssystem angesehen werden, dessen Beziehung der reflexiv-transitive Abschluss von ist →. Da eine Sequenz von Reduktionssequenzen wieder eine Reduktionssequenz ist (oder äquivalent, da die Bildung des reflexiv-transitiven Verschlusses idempotent ist), ∗∗→ = ∗→. Daraus folgt, dass → genau dann konfluent ist, wenn ∗→ ist lokal konfluent.

Ein Umschreibungssystem kann lokal konfluent sein, ohne (global) konfluent zu sein. Beispiele sind in Bild 3 und 4 gezeigt. Newmans Lemma besagt jedoch, dass ein lokal konfluentes Umschreibungssystem keine unendlichen Reduktionssequenzen aufweist (in diesem Fall soll es so sein) Beenden oder stark normalisierend), dann ist es global konfluent.

Halbkonfluenz[edit]

Die Definition der lokalen Konfluenz unterscheidet sich von der der globalen Konfluenz darin, dass nur Elemente berücksichtigt werden, die von einem bestimmten Element in einem einzigen Umschreibeschritt erreicht wurden. Indem wir ein Element betrachten, das in einem einzigen Schritt erreicht wird, und ein anderes Element, das durch eine beliebige Sequenz erreicht wird, gelangen wir zum Zwischenkonzept der Halbkonfluenz: ein ∈ S. soll, wenn überhaupt, halbkonfluent sein b, c ∈ S. mit ein → b und ein ∗→ c es gibt d ∈ S. mit b ∗→ d und c ∗→ d;; wenn jeder ein ∈ S. ist halbkonfluent, wir sagen, dass → halbkonfluent ist.

Ein halbkonfluentes Element muss nicht konfluent sein, aber ein halbkonfluentes Umschreibungssystem ist notwendigerweise konfluent, und ein konfluentes System ist trivial halbkonfluent.

Starker Zusammenfluss[edit]

Starke Konfluenz ist eine weitere Variation der lokalen Konfluenz, die es uns ermöglicht zu schließen, dass ein Umschreibungssystem global konfluent ist. Ein Element ein ∈ S. soll, wenn überhaupt, stark konfluent sein b, c ∈ S. mit ein → b und ein → c es gibt d ∈ S. mit b ∗→ d und entweder c → d oder c = d;; wenn jeder ein ∈ S. ist stark konfluent, wir sagen, dass → stark konfluent ist.

Ein konfluentes Element muss nicht stark konfluent sein, aber ein stark konfluentes Umschreibungssystem ist notwendigerweise konfluent.

Beispiele für konfluente Systeme[edit]

Siehe auch[edit]

Verweise[edit]

Externe Links[edit]