confluent category

Confluent categories


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.


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.


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