nLab
confluent category

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. 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 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

Revised on November 5, 2014 15:30:49 by Todd Trimble (67.81.95.215)