Confluence

Definition

An abstract reduction system $(A,\to )$ is confluent if, whenever $a{\to }^{\ast }b$ and $a{\to }^{\ast }c$, there exists $d$ such that $b{\to }^{\ast }d$ and $c{\to }^{\ast }d$.

Equivalently, any two reduction sequences starting from the same object can be joined again.

Consequences

Confluence implies that if an element has a normal form, then that normal form is unique. This makes reduction a reliable method of computing canonical representatives.

Confluence is closely related to local confluence and diamond properties, which often provide easier sufficient conditions for it.

Related Concepts

Abstract Reduction System
Church-Rosser Property
Diamond Property (graph theory)
Normal Form
Strong Normalization
Convergent (Rewriting)

References

baader1998-term-rewriting