Confluence (term rewriting)

From Wikipedia, the free encyclopedia

For other uses, see Confluence (disambiguation).

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.

1 Motivating example
2 General case and theory
3 See also
4 References
5 External links

[edit] 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

$(11 + 9) \times (2 + 4)$

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

$20 \times (2 + 4) = 20 \times 6 = 120$

Simplifying the second, gives

$(11 + 9) \times 6 = 20 \times 6 = 120$

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.

[edit] 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

$w \rightarrow_{i_1} w_1 \rightarrow_{i_2} w_2 \rightarrow_{i_3} \cdots$

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

$w \rightarrow^*_I w_n$ ,

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 ∈ S 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 sometimes called the diamond property, after the shape of the diagram shown on the right. Caution: other presentations 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.

[edit] Local confluence

An element a ∈ S is said to be locally (or weakly) confluent if for all b, c ∈ S with a → b and a → c there exists d ∈ S with b →* d and c →* d. If every a ∈ S is locally confluent, we say that → is locally (or weakly) 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 referred to as global confluence.

We may view →*, which we introduced as a notation for reduction sequences, as a rewriting system in its own right, whose relation is the transitive closure of R. Since a sequence of reduction sequences is again a reduction sequence (or, equivalently, since forming the transitive closure is idempotent), →** = →*. It follows that → is confluent if and only if →* is locally confluent.

A rewriting system may be locally confluent without being globally confluent. 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.

[edit] 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 →* c there exists d ∈ S with b →* d and c →* 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.

[edit] 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 →* d and either c → d or c = d; if every a ∈ S is strongly confluent, we say that → is strongly confluent.

A strongly confluent element need not be confluent, but a strongly confluent rewriting system is necessarily confluent.

[edit] See also

[edit] References

Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003
Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998