nLab confluent category

Confluent categories

Confluent categories

Definition

A category is confluent if for any span BACB \leftarrow A \to C, there exists a cospan BDCB \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,)(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,cXa,b,c \in X such that a *ba \rightarrow^{*} b and a *ca \rightarrow^{*} c, there exists dXd \in X such that b *db \rightarrow^{*} d and c *dc \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 α ABC:(AB)CA(BC)\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.

References

Last revised on March 18, 2024 at 15:38:58. See the history of this page for a list of all contributions to it.