confluence
Call a binary relation^{} $\to $ on a set $S$ 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
$\text{xymatrix}\mathrm{@}R-=10pta\text{ar}{[dr]}^{*}\mathrm{\&}cb\text{ar}{[ur]}_{*}$
where the starred arrows represent
$$a\to {a}_{1}\to \mathrm{\cdots}\to {a}_{n}\to c\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}b\to {b}_{1}\to \mathrm{\cdots}\to {b}_{m}\to c$$ |
respectively ($m,n$ are non-negative integers). The case $m=0$ (or $n=0$) 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 $a,b$ are joinable. In other words, $\to $ is confluent iff ${\to}^{*}$ has the amalgamation property. Graphically, this says that, whenever we have a diagram
$\text{xymatrix}\mathrm{@}R-=10pt\mathrm{\&}ax\text{ar}{[ur]}^{*}\text{ar}{[dr]}_{*}\mathrm{\&}\mathrm{\&}b$
then it can be “completed” into a “diamond”:
$\text{xymatrix}\mathrm{@}R-=10pt\mathrm{\&}a\text{ar}{[dr]}^{*}x\text{ar}{[ur]}^{*}\text{ar}{[dr]}_{*}\mathrm{\&}\mathrm{\&}c\mathrm{\&}b\text{ar}{[ur]}_{*}\mathrm{\&}$
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 $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 $\to $ is confluent iff $\to $ has the Church-Rosser property^{}.
References
- 1 F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press (1998).
Title | confluence |
Canonical name | Confluence |
Date of creation | 2013-03-22 17:47:24 |
Last modified on | 2013-03-22 17:47:24 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 14 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 68Q42 |
Related topic | ChurchRosserProperty |
Related topic | AmalgamationProperty |
Related topic | NormalizingReduction |
Related topic | TerminatingReduction |
Defines | confluent |
Defines | joinable |
Defines | semi-confluent |