Confluence is a property of term rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. Rewriting in mathematics, computer science and logic covers a wide range of non-deterministic methods of replacing subterms of a formula with other terms. ...

Motivating example

Consider the rules of regular arithmetic. We can think of these rules as forming a rewriting system. Suppose we are given the expression

We can rewrite this expression in two ways -- either simplifying the first bracket, or the second. Simplifying the first bracket, we have

Simplifying the second, gives

We get the same result from rewriting the term in two different ways. This suggests that the rewriting system formed from regular arithmetic is a confluent rewriting system.

General case and theory

We can think of a rewriting system abstractly as being a set S, together with a relation R which is a subset of S×S. Instead of denoting relations as pairs (s, t), with s,t ∈ S, we write s →_i t, where i is from some index set I. If u ∈ S, and u →_j v for some j ∈ I, then we say v is a reduct of u (alternatively v is an expansion of u, or u is reduced to v). We can also think of a chain of reductions of some element: if w ∈ S, then we may have

where i_k ∈ I. We call this chain a reduction sequence, or just a reduction of w. If the reduction sequence terminates, say in w_n, we write

,

reflecting that relations in I were chosen. If I is clear from context then we can omit this subscript.

With this established, confluence can be defined as follows. Let a, b, c ∈ S, with a →* b and a →* c. If a is confluent, there exists a d ∈ A with b →* d and c →* d. If every a ∈ S is confluent, we say that → is confluent, or has the Church-Rosser property. This property is also called the diamond property, after the shape of the diagram shown on the right. This shape is a rhombus In geometry, a rhombus (also known as a rhomb) is a quadrilateral in which all of the sides are of equal length. ...

Variations

A number of variations on the idea of confluence exist. These are important since they enable us to draw equivalences between confluence in the sense above and these variations.

We have local confluence (also known as weak confluence), which states that, given a, b, c ∈ S, a → b and a → c, and a is locally confluent, there exists a d ∈ A with b →* d and c →* d. If every a ∈ S is confluent, then we say that → is locally confluent, or has 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 known as global confluence.

If → is confluent, then →* is weakly confluent, and vice versa.

Local confluence can hold in some system, but global confluence may not hold.

See also

• critical pair

References

• Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003

External links

• Eric W. Weisstein, Confluent at MathWorld.