confluence (original) (raw)

Call a binary relation → on a set S a reduction. Let →* be the reflexive transitive closure of →. Two elements a,b∈S are said to be joinable if there is an element c∈S such that a→*c and b→*c. Graphically, this means that

\xymatrix⁢@⁢R-=10⁢p⁢t⁢a⁢\ar⁢[d⁢r]*⁢&⁢c⁢b⁢\ar⁢[u⁢r]*

where the starred arrows represent

respectively (m,n are non-negative integers). The case m=0 (or n=0) means a→c (or b→c).

Definition. → is said to be confluent if whenever x→*a and x→*b, then a,b are joinable. In other words, → is confluent iff →* has the amalgamation property. Graphically, this says that, whenever we have a diagram

\xymatrix⁢@⁢R-=10⁢p⁢t⁢&⁢a⁢x⁢\ar⁢[u⁢r]*⁢\ar⁢[d⁢r]*⁢&⁢&⁢b

then it can be “completed” into a “diamond”:

\xymatrix⁢@⁢R-=10⁢p⁢t⁢&⁢a⁢\ar⁢[d⁢r]*⁢x⁢\ar⁢[u⁢r]*⁢\ar⁢[d⁢r]*⁢&⁢&⁢c⁢&⁢b⁢\ar⁢[u⁢r]*⁢&

Remark. A more general property than confluence, called semi-confluence is defined as follows: → is semi-confluent if for any triple x,a,b∈S such that x→a and x→*b, then a,b are joinable. It turns out that this seemingly weaker notion is actually equivalent to the stronger notion of confluence. In addition, it can be shown that → is confluent iff → has the Church-Rosser property.

References

• 1 F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press (1998).