nLab confluent category

Definition

A category is confluent if for any span $B \leftarrow A \to C$, there exists a cospan $B \to D \leftarrow C$. Note that we do not require the resulting square to commute.

Remarks

If the morphisms in a category represent (sequences of) “rewriting” operations, then confluence means that any two ways to rewrite the same thing can eventually be brought back together.

If $(X,\rightarrow)$ is an abstract rewriting system ie. a set equipped with a binary relation $\rightarrow$ and if $\rightarrow^{*}$ is the reflexive-transitive closure of $\rightarrow$, then we say that $\rightarrow$ is confluent iff for every $a,b,c \in X$ such that $a \rightarrow^{*} b$ and $a \rightarrow^{*} c$, there exists $d \in X$ such that $b \rightarrow^{*} d$ and $c \rightarrow^{*} d$.

This is a good property of rewriting in systems such as the lambda calculus (the Church-Rosser theorem), and as such it is a property one might expect for the hom-categories in a 2-categorical model of lambda calculus.

Another good property one might want to assume is termination, i.e. the lack of infinite chains of nonidentity arrows.

As stated in the definition, the notion of confluence is perfectly sensible if we replace “category” by “directed graph (quiver)”. However, it is also occasionally useful to strengthen the notion of confluence so that commutativity of the resulting square holds in the category. An example is Mac Lane’s proof of the coherence theorem for monoidal categories (as given in Categories Work), where the “rewrite” arrows are expanded (whiskered) instances of associativity morphisms $\alpha_{A B C}: (A \otimes B) \otimes C \to A \otimes (B \otimes C)$ (as opposed to their inverses) in a free monoidal category.

Related pages

• lambda-calculus

• diamond

• locally confluent

References

• John Baez, 2-categories of computation.

• Barnaby P. Hilken, Towards a proof theory of rewriting: the simply-typed 2λ-calculus, Theor. Comp. Sci. 170 (1996), 407-444.