Refactoring Heterogeneous Relation Algebras around Ordered
Categories and Converse
Wolfram Kahl
We present a reorganisation of popular theories of "reasoning
with relational flavour'', including allegories, Kleene algebras, and
Dedekind categories, into an relatively symmetric picture using ordered
categories as common base and defining converse independently from
joins and meets.
As an example application, we use this to regroup results about
formalisation of algebraic graph rewriting and thus exhibit
opportunities for applying these approaches in new settings.
Finally we discuss how this approach influences the design of
compatible approaches to formalisation and mechanisation of
relation-algebraic theories.
Journal on Relation Methods in Computer Science, Vol. 1, pp. 277-313,
2004