# Confluent categories

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