View source for Confluence (abstract rewriting)

[[Image:Koblenz im Buga-Jahr 2011 - Deutsches Eck 01.jpg|thumb|The name ''[[confluence]]'' is inspired from geography, where it means the meeting of two bodies of water.]]
In computer science and mathematics, '''confluence''' is a property of [[rewriting]] systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an [[abstract rewriting system]].
== Motivating examples ==
[[File:Confluence example expression.svg|right]]
The usual rules of elementary arithmetic form an abstract rewriting system.
For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses;
however, in both cases the same result is eventually obtained.
If every arithmetic expression evaluates to the same result regardless of reduction strategy, the arithmetic rewriting system is said to be ground-confluent. Arithmetic rewriting systems may be confluent or only ground-confluent depending on details of the rewriting system.<ref>{{cite web |last1=Walters |first1=H.R. |last2=Zantema |first2=H. |title=Rewrite systems for integer arithmetic |url=https://pure.tue.nl/ws/files/4421201/433758.pdf |publisher=Utrecht University |date=Oct 1994}}</ref>
A second, more abstract example is obtained from the following proof of each [[Group (mathematics)|group]] element equalling the [[Group (mathematics)#Definition|inverse]] of its inverse:<ref>{{harvnb|Bläsius|Bürckert|1992|p=134}}: axiom and proposition names follow the original text</ref>
{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Group axioms
|-
| '''A1''' || 1 ⋅ ''a'' || = ''a''
|-
| '''A2''' || ''a''<sup>−1</sup> ⋅ ''a'' || = 1
|-
| '''A3''' &nbsp; &nbsp; || (''a'' ⋅ ''b'') ⋅ ''c'' || = ''a'' ⋅ (''b'' ⋅ ''c'')
|}
{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Proof of '''R4''': ''a''<sup>−1</sup>⋅(''a''⋅''b'') = ''b''
|-
|   || ''a''<sup>−1</sup> ⋅ (''a'' ⋅ ''b'') ||
|-
| = || (''a''<sup>−1</sup> ⋅ ''a'') ⋅ ''b'' || by A3(r) &nbsp;  &nbsp;
|-
| = || 1 ⋅ ''b'' || by A2
|-
| = || ''b'' || by A1
|}
{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Proof of '''R6''': (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ 1 = ''a''
|-
|   || (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ 1 ||
|-
| = || (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ (''a''<sup>−1</sup> ⋅ ''a'') || by A2(r)
|-
| = || ''a'' || by R4
|}
{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Proof of '''R10''': (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ ''b'' = ''a'' ⋅ ''b''
|-
|   || (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ ''b'' ||
|-
| = || (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ (''a''<sup>−1</sup> ⋅ (''a'' ⋅ ''b'')) || by R4(r)
|-
| = || ''a'' ⋅ ''b'' || by R4
|}
{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Proof of '''R11''': ''a'' ⋅ 1 = ''a''
|-
|   || ''a'' ⋅ 1 ||
|-
| = || (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ 1 || by R10(r)
|-
| = || ''a'' || by R6
|}
{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Proof of '''R12''': (''a''<sup>−1</sup>)<sup>−1</sup> = ''a''
|-
|   || (''a''<sup>−1</sup>)<sup>−1</sup> ||
|-
| = || (''a''<sup>−1</sup>)<sup>−1</sup> ⋅ 1 || by R11(r) &nbsp;  &nbsp;
|-
| = || ''a'' || by R6
|}
{{clear}}
This proof starts from the given group axioms A1–A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem. Some of the proofs require non-obvious, or even creative, steps, like applying axiom A2 in reverse, thereby rewriting "1" to "''a''<sup>−1</sup> ⋅ a" in the first step of R6's proof. One of the historical motivations to develop the ''theory of term rewriting'' was to avoid the need for such steps, which are difficult to find by an inexperienced human, let alone by a computer program {{Citation needed|date=April 2023}}.
If a [[Term rewriting#Term rewriting systems|term rewriting system]] is confluent and ''[[Rewriting#Termination|terminating]]'', a straightforward method exists to prove equality between two expressions (also known as ''[[term (logic)|terms]]'') ''s'' and ''t'':
Starting with ''s'', apply equalities<ref group=note>then called ''rewrite rules'' to emphasize their left-to-right orientation</ref> from left to right as long as possible, eventually obtaining a term ''s′''.
Obtain from ''t'' a term ''t′'' in a similar way.
If both terms ''s′'' and ''t′'' literally agree, then ''s'' and ''t'' are proven equal.
More importantly, if they disagree, then ''s'' and ''t'' cannot be equal.
That is, any two terms ''s'' and ''t'' that can be proven equal at all can be done so by that method.
The success of that method does not depend on a certain sophisticated order in which to apply rewrite rules, as confluence ensures that any sequence of rule applications will eventually lead to the same result (while the ''termination'' property ensures that any sequence will eventually reach an end at all). Therefore, if a confluent and terminating term rewriting system can be provided for some [[equational theory]],<ref group=note>The [[Knuth–Bendix completion algorithm]] can be used to compute such a system from a given set of equations. Such a system e.g. for groups is shown [[Word problem (mathematics)#Example: A term rewriting system to decide the word problem in the free group|here]], with its propositions consistently numbered. Using it, a proof of e.g. R6 consists in applying R11 and R12 in any order to the term (''a''<sup>−1</sup>)<sup>−1</sup>⋅1 to obtain the term ''a''; no other rules are applicable.</ref>
not a tinge of creativity is required to perform proofs of term equality; that task hence becomes amenable to computer programs. Modern approaches handle more general ''abstract rewriting systems'' rather than ''term'' rewriting systems; the latter are a special case of the former.
== General case and theory ==
[[Image:Confluence.svg|right|200px|thumb|In this diagram, {{mvar|a}} reduces to both {{mvar|b}} or {{mvar|c}} in zero or more rewrite steps (denoted by the asterisk). In order for the rewrite relation to be confluent, both reducts must in turn reduce to some common {{mvar|d}}.]]
A rewriting system can be expressed as a [[directed graph]] in which nodes represent expressions and edges represent rewrites. So, for example, if the expression ''a'' can be rewritten into ''b'', then we say that ''b'' is a ''reduct'' of ''a'' (alternatively, ''a'' ''reduces to'' ''b'', or ''a'' is an ''expansion'' of ''b''). This is represented using arrow notation; ''a'' → ''b'' indicates that ''a'' reduces to ''b''. Intuitively, this means that the corresponding graph has a directed edge from ''a'' to ''b''.
If there is a path between two graph nodes ''c'' and ''d'', then it forms a ''reduction sequence''. So, for instance, if ''c'' → ''c′'' → ''c′′'' → ... → ''d′'' → ''d'', then we can write ''c'' {{overset|∗|→}} ''d'', indicating the existence of a reduction sequence from ''c'' to ''d''. Formally, {{overset|∗|→}} is the [[Closure (mathematics)#Binary relation closures|reflexive-transitive closure]] of →. Using the example from the previous paragraph, we have (11+9)×(2+4) → 20×(2+4) and 20×(2+4) → 20×6, so (11+9)×(2+4) {{overset|∗|→}} 20×6.
With this established, confluence can be defined as follows. ''a'' ∈ ''S'' is deemed '''confluent''' if for all pairs ''b'', ''c'' ∈ ''S'' such that ''a'' {{overset|∗|→}} ''b'' and ''a'' {{overset|∗|→}} ''c'', there exists a ''d'' ∈ ''S'' with ''b'' {{overset|∗|→}} ''d'' and ''c'' {{overset|∗|→}} ''d'' (denoted <math>b \mathbin\downarrow c</math>). If every ''a'' ∈ ''S'' is confluent, we say that → is confluent. This property is also sometimes called the ''diamond property'', after the shape of the diagram shown on the right. Some authors reserve the term ''diamond property'' for a variant of the diagram with single reductions everywhere; that is, whenever ''a'' → ''b'' and ''a'' → ''c'', there must exist a ''d'' such that ''b'' → ''d'' and ''c'' → ''d''. The single-reduction variant is strictly stronger than the multi-reduction one.
=== Ground confluence ===
A term rewriting system is '''ground confluent''' if every [[ground term]] is confluent, that is, every term without variables.<ref>{{cite book |last1=Robinson |first1=Alan J. A. |last2=Voronkov |first2=Andrei |title=Handbook of Automated Reasoning |date=5 July 2001 |publisher=Gulf Professional Publishing |isbn=978-0-444-82949-8 |page=560 |url=https://books.google.com/books?id=X3z8ujBRgmEC&dq=ground%20confluent&pg=PA560 |language=en}}</ref>
=== Local confluence ===
[[File:Cyclic locally, but not globally confluent rewrite system.png|thumb|Figure 1: Cyclic, locally-confluent, but not globally confluent rewrite system<ref name="Dershowitz.Jouannaud.1990.Fig2">{{cite book|isbn=0-444-88074-7|editor=Jan van Leeuwen|title=Formal Models and Semantics|publisher=Elsevier|series=Handbook of Theoretical Computer Science|volume=B|year=1990|author=N. Dershowitz and J.-P. Jouannaud|contribution=Rewrite Systems|pages=243&ndash;320}} Here: p.268, Fig.2a+b.</ref>]]
[[File:Non-cyclic locally, but not globally confluent rewrite system.gif|thumb|Figure 2: Infinite non-cyclic, locally-confluent, but not globally confluent rewrite system<ref name="Dershowitz.Jouannaud.1990.Fig2"/>]]
An element ''a'' ∈ ''S'' is said to be '''locally confluent'''  (or ''weakly confluent''{{sfn|Terese|2003|pp=10-11}}) if for all ''b'', ''c'' ∈ ''S'' with ''a'' → ''b'' and ''a'' → ''c'' there exists ''d'' ∈ ''S'' with ''b'' {{overset|∗|→}} ''d'' and ''c'' {{overset|∗|→}} ''d''. If every ''a'' ∈ ''S'' is locally confluent, then → is called locally confluent, or having the ''weak Church–Rosser property''. This is different from confluence in that ''b'' and ''c'' must be reduced from ''a'' in one step. In analogy with this, confluence is sometimes referred to as ''global confluence''.
The relation {{overset|∗|→}}, introduced as a notation for reduction sequences, may be viewed as a rewriting system in its own right, whose relation is the [[Closure (mathematics)#Binary relation closures|reflexive-transitive closure]] of ''→''. Since a sequence of reduction sequences is again a reduction sequence (or, equivalently, since forming the reflexive-transitive closure is [[idempotence#Unary operation|idempotent]]), {{overset|∗|{{overset|∗|→}}}} = {{overset|∗|→}}. It follows that → is confluent if and only if {{overset|∗|→}} is locally confluent.
A rewriting system may be locally confluent without being (globally) confluent. Examples are shown in figures 1 and 2. However, [[Newman's lemma]] states that if a locally confluent rewriting system has no infinite reduction sequences (in which case it is said to be ''terminating'' or ''strongly normalizing''), then it is globally confluent.
=== Church–Rosser property ===
A rewriting system is said to possess the '''Church–Rosser property''' if and only if <math>x \stackrel{*}{\leftrightarrow} y</math> implies <math>x\mathbin\downarrow y</math> for all objects ''x'', ''y''. [[Alonzo Church]] and [[J. Barkley Rosser]] proved in 1936 that [[lambda calculus]] has this property;<ref>Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans.
AMS, 39:472-482, 1936</ref> hence the name of the property.{{sfn|Baader|Nipkow|1998|p=9}} (The fact that lambda calculus has this property is also known as the [[Church–Rosser theorem]].) In a rewriting system with the Church–Rosser property the word problem may be reduced to the search for a common successor. In a Church–Rosser system, an object has ''at most one'' [[normal form (abstract rewriting)|normal form]]; that is the normal form of an object is unique if it exists, but it may well not exist. In lambda calculus for instance, the expression (λx.xx)(λx.xx) does not have a normal form because there exists an infinite sequence of [[β-reduction]]s (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ...<ref>{{cite book |last1=Cooper |first1=S. B. |title=Computability theory |date=2004 |publisher=Chapman & Hall/CRC |location=Boca Raton |isbn=1584882379 |page=184}}</ref>
A rewriting system possesses the Church–Rosser property [[if and only if]] it is confluent.{{sfn|Baader|Nipkow|1998|p=11}} Because of this equivalence, a fair bit of variation in definitions is encountered in the literature. For instance, in "Terese" the Church–Rosser property and confluence are defined to be synonymous and identical to the definition of confluence presented here; Church–Rosser as defined here remains unnamed, but is given as an equivalent property; this departure from other texts is deliberate.{{sfn|Terese|2003|p=11}}
=== Semi-confluence ===
The definition of local confluence differs from that of global confluence in that only elements reached from a given element in a single rewriting step are considered. By considering one element reached in a single step and another element reached by an arbitrary sequence, we arrive at the intermediate concept of semi-confluence: ''a'' ∈ ''S'' is said to be '''semi-confluent''' if for all ''b'', ''c'' ∈ ''S'' with ''a'' → ''b'' and ''a'' {{overset|∗|→}} ''c'' there exists ''d'' ∈ ''S'' with ''b'' {{overset|∗|→}} ''d'' and ''c'' {{overset|∗|→}} ''d''; if every ''a'' ∈ ''S'' is semi-confluent, we say that → is semi-confluent.
A semi-confluent element need not be confluent, but a semi-confluent rewriting system is necessarily confluent, and a confluent system is trivially semi-confluent.
=== Strong confluence ===
Strong confluence is another variation on local confluence that allows us to conclude that a rewriting system is globally confluent. An element ''a'' ∈ ''S'' is said to be '''strongly confluent''' if for all ''b'', ''c'' ∈ ''S'' with ''a'' → ''b'' and ''a'' → ''c'' there exists ''d'' ∈ ''S'' with ''b'' {{overset|∗|→}} ''d'' and either ''c'' → ''d'' or ''c'' = ''d''; if every ''a'' ∈ ''S'' is strongly confluent, we say that → is strongly confluent.
A confluent element need not be strongly confluent, but a strongly confluent rewriting system is necessarily confluent.
== Examples of confluent systems ==
* Reduction of [[polynomial]]s modulo an [[ideal (ring theory)|ideal]] is a confluent rewrite system provided one works with a [[Gröbner basis]].
* [[Matsumoto's theorem (group theory)|Matsumoto's theorem]] follows from confluence of the braid relations.
* β-reduction of λ-terms is confluent by the [[Church–Rosser theorem]].
== See also ==
* [[Convergence (logic)]]
* [[Critical pair (logic)]]
* [[Normal form (abstract rewriting)]]
== Notes ==
{{reflist|group=note}}
== References ==
{{reflist}}
* {{cite book|author1="Terese"|first2=Marc|last2=Bezem|first3=Jan Willem|last3=Klop|author3-link=Jan Willem Klop |first4=Roel|last4=de Vrijer|title=Term rewriting systems|publisher=Cambridge University Press|series=Cambridge Tracts in Theoretical Computer Science|date=2003|isbn=0-521-39115-6|ref={{harvid|Terese|2003}}}}
* {{cite book |last1=Baader |first1=Franz|author1-link=Franz Baader |last2=Nipkow |first2=Tobias|author2-link=Tobias Nipkow |title=Term Rewriting and All That |date=1998 |publisher=Cambridge University Press |isbn=978-0-521-77920-3 |url=https://books.google.com/books?id=N7BvXVUCQk8C&q=confluence+OR+confluent|language=en}}
* {{cite book| title=Deduktionssysteme| year=1992| page=291| publisher=Oldenbourg|editor1-first=K. H.|editor1-last=Bläsius|editor2-first=H.-J.|editor2-last=Bürckert}}
==External links==
* {{MathWorld | urlname=Confluent | title=Confluent}}
{{Authority control}}
{{DEFAULTSORT:Confluence (Abstract Rewriting)}}
[[Category:Rewriting systems]]