PlanetMath: confluence

(more info)

Math for the people, by the people.

Main Menu

sections Encyclopædia
Papers
Books
Expositions

meta Requests (191)
Orphanage
Unclass'd
Unproven (496)
Corrections (10)
Classification

talkback Polls
Forums
Feedback
Bug Reports

downloads Snapshots
PM Book

information News
Docs
Wiki
ChangeLog
TODO List
Legalese
About

Entry average rating: No information on entry rating

confluence

(Definition)

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

$\xymatrix@R-=10pt{ a\ar[dr]^{*}\ &c\ b\ar[ur]_{*} }$

where the starred arrows represent

$\displaystyle a\to a_1\to \cdots \to a_n \to c$ and $\displaystyle \qquad b\to b_1\to \cdots \to b_m \to c$

respectively (

are non-negative integers). The case

(or

) means $a\to c$ (or $b\to c$ ).

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

$\xymatrix@R-=10pt{ &a\ x\ar[ur]^{*}\ar[dr]_{*} &\ &b }$

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

$\xymatrix@R-=10pt{ &a\ar[dr]^{*}\ x\ar[ur]^{*}\ar[dr]_{*} &&c\ &b\ar[ur]_{*}& }$

Remark. A more general property than confluence, called semi-confluence is defined as follows: $\to$ is semi-confluent if for any triple $x,a,b\in S$ such that $x\to a$ and $x\to^* b$ , then 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 $\to$ is confluent iff $\to$ has the Church-Rosser property.