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.

References

Revised on May 11, 2011 19:18:26 by Toby Bartels (64.89.62.77)